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