// dining cryptographers
// gxn 27/01/16

// pomdp model
pomdp

// observable variables (for crypt6)
// the announcements of all cryptographers 
// only its own coin and the coin of its left neighbour
// if it guesses correctly (this is the target so needs to be observable)
// also local states of modules this only indicates:
// - if a cryptographer has announced
// - if the master has made its choice
observables
	coin1, coin6, m, s1, s2, s3, s4, s5, s6, guess, correct, agree1, agree2, agree3, agree4, agree5, agree6
endobservables

// constants used in renaming
const int p1=1;
const int p2=2;
const int p3=3;
const int p4=4;
const int p5=5;
const int p6=6;

module master
	
	m : [0..1]; // local state (has chosen who pays)
	pay : [1..6]; // who actually pays
	
	// randomly choose who pays
	[] m=0 -> 1/5 : (m'=1) & (pay'=1) + 1/5 : (m'=1) & (pay'=2) + 1/5 : (m'=1) & (pay'=3) + 1/5 : (m'=1) & (pay'=4) + 1/5 : (m'=1) & (pay'=5);
	
	// test cases
	//[] m=0 -> (m'=1); // master pays
	//[] m=0 -> (m'=1) & (pay'=1); // crypt 1 pays
	//[] m=0 -> (m'=1) & (pay'=2); // crypt 2 pays
	//[] m=0 -> (m'=1) & (pay'=3); // crypt 3 pays
	//[] m=0 -> (m'=1) & (pay'=4); // crypt 4 pays
	//[] m=0 -> (m'=1) & (pay'=5); // crypt 5 pays
	
endmodule

module crypt1
	
	coin1 : [0..2]; // value of coin
	s1 : [0..1]; // local state (has announced yet)
	agree1 : [0..1]; // agree or not
	
	// flip coin and share values
	[flip] m=1 & coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
	
	// make choice (once relevant coins have been flipped)
	// does not pay
	[choose1] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay!=p1) -> (s1'=1) & (agree1'=1);
	[choose1] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
	// pays
	[choose1] s1=0 & coin1>0 & coin2>0 & coin1=coin2 & (pay=p1) -> (s1'=1);
	[choose1] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1) -> (s1'=1) & (agree1'=1);
	// when everyone has announced
	[done] s1=1 -> true;

endmodule

// construct further cryptographers through renaming
module crypt2 =crypt1[coin1=coin2, s1=s2, p1=p2, agree1=agree2, coin2=coin3, choose1=choose2 ] endmodule
module crypt3 =crypt1[coin1=coin3, s1=s3, p1=p3, agree1=agree3, coin2=coin4, choose1=choose3 ] endmodule
module crypt4 =crypt1[coin1=coin4, s1=s4, p1=p4, agree1=agree4, coin2=coin5, choose1=choose4 ] endmodule
module crypt5 =crypt1[coin1=coin5, s1=s5, p1=p5, agree1=agree5, coin2=coin6, choose1=choose5 ] endmodule

// the cryptographer that guesses who pays
module crypt6
	
	coin6 : [0..2];
	s6 : [0..2];
	agree6 : [0..1];
	guess : [0..5];
	correct : [0..1];
	
	// flip coin
	[flip] m=1 & coin6=0 -> 0.5 : (coin6'=1) + 0.5 : (coin6'=2);
	
	// make choice (once relevant coins have been flipped)
	// assume does not pay
	[choose6] s6=0 & coin6>0 & coin1>0 & coin6=coin1 -> (s6'=1) & (agree6'=1);
	[choose6] s6=0 & coin6>0 & coin1>0 & !(coin6=coin1) -> (s6'=1);
	// pays
	[choose6] s6=0 & coin6>0 & coin1>0 & coin6=coin1 & (pay=p6) -> (s6'=1);
	[choose6] s6=0 & coin6>0 & coin1>0 & !(coin6=coin1) & (pay=p6) -> (s6'=1) & (agree6'=1);
	
	// after everyone has announced guess who payed
	[done] s6=1 -> (s6'=2);
	[guess1] s6=2 & guess=0 -> (guess'=1);
	[guess2] s6=2 & guess=0 -> (guess'=2);
	[guess3] s6=2 & guess=0 -> (guess'=3);
	[guess4] s6=2 & guess=0 -> (guess'=4);
	[guess5] s6=2 & guess=0 -> (guess'=5);
	
	// check whether guessed correctly
	[check] s6=2 & guess>0 & guess=pay -> (correct'=1);
	[check] s6=2 & guess>0 & !(guess=pay) -> true;

endmodule