Concurrency: State Models and Java Programs

Appendix A. FSP Quick Reference

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

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.

Composite Processes

A composite process is the parallel composition of one or more processes. The definition of a composite process is preceded by ||.

Example

||Composite = (P || Q).

Table A.2. Composite process operators

Parallel Composition ||	If P and Q are processes then (P||Q) represents the concurrent execution of P and Q.
Replicator forall	forall [i:1..N] P(i) is the parallel composition (P(1) || ... || P(N)).
Process Labeling ...