A process is defined by one or more local processes separated by commas. The definition is terminated by a full stop. STOP and ERROR are primitive local processes.
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. |