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

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