// 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