s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3593 Commits
5 Branches
0 Tags
31 MiB
 
 
 
 
 
 
Branch: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
prism-accumulation/prism-examples/mutual
Dave Parker 6f5d45b888
Example fixes re new semantics (result reported for initial state by default) - need more filters. 		15 years ago
..
.autopp Tidy up mutual (and add pp files). 18 years ago
.mutualN.nm.pp Tidy up mutual (and add pp files). 18 years ago
README.txt Added txt extension to README files. 15 years ago
auto Tidy up mutual (and add pp files). 18 years ago
mutual.pctl Example fixes re new semantics (result reported for initial state by default) - need more filters. 15 years ago
mutual3.nm Tidy up mutual (and add pp files). 18 years ago
mutual4.nm Tidy up mutual (and add pp files). 18 years ago
mutual5.nm Tidy up mutual (and add pp files). 18 years ago
mutual8.nm Tidy up mutual (and add pp files). 18 years ago
mutual10.nm Tidy up mutual (and add pp files). 18 years ago

README.txt 

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