model.prism (0.01 MB)
property.props (0.01 MB)
model.jani (0.36 MB)

Taken from QVBS (January 2026).
The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020.

Original Prism model and property files have been adapted for compatibility and simplicity:
- Constants: All open constants are now explicitly set within model.prism (no need to set them via command line)
- Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property.
- Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.

// 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) & (p5<4 | p5>13) & (p6<4 | p6>13) & (p7<4 | p7>13) & (p8<4 | p8>13) & (p9<4 | p9>13);
// some in admit
formula some_a	 = 	(p1>=14 & p1<=15) | (p2>=14 & p2<=15) | (p3>=14 & p3<=15) | (p4>=14 & p4<=15) | (p5>=14 & p5<=15) | (p6>=14 & p6<=15) | (p7>=14 & p7<=15) | (p8>=14 & p8<=15) | (p9>=14 & p9<=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) | (p5>=4 & p5<=5) | (p5>=10 & p5<=15) | (p6>=4 & p6<=5) | (p6>=10 & p6<=15) | (p7>=4 & p7<=5) | (p7>=10 & p7<=15) | (p8>=4 & p8<=5) | (p8>=10 & p8<=15) | (p9>=4 & p9<=5) | (p9>=10 & p9<=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) | (p5>=0 & p5<=3) | (p5>=7 & p5<=8) | (p6>=0 & p6<=3) | (p6>=7 & p6<=8) | (p7>=0 & p7<=3) | (p7>=7 & p7<=8) | (p8>=0 & p8<=3) | (p8>=7 & p8<=8) | (p9>=0 & p9<=3) | (p9>=7 & p9<=8);
// none in enter
formula none_e	 = 	(p1<2 | p1>3) & (p2<2 | p2>3) & (p3<2 | p3>3) & (p4<2 | p4>3) & (p5<2 | p5>3) & (p6<2 | p6>3) & (p7<2 | p7>3) & (p8<2 | p8>3) & (p9<2 | p9>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
	
	module process5 = process0 [p0=p5, p5=p0] endmodule
	
	module process6 = process0 [p0=p6, p6=p0] endmodule
	
	module process7 = process0 [p0=p7, p7=p0] endmodule
	
	module process8 = process0 [p0=p8, p8=p0] endmodule
	
	module process9 = process0 [p0=p9, p9=p0] endmodule

label "target" = (p1=10);

"live": Pmax=? [F "target"];

File too large to display (size: 0.36 MB).