Process Model
Process Model
From the first set of notes we saw that the behaviour of a process is defined by the sequence of statements it executes. The notation:
P = (a ® P’)
means that process P is said to engage in the event or action a and then behave like P’. If P’ = (b ® P’’) it follows that:
P = (a ® b ® P’’)
A clock process which initialises and then repeatedly engages in tick events can be modelled as:
clock = (init ® repeat)
repeat = (tick ® repeat)
The alphabet of a process is the set of events/actions that it may engage in. The alphabet of a process P is written aP. Consequently,
a clock = {init, tick}