// crowds protocol
// 4 players: 2 honest + 2 malicious

dtmc

//total number of players
const int N=4; 
//total number of honest players
const int Nh=2;

//probability of continue to relay, 1-PF probability of forwarding to the dest
const double PF=0.5; 

// Probability that a crowd member to coorporate or be selfish
const double x1 ;
const double x2 ;
const double x3 = 0;
const double x4 = 0;


// factor weights
const double ra=3;
const double rc=1;

//malicious or not
const bool m1 = false;
const bool m2 = false;
const bool m3 = true;
const bool m4 = true;


// formulae 
// there is a message sent to (initiator) player 1
formula msgTo1 = i=1 & (s=1 | s=4);

// there is a message sent to (honest) player 2
formula msgTo2 = i=2 & (s=1 | s=4);

// there is a message sent to (malicious) player 3
formula msgTo3 = i=3 & (s=1 | s=4);

// there is a message sent to (malicious) player 4
formula msgTo4 = i=4 & (s=1 | s=4);

// make decisions: to corporate or not
formula decision1 = msgTo1 & !m1 & ii!=1 ;
formula decision2 = msgTo2 & !m2 & ii!=2 ;
formula decision3 = msgTo3 & !m3 & ii!=3 ;
formula decision4 = msgTo4 & !m4 & ii!=4 ;

//formula violateAnonymity = (f=1) & (i=4) & (ii=1);


module crowds

	//status: 0-initiator picked up 1-sent 2-cor 3-notcor/discarded 4-relayed 5-dest
	s: [-1..5] init -1; //status: 0-initiator picked up 1-sent 2-cor 3-notcor 4-relayed 5-dest

        //who is the initiator?
        ii: [0..Nh] init 0;


	i: [0..N] init 0; //send to
	f: [0..N] init 0; //from

	//pick up an initiator
        [initiate] (s=-1) ->  1/Nh: (f'=1) & (i'=1) & (s'=0) & (ii'=1)
                              + 1/Nh: (f'=2) & (i'=2) & (s'=0) & (ii'=2);

        /////////////////////////////
        //if i=1 is an initiator

        //start to send out a message
	[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) ; 
	//to relay a message as an initiator
	[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); 

        // if i=1 is an honest relayer- relay to each other
        [c1] decision1 -> x1: (f'=i) & (s'=2)
                          + (1-x1):(i'=0) & (f'=0) & (ii'=0) & (s'=-1) ;
	//to relay a message as an honest user
        [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);

        // if i=1 is a malicious member - send to the dest directly
        [] msgTo1 & m1 -> (s'=5) & (i'=0) & (f'=i);


        /////////////////////////////
        //if i=2 is an initiator

        //start to send out a message
        [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) ;
        //to relay a message as an initiator
        [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);


        // if i=2 is an honest relayer- relay to each other
        [c2] decision2 -> x2: (f'=i) & (s'=2)
                          + (1-x2):(i'=0) & (f'=0) & (ii'=0) & (s'=-1);
        //to relay a message as an honest user
        [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);

        // if i=2 is a malicious member - send to the dest directly
        [] msgTo2 & m2 -> (s'=5) & (i'=0) & (f'=0) & (ii'=0);


        /////////////////////////////
        //if i=3 is an initiator

        //start to send out a message
        [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) ;
        //to relay a message as an initiator
        [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);


        // if i=3 is an honest relayer- relay to each other
        [c3] decision3 -> x3: (f'=i) & (s'=2)
                          + (1-x3):(i'=0) & (f'=0) & (ii'=0) & (s'=-1) ;
        //to relay a message as an honest user
        [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);

        // if i=3 is a malicious member - send to the dest directly
        [] msgTo3 & m3 -> (s'=5) & (i'=0) & (f'=0) & (ii'=0);

        /////////////////////////////
        //if i=4 is an initiator
        //start to send out a message
        [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) ;
        //to relay a message as an initiator
        [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);


        // if i=4 is an honest relayer- relay to each other
        [c4] decision4 -> x4: (f'=i) & (s'=2)
                          + (1-x4):(i'=0) & (f'=0) & (ii'=0) & (s'=-1) ;
        //to relay a message as an honest user
        [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);

        // if i=4 is a malicious member - send to the dest directly
        [] 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