We now introduce a second example: a CTMC that models an N-place queue of jobs and a server which removes jobs from the queue and processes them. The PRISM code is as follows:
The PRISM Language: Example 2
This example also introduces a number of other PRISM language concepts, including constants, action labels and synchronisation. These are described in the following sections.