Appendix A: FSP Quick Reference

A.1 Processes

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.

Example

 Process = (a -> Local), Local   = (b -> STOP).

Table A.1: Process operators
Open table as spreadsheet

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.