Action Prefix "->"


(a -> P) 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.

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:

LTS diagrams

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.