speed-ind.2100

Download

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

Origin

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.

Contents of file: model.prism

ctmc
const int T=2100;

module S1_def
  S1 : [0..250] init 200;
  [] S1=0 -> (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10)/50):(S1'=50);
  [] S1=50 -> (0.0075*S1/50):(S1'=0) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10)/50):(S1'=100);
  [] S1=100 -> (0.0075*S1/50):(S1'=50) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10)/50):(S1'=150);
  [] S1=150 -> (0.0075*S1/50):(S1'=100) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10)/50):(S1'=200);
  [] S1=200 -> (0.0075*S1/50):(S1'=150) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10)/50):(S1'=250);
  [] S1=250 -> (0.0075*S1/50):(S1'=200);
endmodule
module S2_def
  S2 : [0..100] init 0;
  [] S2=0 -> (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=10);
  [] S2=10 -> (0.0075*S2/10):(S2'=0) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=20);
  [] S2=20 -> (0.0075*S2/10):(S2'=10) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=30);
  [] S2=30 -> (0.0075*S2/10):(S2'=20) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=40);
  [] S2=40 -> (0.0075*S2/10):(S2'=30) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=50);
  [] S2=50 -> (0.0075*S2/10):(S2'=40) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=60);
  [] S2=60 -> (0.0075*S2/10):(S2'=50) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=70);
  [] S2=70 -> (0.0075*S2/10):(S2'=60) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=80);
  [] S2=80 -> (0.0075*S2/10):(S2'=70) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=90);
  [] S2=90 -> (0.0075*S2/10):(S2'=80) + (10*(0.099/(1.99+pow((0.5*S1),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/10):(S2'=100);
  [] S2=100 -> (0.0075*S2/10):(S2'=90);
endmodule
module S3_def
  S3 : [0..150] init 120;
  [] S3=0 -> (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=15);
  [] S3=15 -> (0.0075*S3/15):(S3'=0) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=30);
  [] S3=30 -> (0.0075*S3/15):(S3'=15) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=45);
  [] S3=45 -> (0.0075*S3/15):(S3'=30) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=60);
  [] S3=60 -> (0.0075*S3/15):(S3'=45) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=75);
  [] S3=75 -> (0.0075*S3/15):(S3'=60) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=90);
  [] S3=90 -> (0.0075*S3/15):(S3'=75) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=105);
  [] S3=105 -> (0.0075*S3/15):(S3'=90) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=120);
  [] S3=120 -> (0.0075*S3/15):(S3'=105) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=135);
  [] S3=135 -> (0.0075*S3/15):(S3'=120) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/15):(S3'=150);
  [] S3=150 -> (0.0075*S3/15):(S3'=135);
endmodule
module S4_def
  S4 : [0..120] init 0;
  [] S4=0 -> (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/40):(S4'=40);
  [] S4=40 -> (0.0075*S4/40):(S4'=0) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/40):(S4'=80);
  [] S4=80 -> (0.0075*S4/40):(S4'=40) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*S2),(2)))*10)/40):(S4'=120);
  [] S4=120 -> (0.0075*S4/40):(S4'=80);
endmodule
module Y_def
  Y : [0..90] init 0;
  [] Y=0 -> (10*0.099/(1.99+pow((0.5*B),(2)))*10/30):(Y'=30);
  [] Y=30 -> (0.0075*Y/30):(Y'=0) + (10*0.099/(1.99+pow((0.5*B),(2)))*10/30):(Y'=60);
  [] Y=60 -> (0.0075*Y/30):(Y'=30) + (10*0.099/(1.99+pow((0.5*B),(2)))*10/30):(Y'=90);
  [] Y=90 -> (0.0075*Y/30):(Y'=60);
endmodule
module Z_def
  Z : [0..90] init 0;
  [] Z=0 -> (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/30):(Z'=30);
  [] Z=30 -> (0.0075*Z/30):(Z'=0) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/30):(Z'=60);
  [] Z=60 -> (0.0075*Z/30):(Z'=30) + (10*(0.099/(1.99+pow((0.5*S4),(2)))*10+0.099/(1.99+pow((0.5*S3),(2)))*10)/30):(Z'=90);
  [] Z=90 -> (0.0075*Z/30):(Z'=60);
endmodule
module CC_def
  CC : [0..120] init 120;
  [] CC=0 -> (10*0.099/(1.99+pow((0.5*Z),(2)))*10/40):(CC'=40);
  [] CC=40 -> (0.0075*CC/40):(CC'=0) + (10*0.099/(1.99+pow((0.5*Z),(2)))*10/40):(CC'=80);
  [] CC=80 -> (0.0075*CC/40):(CC'=40) + (10*0.099/(1.99+pow((0.5*Z),(2)))*10/40):(CC'=120);
  [] CC=120 -> (0.0075*CC/40):(CC'=80);
endmodule
module XX_def
  XX : [0..90] init 0;
  [] XX=0 -> (10*0.099/(1.99+pow((0.5*AA),(2)))*10/30):(XX'=30);
  [] XX=30 -> (0.0075*XX/30):(XX'=0) + (10*0.099/(1.99+pow((0.5*AA),(2)))*10/30):(XX'=60);
  [] XX=60 -> (0.0075*XX/30):(XX'=30) + (10*0.099/(1.99+pow((0.5*AA),(2)))*10/30):(XX'=90);
  [] XX=90 -> (0.0075*XX/30):(XX'=60);
endmodule
const int AA=0;
const int B=120;

label "target" = ((S2 > 80) & (S3 < 20));

Contents of file: property.props

"change_state" : P=? [ F<=2100 "target"];

Contents of file: model.jani

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

Benchmark speed-ind.2100