(Pnueli & Zuck)

This case study is based on Pnueli and Zuck's [PZ86] probabilistic
symmetric solution to the *n*-process mutual exclusion problem.
The model is represented as an MDP.
We let **N** denotes the number of processes.
By way of example, the PRISM source code for the case where **N = 3** is given below.

// mutual exclusion [PZ82] // dxp/gxn 19/12/99 mdp // atomic formula // none in low, high, tie formula none_lht = p2!=4..13 & p3!=4..13; // some in admit formula some_a = p2=14..15 | p3=14..15; // some in high, admit formula some_ha = p2=4..5,10..15 | p3=4..5,10..15; // none in high, tie, admit formula none_hta = p2=0..3,7..8 & p3=0..3,7..8; // none in enter formula none_e = p2!=2..3 & p3!=2..3; // process 1 module process1 p1: [0..15]; [] p1=0 -> (p1'=0); [] p1=0 -> (p1'=1); [] p1=1 -> (p1'=2); [] p1=2 & (none_lht | some_a) -> (p1'=3); [] p1=2 & !(none_lht | some_a) -> (p1'=2); [] p1=3 -> (p1'=4); [] p1=3 -> (p1'=7); [] p1=4 & some_ha -> (p1'=5); [] p1=4 & !some_ha -> (p1'=10); [] p1=5 -> (p1'=6); [] p1=6 & some_ha -> (p1'=6); [] p1=6 & !some_ha -> (p1'=9); [] p1=7 & none_hta -> (p1'=8); [] p1=7 & !none_hta -> (p1'=7); [] p1=8 -> (p1'=9); [] p1=9 -> 0.5 : (p1'=4) + 0.5 : (p1'=7); [] p1=10 -> (p1'=11); [] p1=11 & none_lht -> (p1'=13); [] p1=11 & !none_lht -> (p1'=12); [] p1=12 -> (p1'=0); [] p1=13 -> (p1'=14); [] p1=14 & none_e -> (p1'=15); [] p1=14 & !none_e -> (p1'=14); [] p1=15 -> (p1'=0); endmodule // construct further modules through renaming module process2 = process1 [p1=p2, p2=p1] endmodule module process3 = process1 [p1=p3, p3=p1] endmodule

The table below shows statistics for each model we have built.
The first section gives the number of **states** in the MDP representing the model.
The second part refers to the MTBDD which represents this MDP:
the total number of **nodes** and
the number of **leaves** (terminal nodes).

N: |
Model: |
MTBDD: |
|||

States: |
Nodes: |
Leaves: |
|||

3 | 2,368 | 1,802 | 3 | ||

4 | 27,600 | 4,100 | 3 | ||

5 | 308,800 | 7,149 | 3 | ||

8 | 3.9x10^{8} | 20,736 | 3 | ||

10 | 4.4x10^{10} | 33,494 | 3 |

The table below gives the times taken to construct the models. There are two stages. Firstly, the system description (in our module based language) is parsed and converted to the MTBDD representing it. Secondly, reachability is performed to identify non-reachable states and the MTBDD is filtered accordingly. Reachability is performed using a BDD based fixpoint algorithm. The number of iterations for this process is also given.

N: |
Construction: |
Reachability: |
|||

Time (s): |
Time (s): |
Iter.s: |
|||

3 | 0.58 | 0.13 | 22 | ||

4 | 0.67 | 0.48 | 28 | ||

5 | 0.72 | 1.23 | 34 | ||

8 | 1.09 | 9.02 | 52 | ||

10 | 1.44 | 19.5 | 64 |

**Scheduler-Liveness:**for each time*t*and any process*P*_{i}not in its*remainder phase*at time*t*, there exists a time*t*' >*t*in which*P*_{i}makes a move.

This corresponds to the conditions on the *adversary/scheduler*
which we impose by model checking against only *fair* adversaries.

We have model checked the following properties:

// theorem 1 (mutual exclusion) !((p1>9) & (p2>9)) & !((p1>9) & (p3>9)) & !((p2>9) & (p3>9)) // theorem 2 (liveness - if process 1 tries then eventually it enters the critical section) (p1=1) => P>=1 [ true U (p1=10) ] // lemma c (if the crical section is occupied then eventually it becomes clear) (p1>9) | (p2>9) | (p3>9) => P>=1 [ true U (p1<10) & (p2<10) & (p3<10) ] // lemma d (if a process is between 4 and 13 (in our version) then eventually some process gets to 14) ((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) => P>=1 [ true U (p1=14) | (p2=14) | (p3=14) ]

**Theorem 1 from [PZ86] (Mutual Exclusion):**the model checking statistics for this property are given below.**N:****Time (s):**3 0.03 4 0.04 5 0.05 8 0.08 10 0.11

**Conclusion:**the property holds in all states**Theorem 2 from [PZ86] (Liveness):**the model checking statistics for this property are given below.**N:****Precomputation:****Main Algorithm:****Time (s):****Iterations:****Time (s):****Iterations:**3 0.26 27 0 0 4 1.32 36 0 0 5 4.63 45 0 0 8 47.3 72 0 0 10 127 90 0 0

**Conclusion:**the property holds in all states.**Lemma C from [PZ86]:**the model checking statistics for this property are given below.**N:****Precomputation:****Main Algorithm:****Time (s):****Iterations:****Time (s):****Iterations:**3 0.11 10 0 0 4 0.52 12 0 0 5 1.30 14 0 0 8 3.87 20 0 0 10 6.08 24 0 0

**Conclusion:**the property holds in all states.**Lemma D from [PZ86]:**the model checking statistics for this property are given below.**N:****Precomputation:****Main Algorithm:****Time (s):****Iterations:****Time (s):****Iterations:**3 0.23 22 0 0 4 1.13 29 0 0 5 3.35 37 0 0 8 28.5 61 0 0 10 76.3 77 0 0

**Conclusion:**the property holds in all states.