// randomized two process wait-free test-and-set [TV02]
// gxn/dxp 12/07/02

mdp

// tester process
module tester

	t : [0..1];

	[] t=0 -> (t'=1); // start test

endmodule


// process 0
module proc0
	
	// local states
	l0 : [0..10];
	// 0  - rst	
	// 1  - me
	// 2  - not me
	// 3  - choose
	// 4  - to me
	// 5  - to he
	// 6  - he
	// 7  - not he
	// 8  - tst0
	// 9  - tst1
	// 10 - free

	// shared variable owned by process 0
	R0 : [0..3];
	// 0 - rst
	// 1 - choose
	// 2 - he
	// 3 - me
	
	// rst
	[p0] l0=0 -> (R0'=3) & (l0'=1);
	// me
	[p0] l0=1 & R1=3  -> (l0'=2);
	[p0] l0=1 & !R1=3 -> (l0'=8); // finished and test not started
	// not me
	[p0] l0=2 -> (R0'=1) & (l0'=3);
	// choose
	[p0] l0=3 & R1=2 -> (l0'=4); // R1=he
	[p0] l0=3 & R1=1 -> 0.5 : (l0'=4) + 0.5 : (l0'=5);  // R1=choose 
	[p0] l0=3 & !(R1=2 | R1=1) -> (l0'=5); // otherwise
	// to me
	[p0] l0=4 -> (R0'=3) & (l0'=1);
	// to he
	[p0] l0=5 -> (R0'=2) & (l0'=6);
	// he
	[p0] l0=6 & R1=2  -> (l0'=7);
	[p0] l0=6 & !R1=2 -> (l0'=9); // finished and test not started
	// not he
	[p0] l0=7 -> (R0'=1) & (l0'=3);
	// tst0 (removed transitions once test starts as only looking at one test and set operation)
	[p0] t=0 & l0=8 -> (R0'=0) & (l0'=0);
	// tst1 (removed transitions once test starts as only looking at one test and set operation)
	[p0] t=0 & l0=9 & !R1=0 -> (l0'=9); // R1 not rst
	[p0] t=0 & l0=9 & R1=0 -> (l0'=10); // R1 equals rst
	// free
	[p0] l0=10 -> (R0'=3) & (l0'=1);

endmodule  

// construct process 1 through renaming
module proc1=proc0[l0=l1,R0=R1,R1=R0,p0=p1] endmodule

// rewards
rewards "process0" // reads/writes by process 0 (all transitions of process 0 require one access)
	[p0] t=1 : 1;
endrewards
rewards "process1" // reads/writes by process 1 (all transitions of process 1 require one access)
	[p1] t=1 : 1;
endrewards