Another feature of PRISM introduced in Example 2 is synchronisation.
In the style of many process algebras, we allow commands to be labelled with actions.
These are placed inside the square brackets which mark the start of the command,
serve in this command from Example 2:
These actions can be used to force two or more modules to make transitions simultaneously
(i.e. to synchronise).
For example, in state
the composed model can move to state
synchronising over the
The rate of this transition is equal to the product of the two individual rates
(in this case,
lambda * 1 = lambda).
The product of two rates does not always meaningfully represent the rate of a synchronised transition.
A common technique, as seen here, is to make one action passive, with rate 1 and one action active,
which actually defines the rate for the synchronised transition.
By default, all modules are combined using the standard CSP parallel composition
(i.e. modules synchronise over all their common actions).