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

// pomdp model
pomdp

// observable variables (for crypt5)
// 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, coin5, m, s1, s2, s3, s4, s5, guess, correct, agree1, agree2, agree3, agree4, agree5
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;

module master
	
	m : [0..1]; // local state (has chosen who pays)
	pay : [1..4]; // who actually pays
	
	// randomly choose who pays
	[] m=0 -> 1/4 : (m'=1) & (pay'=1) + 1/4 : (m'=1) & (pay'=2) + 1/4 : (m'=1) & (pay'=3) + 1/4 : (m'=1) & (pay'=4);
	
	// 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
	
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

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

endmodule