www.prismmodelchecker.org

PRISM code: rabin5.forgrip.nm

mdp

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

module process1

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

	[] (p1=0) -> (p1'=0);
	[] (p1=0) -> (p1'=1);
	[] (p1=1) & (b<b1 | r!=r1) -> 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.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6))
	                            + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7));
	[] (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);
	[] (p1=1) & (r1=r & b1<=b & ((c=0 & b1!=b) | c=1)) -> (p1'=p1);
	[] (p1=2) -> (p1'=0) & (c'=0);
	[] (p1=2) -> (p1'=2);
	
endmodule

module process2 = process1 [p1=p2, p2=p1, b1=b2, b2=b1, r1=r2, r2=r1] endmodule
module process3 = process1 [p1=p3, p3=p1, b1=b3, b3=b1, r1=r3, r3=r1] endmodule
module process4 = process1 [p1=p4, p4=p1, b1=b4, b4=b1, r1=r4, r4=r1] endmodule
module process5 = process1 [p1=p5, p5=p1, b1=b5, b5=b1, r1=r5, r5=r1] endmodule
View: printable version          Download: rabin5.forgrip.nm

Case Studies