// simple anonymity example // 3 players, 2 honest dtmc //total number of players const int N=3; //total number of honest players const int Nh=2; // Probability that a crowd member to coorporate or be selfish const double x1 ; const double x2 ; module eg s: [0..3] init 0; f: [0..3] init 0; //from [s0] s=0 -> x1: (f'=0) & (s'=1) + (1/2-x1): (f'=0) & (s'=2) + 1/2 : (f'=0) & (s'=3) ; [s1] s=1 -> 5/8: (f'=1) & (s'=0) + x2: (f'=1) & (s'=2) + (3/8-x2) : (f'=1) & (s'=3) ; [s2] s=2 -> (f'=2) & (s'=3); [] s=3 -> true; endmodule rewards "rew0" [s0] true : 1; endrewards rewards "rew1" [s1] true : 2; endrewards