|
A process is defined by a one or more local processes separated by commas. The definition is terminated by a full stop. STOP and ERROR are primitive local processes.
Example
Process = (a -> Local),
Local = (b -> STOP).
Action Prefix ->
|
If x is an action and P a process then (x->P) describes a process that initially engages in the action x and then behaves exactly as described by P.
|
Choice |
|
If x and y are actions then (x->P|y->Q) describes a process which initially engages in either of the actions x or y. After the first action has occurred, the subsequent behavior is described by P if the first action was x and Q if the first action was y.
|
Guarded Action
when
|
The choice (when B x -> P | y -> Q) means that when the guard B is true then the actions x and y are both eligible to be chosen, otherwise if B is false then the action x cannot be chosen.
|
Alphabet
Extension +
|
The alphabet of a process is the set of actions in which it can engage. P + S extends the alphabet of the process P with the actions in the set S.
|
Table A.1 – Process operators
|