dtmc
const int N=4;
const int Nh=2;
const double PF=0.5;
const double x1 ;
const double x2 ;
const double x3 = 0;
const double x4 = 0;
const double ra=3;
const double rc=1;
const bool m1 = false;
const bool m2 = false;
const bool m3 = true;
const bool m4 = true;
formula msgTo1 = i=1 & (s=1 | s=4);
formula msgTo2 = i=2 & (s=1 | s=4);
formula msgTo3 = i=3 & (s=1 | s=4);
formula msgTo4 = i=4 & (s=1 | s=4);
formula decision1 = msgTo1 & !m1 & ii!=1 ;
formula decision2 = msgTo2 & !m2 & ii!=2 ;
formula decision3 = msgTo3 & !m3 & ii!=3 ;
formula decision4 = msgTo4 & !m4 & ii!=4 ;
module crowds
s: [-1..5] init -1;
ii: [0..Nh] init 0;
i: [0..N] init 0;
f: [0..N] init 0;
[initiate] (s=-1) -> 1/Nh: (f'=1) & (i'=1) & (s'=0) & (ii'=1)
+ 1/Nh: (f'=2) & (i'=2) & (s'=0) & (ii'=2);
[s1] s=0 & ii=1 & i=1 -> 1/N : (i'=1) & (s'=1) + 1/N : (i'=2) & (s'=1)
+ 1/N : (i'=3) & (s'=1) + 1/N : (i'=4) & (s'=1) ;
[r1] msgTo1 & ii=1 -> 1/N : (i'=1) & (f'=i) & (s'=1)
+ 1/N : (i'=2) & (f'=i) & (s'=1)
+ 1/N : (i'=3) & (f'=i) & (s'=1)
+ 1/N : (i'=4) & (f'=i) & (s'=1);
[c1] decision1 -> x1: (f'=i) & (s'=2)
+ (1-x1):(i'=0) & (f'=0) & (ii'=0) & (s'=-1) ;
[r1] i=1 & s=2 & (ii!=1) & !m1 -> PF*1/N: (i'=1) & (s'=4) & (f'=i)
+ PF*1/N: (i'=2) & (s'=4) & (f'=i)
+ PF*1/N: (i'=3) & (s'=4) & (f'=i)
+ PF*1/N: (i'=4) & (s'=4) & (f'=i)
+ 1-PF: (s'=5) & (i'=0) & (f'=0) & (ii'=0);
[] msgTo1 & m1 -> (s'=5) & (i'=0) & (f'=i);
[s2] s=0 & ii=2 & i=2 -> 1/N : (i'=1) & (s'=1) + 1/N : (i'=2) & (s'=1)
+ 1/N : (i'=3) & (s'=1) + 1/N : (i'=4) & (s'=1) ;
[r2] msgTo2 & ii=2 -> 1/N : (i'=1) & (f'=i) & (s'=1)
+ 1/N : (i'=2) & (f'=i) & (s'=1)
+ 1/N : (i'=3) & (f'=i) & (s'=1)
+ 1/N : (i'=4) & (f'=i) & (s'=1);
[c2] decision2 -> x2: (f'=i) & (s'=2)
+ (1-x2):(i'=0) & (f'=0) & (ii'=0) & (s'=-1);
[r2] i=2 & s=2 & (ii!=2) & !m2 -> PF*1/N: (i'=1) & (s'=4) & (f'=i)
+ PF*1/N: (i'=2) & (s'=4) & (f'=i)
+ PF*1/N: (i'=3) & (s'=4) & (f'=i)
+ PF*1/N: (i'=4) & (s'=4) & (f'=i)
+ 1-PF: (s'=5) & (i'=0) & (f'=0) & (ii'=0);
[] msgTo2 & m2 -> (s'=5) & (i'=0) & (f'=0) & (ii'=0);
[s3] s=0 & ii=3 & i=3 -> 1/N : (i'=1) & (s'=1) + 1/N : (i'=2) & (s'=1)
+ 1/N : (i'=3) & (s'=1) + 1/N : (i'=4) & (s'=1) ;
[r3] msgTo3 & ii=3 -> 1/N : (i'=1) & (f'=i) & (s'=1)
+ 1/N : (i'=2) & (f'=i) & (s'=1)
+ 1/N : (i'=3) & (f'=i) & (s'=1)
+ 1/N : (i'=4) & (f'=i) & (s'=1);
[c3] decision3 -> x3: (f'=i) & (s'=2)
+ (1-x3):(i'=0) & (f'=0) & (ii'=0) & (s'=-1) ;
[r3] i=3 & s=2 & (ii!=3) & !m3 -> PF*1/N: (i'=1) & (s'=4) & (f'=i)
+ PF*1/N: (i'=2) & (s'=4) & (f'=i)
+ PF*1/N: (i'=3) & (s'=4) & (f'=i)
+ PF*1/N: (i'=4) & (s'=4) & (f'=i)
+ 1-PF: (s'=5) & (i'=0) & (f'=0) & (ii'=0);
[] msgTo3 & m3 -> (s'=5) & (i'=0) & (f'=0) & (ii'=0);
[s4] s=0 & ii=4 & i=4 -> 1/N : (i'=1) & (s'=1) + 1/N : (i'=2) & (s'=1)
+ 1/N : (i'=3) & (s'=1) + 1/N : (i'=4) & (s'=1) ;
[r4] msgTo4 & ii=4 -> 1/N : (i'=1) & (f'=i) & (s'=1)
+ 1/N : (i'=2) & (f'=i) & (s'=1)
+ 1/N : (i'=3) & (f'=i) & (s'=1)
+ 1/N : (i'=4) & (f'=i) & (s'=1);
[c4] decision4 -> x4: (f'=i) & (s'=2)
+ (1-x4):(i'=0) & (f'=0) & (ii'=0) & (s'=-1) ;
[r4] i=4 & s=2 & (ii!=4) & !m4 -> PF*1/N: (i'=1) & (s'=4) & (f'=i)
+ PF*1/N: (i'=2) & (s'=4) & (f'=i)
+ PF*1/N: (i'=3) & (s'=4) & (f'=i)
+ PF*1/N: (i'=4) & (s'=4) & (f'=i)
+ 1-PF: (s'=5) & (i'=0) & (f'=0) & (ii'=0);
[] msgTo4 & m4 -> (s'=5) & (i'=0) & (f'=0) & (ii'=0);
endmodule
rewards "rew1"
[s1] true : 1;
[r1] true : 2;
endrewards
rewards "rew2"
[s2] true : 2;
[r2] true : 3;
endrewards