// N-processor mutual exclusion [Rab82]
// with global variables to remove sychronization 
// gxn/dxp 03/12/08

// modified version to verify a variant of the bounded waiting property
// namely the probability a process entries the critical sectiongiven it tries

// note we have removed the self loops to allow the fairness constraints 
// to be ignored during verification

// split the drawing phase into two steps but is still atomic as no
// other process can move one the first step has been made

mdp

// size of shared counter
const int K = 7; // 4+ceil(log_2 N)

// 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..K];
global r : [1..2];

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

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

// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0);

module process1

	p1 : [0..2];
	b1 : [0..K];
	r1 : [0..2];
	draw1 : [0..1];

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

// construct further modules through renaming
module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule
module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule
module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule
module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule
module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule

// formulas/labels for use in properties:

// number of processes in critical section
formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0);

// one of the processes is trying
label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1;

// one of the processes is in the critical section
label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2;

// maximum value of the bi's
formula maxb = max(b1,b2 ,b3 ,b4 ,b5 ,b6 );