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));