Choice "|"

(a -> P | b -> Q) describes a process which initially engages in either of the actions a or b. After the first action has been performed, subsequent behaviour is described by P if the first event was a, or by Q if the first event was b. The LTS corresponding to this process has two possible transitions a and b out of the initial state. The example describes the behaviour of a dispensing machine which dispenses coffee if the black button is pressed and tea if the white button is pressed.

DRINKS = (black -> coffee -> DRINKS | white -> tea -> DRINKS).




FSP follows CCS rather than CSP in not distinguishing between internal and external choice. Consequently, non-deterministic choice is simply expressed by having the same action leading to two different succeeding behaviours as shown in the example which describes tossing a coin.

COIN = (toss -> heads -> COIN |toss -> tails -> COIN).


Action Sets

If a number of different actions are succeeded by the same behaviour, it may be more succinct to use an action set rather than explicit choice. For example, the following processes are exactly equivalent and generate the same LTS.

DOOR1 = (open -> DOOR1 | close -> DOOR1).

DOOR2 = ({open, close} -> DOOR2).