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:
const int N = 10;
const double mu = 1/10;
const double lambda = 1/2;
const double gamma = 1/3;
q : [0..N];
 q<N -> mu:(q'=q+1);
 q=N -> mu:(q'=q);
[serve] q>0 -> lambda:(q'=q-1);
s : [0..1];
[serve] s=0 -> 1:(s'=1);
 s=1 -> gamma:(s'=0);
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.