This case study is based on Pnueli and Zuck's [PZ86] probabilistic symmetric solution to the n-process mutual exclusion problem.

For reference, these are the local states of each process:

No:	No:	Description:			State:
--------------------------------------------------------------
0	0	idle				uninterested
1	1	trying				uninterested
2	2	trying				enter 
3	3	trying				enter 
4	7	trying				high
5	8	trying				high
6	9	trying				tie
7	10	trying				low
8	11	trying				low
9	12	trying				tie
10	13	in critical section		high
11	14	in critical section		high
12	15	in critical section		high
13	17	in critical section		high
14	18	leaving	critical section	admit
15	19	leaving	critical section	admit

For more information, see: http://www.prismmodelchecker.org/casestudies/mutual.php

=====================================================================================

[PZ86]
A. Pnueli and L. Zuck
Verification of Multiprocess Probabilistic Protocols
Distributed Computing, 1(1):53-72, 1986