// mutual exclusion [PZ82]
// dxp/gxn 19/12/99

mdp

// atomic formula
// none in low, high, tie
formula none_lht = 	(p1<4 | p1>13) & (p2<4 | p2>13) & (p3<4 | p3>13) & (p4<4 | p4>13);
// some in admit
formula some_a	 = 	(p1>=14 & p1<=15) | (p2>=14 & p2<=15) | (p3>=14 & p3<=15) | (p4>=14 & p4<=15);
// some in high, admit
formula some_ha	 = (p1>=4 & p1<=5) | (p1>=10 & p1<=15) | (p2>=4 & p2<=5) | (p2>=10 & p2<=15) | (p3>=4 & p3<=5) | (p3>=10 & p3<=15) | (p4>=4 & p4<=5) | (p4>=10 & p4<=15);
// none in high, tie, admit
formula none_hta = (p1>=0 & p1<=3) | (p1>=7 & p1<=8) | (p2>=0 & p2<=3) | (p2>=7 & p2<=8) | (p3>=0 & p3<=3) | (p3>=7 & p3<=8) | (p4>=0 & p4<=3) | (p4>=7 & p4<=8);
// none in enter
formula none_e	 = 	(p1<2 | p1>3) & (p2<2 | p2>3) & (p3<2 | p3>3) & (p4<2 | p4>3);

// process 0
module process0

	p0: [0..15] init 1;
	
	[] p0=0 -> (p0'=0);
	[] p0=0 -> (p0'=1);
	[] p0=1 -> (p0'=2);
	[] p0=2 &  (none_lht | some_a) -> (p0'=3);
	[] p0=2 & !(none_lht | some_a) -> (p0'=2);
	[] p0=3 -> (p0'=4);
	[] p0=3 -> (p0'=7);
	[] p0=4 &  some_ha -> (p0'=5);
	[] p0=4 & !some_ha -> (p0'=10);
	[] p0=5 -> (p0'=6);
	[] p0=6 &  some_ha -> (p0'=6);
	[] p0=6 & !some_ha -> (p0'=9);
	[] p0=7 &  none_hta -> (p0'=8);
	[] p0=7 & !none_hta -> (p0'=7);
	[] p0=8  -> (p0'=9);
	[] p0=9  -> 0.5 : (p0'=4) + 0.5 : (p0'=7);
	[] p0=10 -> (p0'=11);
	[] p0=11 &  none_lht -> (p0'=13);
	[] p0=11 & !none_lht -> (p0'=12);
	[] p0=12 -> (p0'=0);
	[] p0=13 -> (p0'=14);
	[] p0=14 &  none_e -> (p0'=15);
	[] p0=14 & !none_e -> (p0'=14);
	[] p0=15 -> (p0'=0);
	
endmodule

// construct further modules through renaming

	module process1 = process0 [p0=p1, p1=p0] endmodule
	
	module process2 = process0 [p0=p2, p2=p0] endmodule
	
	module process3 = process0 [p0=p3, p3=p0] endmodule
	
	module process4 = process0 [p0=p4, p4=p0] endmodule


label "target" = (p1=10);