Action Prefix "->"
describes a process which engages in the action a and then behaves as described by P. More operationally, action prefix defines a transition between states. The following recursive definition describes the process CLOCK which repeatedly engages in the action tick.
(a -> P)
CLOCK = (tick -> CLOCK).
The LTS corresponding to the definition above is:
In FSP action labels (such as tick) must always start with a lowercase character and process names must begin with a capital letter (e.g. CLOCK). A primitive process definition is terminated by a full stop. A more complex CLOCK which has two states and engages in the action tick and then tock is defined below:
CLOCK2 = (tick -> TOCK), TOCK = (tock -> CLOCK2).
The scope of the local process TOCK is only the definition of CLOCK2. TOCK cannot be referred to globally. Commas separate local definitions within a primitive process. In this simple process, the local process name is not necessary since its first occurrence can be substituted with its definition:
CLOCK2 = (tick -> (tock -> CLOCK2)).
The internal brackets may be omitted to give:
CLOCK2 = (tick -> tock -> CLOCK2).
The three definitions for CLOCK2 are exactly equivalent and generate the LTS depicted below:
The LTS diagrams here are as generated by LTSA. The initial state is always numbered zero and transitions are read clockwise. Thus tick is a transition from 0 to 1 and tock is a transition from 1 to 0.