// PRISM model of the randomised sequential Prisoner's dilemma problem:
// - The game consists of three players and a scheduler
// - Scheduler determines the order in which players have to choose whether to cooperate or defect
// - After the players have made their choices the pair of them is selected uniformly at random
// - The outcome of the prisoners dilemma is the combination of choices of the selected pair
//
// Author: Aistis Simaitis
// Last modified: 3/10/2012

smg

player sched scheduler endplayer
player ag1 agent1, [fin1] endplayer
player ag2 agent2, [fin2] endplayer
player ag3 agent3, [fin3] endplayer

module scheduler
	turn : [0..3] init 0;
	outcome : [0..3] init 0;

	[] turn=0 & s1=0 -> (turn'=1);
	[] turn=0 & s2=0 -> (turn'=2);
	[] turn=0 & s3=0 -> (turn'=3);
	
	[fin1] true -> (turn'=0);
	[fin2] true -> (turn'=0);
	[fin3] true -> (turn'=0);

	[] s1>0 & s2>0 & s3>0 & outcome=0 -> 1/3 : (outcome'=1)  // agents 1 and 2 chosen
                                           + 1/3 : (outcome'=2)  // agents 1 and 3 chosen
                                           + 1/3 : (outcome'=3); // agents 2 and 3 chosen

	[] outcome>0 -> (turn'=2);

endmodule

module agent1
	s1 : [0..2]; // 1 - cooperate, 2 - defect
	[fin1] turn=turn1 & s1=0 -> (s1'=1);
	[fin1] turn=turn1 & s1=0 -> (s1'=2);
endmodule

module agent2=agent1[s1=s2,turn1=turn2,fin1=fin2] endmodule
module agent3=agent1[s1=s3,turn1=turn3,fin1=fin3] endmodule

const turn1=1; 
const turn2=2;
const turn3=3;

formula target = outcome>0 & turn!=0;
formula cooperating = (outcome=1&(s1=1&s2=1)) | (outcome=2&(s1=1&s3=1)) | (outcome=3&(s2=1&s3=1));
formula defecting = (outcome=1&(s1=2&s2=2)) | (outcome=2&(s1=2&s3=2)) | (outcome=3&(s2=2&s3=2));


rewards "Coalition1"
	outcome=1 : (s1=1&s2=1) ?  4 : ((s1=1&s2=2) ? 0 : ((s1=2&s2=1) ? 7 : ((s1=2&s2=2) ? 2 : 0)));
	outcome=2 : (s1=1&s3=1) ?  4 : ((s1=1&s3=2) ? 0 : ((s1=2&s3=1) ? 7 : ((s1=2&s3=2) ? 2 : 0))); 
	outcome=3 : 0;
endrewards
rewards "Coalition12"
	outcome=1 : (s1=1&s2=1) ?  2*4 : ((s1=1&s2=2) ? 0 : ((s1=2&s2=1) ? 2*7 : ((s1=2&s2=2) ? 2*2 : 0)));
	outcome=2 : (s1=1&s3=1) ?  4 : ((s1=1&s3=2) ? 0 : ((s1=2&s3=1) ? 7 : ((s1=2&s3=2) ? 2 : 0))); 
	outcome=3 : (s2=1&s3=1) ?  4 : ((s2=1&s3=2) ? 0 : ((s2=2&s3=1) ? 7 : ((s2=2&s3=2) ? 2 : 0)));
endrewards
rewards "Coalition123"
	outcome=1 : (s1=1&s2=1) ?  2*4 : ((s1=1&s2=2) ? 0 : ((s1=2&s2=1) ? 2*7 : ((s1=2&s2=2) ? 2*2 : 0)));
	outcome=2 : (s1=1&s3=1) ?  2*4 : ((s1=1&s3=2) ? 0 : ((s1=2&s3=1) ? 2*7 : ((s1=2&s3=2) ? 2*2 : 0))); 
	outcome=3 : (s2=1&s3=1) ?  2*4 : ((s2=1&s3=2) ? 0 : ((s2=2&s3=1) ? 2*7 : ((s2=2&s3=2) ? 2*2 : 0)));
endrewards