We now consider a second example: a self-stabilisation algorithm due to Herman. A self-stabilisation algorithm for a network of processes is a protocol which, when started from some possibly "illegal" start state, returns to a "legal" state without any outside intervention and within some finite number of steps. We call a "legal" state a stable state.
Here is a PRISM model of Herman's algorithm for 7 processes:
// herman's self stabilising algorithm [Her90] // gxn/dxp 13/07/02 // the procotol is synchronous with no nondeterminism (a DTMC) dtmc // module for process 1 module process1 x1 : [0..1] init 1; [step] (x1=x7) -> 0.5 : (x1'=0) + 0.5 : (x1'=1); [step] !(x1=x7) -> (x1'=x7); endmodule // add further processes through renaming module process2 = process1[x1=x2, x7=x1 ] endmodule module process3 = process1[x1=x3, x7=x2 ] endmodule module process4 = process1[x1=x4, x7=x3 ] endmodule module process5 = process1[x1=x5, x7=x4 ] endmodule module process6 = process1[x1=x6, x7=x5 ] endmodule module process7 = process1[x1=x7, x7=x6 ] endmodule // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x5?1:0)+(x5=x6?1:0)+(x6=x7?1:0)+(x7=x1?1:0); // rewards (to calculate expected number of steps) rewards "steps" true : 1; endrewards
The processes are arranged in a ring and are identical. Notice how we use PRISM's module renaming facility to avoid duplicating the module definition for each process.
Have a look at the code and work out what a process does at each step of the protocol.
Notice the step action in the square brackets at the start of every command.
This is used to force all 7 processes to synchronise (move simultaneously at each step).
You can read more about synchronisation in the
manual.
Download the model file herman7.pm from above and load it into PRISM.
The state of each process is given by a single 0/1-valued variable. Initially, this value is 1 for all processes (note how this is done in the variable definition in the model file).
What is the maximum possible number of states that this model can be in?
Are all of these states reachable from the initial configuration (1,1,1,1,1,1,1) of the model?
Select the "Model | Build model" menu option
and look at the information displayed in the bottom left of the GUI to find out.
Take a look at the log to see additional information displayed about the model building process.
Download the property file below and load it into PRISM:
// stable states - where only one process has the same value as the process to its left label "stable" = num_tokens=1; // from the initial state, a stable state is reached with probability 1 P>=1 [ F "stable" ]
For this self-stabilisation algorithm, a stable state is defined as one in which only a single process has a token. A process is said to possess a token if its variable is the same as the process to its left.
Look at the label "stable" which is defined in the file above
and the formula num_tokens from the model file which it uses.
Check that you understand how it relates to the definition of a stable state.
Look at the expressions
section of the manual if not.
Use the PRISM simulator to generate some random paths through the model.
Click on the "stable" label in the top-right part of the simulator
to help you identify which states of these paths are stable.
Note that in this model of the algorithm, we do not actually terminate when a stable state has been reached.
We would like to know whether, from the initial state, a stable state is eventually reached with probability 1.
Check this by verifying the property included in the herman7.pctl file that you loaded into PRISM
(do not forget to deselect the "Use Simulation" option if it is still selected).
If you used a non-probabilistic model checker to verify whether
"from the initial state, a stable state is always eventually reached", what would the result be?
Modify the existing property (double-click or right-click and "Edit") to see if
"the probability of a stable state being reached within 10 steps is (greater than or equal to) 1".
Is it greater than 0.5?
What is the actual probability?
(If you need help, read about the P Operator in the PRISM manual
here
and here.)
Notice that, like in the die example,
we have assigned a reward of 1 to each state of the model.
Create and verify a new property to answer the question
"what is the expected number of steps required for the self-stabilisation algorithm to reach a stable state?".
So far, all our analysis has been for a fixed initial state of the model. We will now carry out a more exhaustive examination of the protocol by considering different classes of initial configuration. PRISM allows a model to have more than one initial state.
Modify the model by removing the "init 1"
part of the definition for variable x1
(and thus also for x2, x3, ... ,x7
since they are defined by renaming).
Add the following code to the end of the model:
init true endinit
Check that the model still builds without errors ("Model | Build model").
Any possible configuration of the process is now considered as an initial state of the model.
Download the following modified properties file and load it into PRISM:
const int k; // states with k tokens label "k_tokens" = num_tokens=k; // stable states - where only one process has the same value as the process to its left label "stable" = num_tokens=1; // maximum expected time to reach a stable state (for all k-token configurations) R=? [ F "stable" {"k_tokens"}{max} ]
This property allows us to compute "the maximum expected time to reach a stable state, starting from any initial configuration in which there are k tokens".
Verify this property for k=7.
Do you get the same value as earlier?
(You should.)
There is an unproven conjecture that, for any number N of processes, the worst-case expected time to reach a stable state always occurs when there are initially 3 tokens. We can't prove this with PRISM, but we can investigate whether it is true for some values of N (in this case, we have N=7 processes).
Create an experiment to compute and plot a graph of the values of the property
for all odd values of k between 1 and 7.
(Again, make sure "Use Simulation" is not still selected.)
[Note: the way that this algorithm works, even numbers of tokens cannot occur.]
Look in the log. You can see exactly which of the various possible configurations result in these worst-case answers.
[Note: in cases where there are more than 10 such configurations, PRISM just prints the first 10.]
For which value of k is the expected time lowest? Why?
For which value is it highest?
Create another PRISM property which computes the minimum expected time to reach a stable state,
starting from any initial configurations in which there are k tokens.
Plot this value for k=1,3,5,7 on a single graph.
This protocol has some other curious properties that can be investigated with PRISM.
In particular, try modifying the algorithm so that the random choice of
each process occurs with probability p,
where p is an undefined constant, rather than 0.5.
Investigate what happens as you vary p.
See here for more details.
Next: Part C