// three processor mutual exclusion [Rab82]
// with global variables to remove sychronization 
// gxn/dxp 02/02/00

nondeterministic

// global variables (all modules can read and write)
// c=0 critical section free
// c=1 critical section not free
// b current highest draw
// r current round 

global c : [0..1];
global b : [0..6];
global r : [1..2];

// local variables: process i 
// state: pi
//  0 remainder
//  1 trying
//  2 critical section
// current draw: bi
// current round: ri

// atomic formula for process 1 drawing
formula draw = p1=1 & (b<b1 | r!=r1);

module process1

	p1 : [0..2];
	b1 : [0..6];
	r1 : [0..2];

	// enter trying
	[] p1=0 -> (p1'=0);
	// remain in remainder
	[] p1=0 -> (p1'=1);
	// make a draw
	[] draw -> 0.5     : (b1'=1) & (r1'=r) & (b'=max(b,1))
		 + 0.25    : (b1'=2) & (r1'=r) & (b'=max(b,2))
		 + 0.125   : (b1'=3) & (r1'=r) & (b'=max(b,3))
		 + 0.0625  : (b1'=4) & (r1'=r) & (b'=max(b,4))
		 + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5))
		 + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6));
	// enter critical section and randomly set r to 1 or 2
	[] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2)
				     + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2);
	// loop when trying and cannot make a draw or enter critical section
	[] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1);
	// leave crictical section
	[] p1=2 -> (p1'=0) & (c'=0);
	// stay in critical section
	[] p1=2 -> (p1'=2);
	
endmodule

// construct further modules through renaming

module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule