prism-accumulation/prism-examples/mutual

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.cs.bham.ac.uk/~dxp/prism/casestudies/mutual.html



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



[PZ86]

A. Pnueli and L. Zuck

Verification of Multiprocess Probabilistic Protocols

Distributed Computing, 1(1):53-72, 1986