majority.2100

Download

model.prism (0.01 MB)
property.props (0.01 MB)
model.jani (0.55 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 D_def
  D : [0..250] init 200;
  [] D=0 -> (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10+0.099/(1.99+pow((0.5*Z),(2)))*10)/50):(D'=50);
  [] D=50 -> (0.0075*D/50):(D'=0) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10+0.099/(1.99+pow((0.5*Z),(2)))*10)/50):(D'=100);
  [] D=100 -> (0.0075*D/50):(D'=50) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10+0.099/(1.99+pow((0.5*Z),(2)))*10)/50):(D'=150);
  [] D=150 -> (0.0075*D/50):(D'=100) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10+0.099/(1.99+pow((0.5*Z),(2)))*10)/50):(D'=200);
  [] D=200 -> (0.0075*D/50):(D'=150) + (10*(0.099/(1.99+pow((0.5*XX),(2)))*10+0.099/(1.99+pow((0.5*Y),(2)))*10+0.099/(1.99+pow((0.5*Z),(2)))*10)/50):(D'=250);
  [] D=250 -> (0.0075*D/50):(D'=200);
endmodule
module Y_def
  Y : [0..120] init 0;
  [] Y=0 -> (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Y'=30);
  [] Y=30 -> (0.0075*Y/30):(Y'=0) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Y'=60);
  [] Y=60 -> (0.0075*Y/30):(Y'=30) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Y'=90);
  [] Y=90 -> (0.0075*Y/30):(Y'=60) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Y'=120);
  [] Y=120 -> (0.0075*Y/30):(Y'=90);
endmodule
module Z_def
  Z : [0..120] init 0;
  [] Z=0 -> (10*(0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Z'=30);
  [] Z=30 -> (0.0075*Z/30):(Z'=0) + (10*(0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Z'=60);
  [] Z=60 -> (0.0075*Z/30):(Z'=30) + (10*(0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Z'=90);
  [] Z=90 -> (0.0075*Z/30):(Z'=60) + (10*(0.099/(1.99+pow((0.5*B),(2)))*10+0.099/(1.99+pow((0.5*D),(2)))*10)/30):(Z'=120);
  [] Z=120 -> (0.0075*Z/30):(Z'=90);
endmodule
module CC_def
  CC : [0..150] init 120;
  [] CC=0 -> (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=10);
  [] CC=10 -> (0.0075*CC/10):(CC'=0) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=20);
  [] CC=20 -> (0.0075*CC/10):(CC'=10) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=30);
  [] CC=30 -> (0.0075*CC/10):(CC'=20) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=40);
  [] CC=40 -> (0.0075*CC/10):(CC'=30) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=50);
  [] CC=50 -> (0.0075*CC/10):(CC'=40) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=60);
  [] CC=60 -> (0.0075*CC/10):(CC'=50) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=70);
  [] CC=70 -> (0.0075*CC/10):(CC'=60) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=80);
  [] CC=80 -> (0.0075*CC/10):(CC'=70) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=90);
  [] CC=90 -> (0.0075*CC/10):(CC'=80) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=100);
  [] CC=100 -> (0.0075*CC/10):(CC'=90) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=110);
  [] CC=110 -> (0.0075*CC/10):(CC'=100) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=120);
  [] CC=120 -> (0.0075*CC/10):(CC'=110) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=130);
  [] CC=130 -> (0.0075*CC/10):(CC'=120) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=140);
  [] CC=140 -> (0.0075*CC/10):(CC'=130) + (10*0.099/(1.99+pow((0.5*EE),(2)))*10/10):(CC'=150);
  [] CC=150 -> (0.0075*CC/10):(CC'=140);
endmodule
module XX_def
  XX : [0..120] init 0;
  [] XX=0 -> (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10)/30):(XX'=30);
  [] XX=30 -> (0.0075*XX/30):(XX'=0) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10)/30):(XX'=60);
  [] XX=60 -> (0.0075*XX/30):(XX'=30) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10)/30):(XX'=90);
  [] XX=90 -> (0.0075*XX/30):(XX'=60) + (10*(0.099/(1.99+pow((0.5*AA),(2)))*10+0.099/(1.99+pow((0.5*B),(2)))*10)/30):(XX'=120);
  [] XX=120 -> (0.0075*XX/30):(XX'=90);
endmodule
module EE_def
  EE : [0..45] init 0;
  [] EE=0 -> (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=3);
  [] EE=3 -> (0.0075*EE/3):(EE'=0) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=6);
  [] EE=6 -> (0.0075*EE/3):(EE'=3) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=9);
  [] EE=9 -> (0.0075*EE/3):(EE'=6) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=12);
  [] EE=12 -> (0.0075*EE/3):(EE'=9) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=15);
  [] EE=15 -> (0.0075*EE/3):(EE'=12) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=18);
  [] EE=18 -> (0.0075*EE/3):(EE'=15) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=21);
  [] EE=21 -> (0.0075*EE/3):(EE'=18) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=24);
  [] EE=24 -> (0.0075*EE/3):(EE'=21) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=27);
  [] EE=27 -> (0.0075*EE/3):(EE'=24) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=30);
  [] EE=30 -> (0.0075*EE/3):(EE'=27) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=33);
  [] EE=33 -> (0.0075*EE/3):(EE'=30) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=36);
  [] EE=36 -> (0.0075*EE/3):(EE'=33) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=39);
  [] EE=39 -> (0.0075*EE/3):(EE'=36) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=42);
  [] EE=42 -> (0.0075*EE/3):(EE'=39) + (10*0.099/(1.99+pow((0.5*D),(2)))*10/3):(EE'=45);
  [] EE=45 -> (0.0075*EE/3):(EE'=42);
endmodule
const int AA=0;
const int B=120;

label "target" = ((EE > 40) & (CC < 20));

Contents of file: property.props

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

Contents of file: model.jani

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

Benchmark majority.2100