File: bakery.pml

package info (click to toggle)
spin 6.5.2%2Bdfsg-2
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 2,512 kB
  • sloc: ansic: 39,876; yacc: 1,021; makefile: 58; sh: 13
file content (24 lines) | stat: -rwxr-xr-x 488 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
 
/* Lamport's Bakery algorithm for 2 processes */

byte turn[2];  /* who's turn is it?           */
byte mutex;    /* # procs in critical section */

active [2] proctype P()
{	byte i = _pid;
	do
	:: turn[i] = 1;
		turn[i] = turn[1-i] + 1;
		(turn[1-i] == 0) || (turn[i] < turn[1-i]) ->
		mutex++;
CS:		/* critical section */
		mutex--;
		turn[i] = 0
	od
}

/*
 * place the ltl property goes at the end,
 * so that P and mutex are defined
 */

ltl invariant { [] ((P@CS) -> (mutex == 1)) }