// secret sharing protocol
// J. Halpern, V. Teague
// Rational secret sharing and multiparty computation: Extended abstract. 
// Proc. STOC'04. pp. 623–632, ACM, 2004

// two rational agents and one altruistic agent

csg

// constants
const double alpha;
const double uall = 1;
const double utwo = 1.5;
const double uone = 2;

// formulae
// agents send messages

formula inm1=c3p;
formula inm2=c1p;
formula inm3=c2p;

formula inp1=c2m;
formula inp2=c3m;
formula inp3=c1m;

formula ip1=mod(inp2+c2,2);
formula ip2=mod(inp3+c3,2);
formula ip3=mod(inp1+c1,2);

formula p1 = mod(inm1+mod(ip1+c1,2),2);
formula p2 = mod(inm2+mod(ip2+c2,2),2);
formula p3 = mod(inm3+mod(ip3+c3,2),2);

// number of secrets sent
formula n = ps1+ps2+ps3; 
// number of secrets each agent has
formula n1 = 1+ps2+ps3;
formula n2 = 1+ps1+ps3;
formula n3 = 1+ps1+ps2;

player agent1
	agent1
endplayer

player agent2
	agent2
endplayer

player agent3
	agent3
endplayer

const rmax;

module steps
	s : [0..6] init 0; 
	r : [0..rmax+1] init 0;

	// step 0
	[] s=0 -> (s'=1); // rational agents decide if to cheat

	//step 1
	[] s=1 -> (s'=2); // random choices
	[] s=2 -> (s'=3); // send shared values or not
	// step 4
	[] s=3 -> (s'=4); // request new round or not
	[] s=4 & s1 & s2 & s3 -> (s'=0) & (r'=min(rmax,r+1)); //restarts
	[] s=4 & !(s1 & s2 & s3) & n=3 -> (s'=5); // stop and all have secret
	[] s=4 & !(s1 & s2 & s3) & n<3 -> (s'=6); // stop and not all have secret
	
	[] s>=5 -> true;
	
endmodule

module agent1 // rational
	c1 : [0..1];
	c1p : [0..1];
	c1m : [0..1];
	s1 : bool;
	ps1 : [0..1] init 0;
	cheat1 : [0..1];
	
	[c10] s=0 -> (cheat1'=0); // does not cheat in this round
	[c11] s=0 -> (cheat1'=1); // cheats in this round

	// internal computation
	[int1] s=1 -> alpha*1/2 : (c1'=1) & (c1p'=1) & (c1m'=mod(1+1,2))
			  + alpha*1/2 : (c1'=1) & (c1p'=0) & (c1m'=mod(1+0,2))
		  	  + (1-alpha)*1/2 : (c1'=0) & (c1p'=1) & (c1m'=mod(0+1,2))
		  	  + (1-alpha)*1/2 : (c1'=0) & (c1p'=0) & (c1m'=mod(0+0,2));

	//decides to send or not
	[s31a] s=2 & p1=1 & c1=1 & cheat1=0 -> (ps1'=1);
	[s31b] s=2 & !(p1=1 & c1=1) -> (ps1'=0);
	[s31c] s=2 & p1=1 & c1=1 & cheat1=1 -> (ps1'=0); // cheats

	// restart or stop
	[s41a] s=3 & ((p1=0 & n=0) | (p1=1 & n=1)) -> (s1'=true);
	[s41b] s=3 & !((p1=0 & n=0) | (p1=1 & n=1)) -> (s1'=false);
	
	//reset
	[s51a] s=4 -> (c1'=0) & (c1p'=0) & (c1m'=0) & (ps1'=0) & (s1'=false) & (cheat1'=0);
endmodule

module agent2 // altruistic
        c2 : [0..1];
        c2p : [0..1];
        c2m : [0..1];
        s2 : bool;
        ps2 : [0..1] init 0;

        [c2] s=0 -> true;

        // internal computation
        [int2] s=1 -> alpha*1/2 : (c2'=1) & (c2p'=1) & (c2m'=mod(1+1,2))
                          + alpha*1/2 : (c2'=1) & (c2p'=0) & (c2m'=mod(1+0,2))
                          + (1-alpha)*1/2 : (c2'=0) & (c2p'=1) & (c2m'=mod(0+1,2))
                          + (1-alpha)*1/2 : (c2'=0) & (c2p'=0) & (c2m'=mod(0+0,2));

        //decides to send or not
        [s32a] s=2 & p2=1 & c2=1 -> (ps2'=1);
        [s32b] s=2 & !(p2=1 & c2=1) -> (ps2'=0);

        // restart or stop
        [s42a] s=3 & ((p2=0 & n=0) | (p2=1 & n=1)) -> (s2'=true);
        [s42b] s=3 & !((p2=0 & n=0) | (p2=1 & n=1)) -> (s2'=false);

        //reset
        [s52a] s=4 -> (c2'=0) & (c2p'=0) & (c2m'=0) & (ps2'=0) & (s2'=false);
endmodule

module agent3 // rational
	c3 : [0..1];
	c3p : [0..1];
	c3m : [0..1];
	s3 : bool;
	ps3 : [0..1] init 0;
	cheat3 : [0..1];
	
	[c30] s=0 -> (cheat3'=0); // does not cheat in this round
	[c31] s=0 -> (cheat3'=1); // cheats in this round

	// internal computation
	[int3] s=1 -> alpha*1/2 : (c3'=1) & (c3p'=1) & (c3m'=mod(1+1,2))
			  + alpha*1/2 : (c3'=1) & (c3p'=0) & (c3m'=mod(1+0,2))
		  	  + (1-alpha)*1/2 : (c3'=0) & (c3p'=1) & (c3m'=mod(0+1,2))
		  	  + (1-alpha)*1/2 : (c3'=0) & (c3p'=0) & (c3m'=mod(0+0,2));

	//decides to send or not
	[s33a] s=2 & p3=1 & c3=1 & cheat3=0 -> (ps3'=1);
	[s33b] s=2 & !(p3=1 & c3=1) -> (ps3'=0);
	[s33c] s=2 & p3=1 & c3=1 & cheat3=1 -> (ps3'=0); // cheats

	// restart or stop
	[s43a] s=3 & ((p3=0 & n=0) | (p3=1 & n=1)) -> (s3'=true);
	[s43b] s=3 & !((p3=0 & n=0) | (p3=1 & n=1)) -> (s3'=false);
	
	//reset
	[s53a] s=4 -> (c3'=0) & (c3p'=0) & (c3m'=0) & (ps3'=0) & (s3'=false) & (cheat3'=0);
endmodule

// utility of player 1
rewards "r1"
	
	[] s=4 & !(s1 & s2 & s3) & n1=3 & n2=3 & n3=3 : uall;
	[] s=4 & !(s1 & s2 & s3) & n1=3 & n2=3 & n3<3 : utwo;
	[] s=4 & !(s1 & s2 & s3) & n1=3 & n2<3 & n3=3 : utwo;
	[] s=4 & !(s1 & s2 & s3) & n1=3 & n2<3 & n3<3 : uone;

endrewards

// utility of player 2
rewards "r2"
	
	[] s=4 & !(s1 & s2 & s3) & n2=3 & n1=3 & n3=3 : uall;
	[] s=4 & !(s1 & s2 & s3) & n2=3 & n1=3 & n3<3 : utwo;
	[] s=4 & !(s1 & s2 & s3) & n2=3 & n1<3 & n3=3 : utwo;
	[] s=4 & !(s1 & s2 & s3) & n2=3 & n1<3 & n3<3 : uone;

endrewards

// utility of player 3
rewards "r3"
	
	[] s=4 & !(s1 & s2 & s3) & n3=3 & n2=3 & n1=3 : uall;
	[] s=4 & !(s1 & s2 & s3) & n3=3 & n2=3 & n1<3 : utwo;
	[] s=4 & !(s1 & s2 & s3) & n3=3 & n2<3 & n1=3 : utwo;
	[] s=4 & !(s1 & s2 & s3) & n3=3 & n2<3 & n1<3 : uone;

endrewards