ctmc
const int N1;
const int N2;
module cl
cl : [0..N2] init N2;
[e1] cl>0 -> cl : (cl'=cl-1);
[e2] cl>0 -> cl : (cl'=cl-1);
[e3] cl<N2 -> (N2-cl) : (cl'=cl+1);
[e4] cl<N2 -> (N2-cl) : (cl'=cl+1);
endmodule
module mg
mg : [0..N1] init N1;
mg_p : [0..N1] init 0;
[e1] mg>0 & mg_p<N1 -> mg : (mg'=mg-1) & (mg_p'=mg_p+1);
[e2] mg_p>0 -> mg_p : (mg_p'=mg_p-1);
[e3] mg_p>0 & mg<N1 -> mg_p : (mg'=mg+1) & (mg_p'=mg_p-1);
[e4] mg_p+mg<N1 -> N1-(mg_p+mg) : (mg_p'=mg_p+1);
endmodule
const double e1rate = 10;
const double e2rate = 100;
const double e3rate = 50;
const double e4rate = 5;
module base_rates
dummy : bool;
[e1] true -> e1rate : true;
[e2] true -> e2rate : true;
[e3] true -> e3rate : true;
[e4] true -> e4rate : true;
endmodule
rewards "percentage_mg"
true : 100*mg/N1;
endrewards
rewards "percentage_mgplus"
true : 100*mg_p/N1;
endrewards
rewards "percentage_mgplus2"
true : max(100*(N1-(mg_p+mg))/N1,0);
endrewards