// POLYNOMIAL RANDOMIZED CONSENSUS [AH90]
// three processes and four rounds
// system model
// gxn/dxp 01/10/09

mdp

const int MAX=4;

// need to turn these into local copies later so the reading phase is complete?
formula leaders_agree1 = (p1=1 | r1<max(r1,r2,r3)) & (p2=1 | r2<max(r1,r2,r3)) & (p3=1 | r3<max(r1,r2,r3));
formula leaders_agree2 = (p1=2 | r1<max(r1,r2,r3)) & (p2=2 | r2<max(r1,r2,r3)) & (p3=2 | r3<max(r1,r2,r3));

formula decide1 = leaders_agree1 & (p1=1 | r1<max(r1,r2,r3)-1) & (p2=1 | r2<max(r1,r2,r3)-1) & (p3=1 | r3<max(r1,r2,r3)-1);
formula decide2 = leaders_agree2 & (p1=2 | r1<max(r1,r2,r3)-1) & (p2=2 | r2<max(r1,r2,r3)-1) & (p3=2 | r3<max(r1,r2,r3)-1);

module process1

	s1 : [0..5]; // local state
	// 0 initialise/read registers
	// 1 finish reading registers (make a decision)
	// 1 warn of change
	// 2 enter shared coin protocol
	// 4 finished
	// 5 error (reached max round and cannot decide)
	r1 : [0..MAX]; // round of the process
	p1 : [0..2]; // preference (0 corresponds to null)

	// nondeterministic choice as to initial preference
	[] s1=0 & r1=0 -> (p1'=1) & (r1'=1);
	[] s1=0 & r1=0 -> (p1'=2) & (r1'=1);
	
	// read registers (currently does nothing because read vs from other processes
	[] s1=0 & r1>0 & r1<=MAX -> (s1'=1);
	// maxke a decision
	[] s1=1 & decide1 -> (s1'=4) & (p1'=1);
	[] s1=1 & decide2 -> (s1'=4) & (p1'=2);
	[] s1=1 & r1<MAX & leaders_agree1 & !decide1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
	[] s1=1 & r1<MAX & leaders_agree2 & !decide2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
	[] s1=1 & r1<MAX & !(leaders_agree1 | leaders_agree2) -> (s1'=2) & (p1'=0);
	[] s1=1 & r1=MAX & !(decide1 | decide2) -> (s1'=5); // run out of rounds so error
	// enter the coin procotol for the current round
	[coin1_s1_start] s1=2 & r1=1 -> (s1'=3);
	[coin2_s1_start] s1=2 & r1=2 -> (s1'=3);
	[coin3_s1_start] s1=2 & r1=3 -> (s1'=3);
	// get response from the coin protocol
	[coin1_s1_p1] s1=3 & r1=1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
	[coin1_s1_p2] s1=3 & r1=1 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
	[coin2_s1_p1] s1=3 & r1=2 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
	[coin2_s1_p2] s1=3 & r1=2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
	[coin3_s1_end] s1=3 & r1=3 -> (s1'=0) & (r1'=r1+1);
	// done so loop
	[done] s1>=4 -> true; 

endmodule

module process2 = process1[ s1=s2,
											p1=p2,p2=p3,p3=p1,
											r1=r2,r2=r3,r3=r1,
											coin1_s1_start=coin1_s2_start,
											coin2_s1_start=coin2_s2_start,
											coin3_s1_start=coin3_s2_start,
											coin1_s1_p1=coin1_s2_p1,
											coin2_s1_p1=coin2_s2_p1,
											coin1_s1_p2=coin1_s2_p2,
											coin2_s1_p2=coin2_s2_p2,
											coin3_s1_end=coin3_s2_end ]
endmodule

module process3 = process1[ s1=s3,
											p1=p3,p2=p1,p3=p2,
											r1=r3,r2=r1,r3=r2,
											coin1_s1_start=coin1_s3_start,
											coin2_s1_start=coin2_s3_start,
											coin3_s1_start=coin3_s3_start,
											coin1_s1_p1=coin1_s3_p1,
											coin2_s1_p1=coin2_s3_p1,
											coin1_s1_p2=coin1_s3_p2,
											coin2_s1_p2=coin2_s3_p2,
											coin3_s1_end=coin3_s3_end ]
endmodule


// constants for the shared coin
const int N=3;
const int K;
const int range = 2*(K+1)*N;
const int counter_init = (K+1)*N;
const int left = N;
const int right= 2*(K+1)*N -N;

// shared coins for round 1 and 2
global counter1 : [0..range] init counter_init;
global counter2 : [0..range] init counter_init;

module r1_coin1
	
	// when protocol is initialised
	r1_start1 : bool;

	// program counter
	r1_pc1 : [0..3];
	// 0 - flip
	// 1 - write 
	// 2 - check
	// 3 - finished
	
	// local coin
	r1_coin1 : [0..1];	

	// start coin protocol for process 1
	[coin1_s1_start] !r1_start1 -> (r1_start1'=true);
	// flip coin
	[] r1_start1 & (r1_pc1=0)  -> 0.5 : (r1_coin1'=0) & (r1_pc1'=1) + 0.5 : (r1_coin1'=1) & (r1_pc1'=1);
	// write tails -1  (reset coin to add regularity)
	[] r1_start1 & (r1_pc1=1) & (r1_coin1=0) & (counter1>0) -> (counter1'=counter1-1) & (r1_pc1'=2) & (r1_coin1'=0);
	// write heads +1 (reset coin to add regularity)
	[] r1_start1 & (r1_pc1=1) & (r1_coin1=1) & (counter1<range) -> (counter1'=counter1+1) & (r1_pc1'=2) & (r1_coin1'=0);
	// check
	// decide tails
	[coin1_s1_p1] r1_start1 & (r1_pc1=2) & (counter1<=left) -> (r1_pc1'=3) & (r1_coin1'=0);
	//decide heads
	[coin1_s1_p2] r1_start1 & (r1_pc1=2) & (counter1>=right) -> (r1_pc1'=3) & (r1_coin1'=1);
	// flip again
	[] r1_start1 & (r1_pc1=2) & (counter1>left) & (counter1<right) -> (r1_pc1'=0);

endmodule

module r1_coin2 = r1_coin1[r1_start1=r1_start2,r1_pc1=r1_pc2,r1_coin1=r1_coin2,coin1_s1_start=coin1_s2_start,coin1_s1_p1=coin1_s2_p1,coin1_s1_p2=coin1_s2_p2,counter1=counter1] endmodule
module r1_coin3 = r1_coin1[r1_start1=r1_start3,r1_pc1=r1_pc3,r1_coin1=r1_coin3,coin1_s1_start=coin1_s3_start,coin1_s1_p1=coin1_s3_p1,coin1_s1_p2=coin1_s3_p2,counter1=counter1] endmodule
module r2_coin1 = r1_coin1[r1_start1=r2_start1,r1_pc1=r2_pc1,r1_coin1=r2_coin1,coin1_s1_start=coin2_s1_start,coin1_s1_p1=coin2_s1_p1,coin1_s1_p2=coin2_s1_p2,counter1=counter2] endmodule
module r2_coin2 = r1_coin1[r1_start1=r2_start2,r1_pc1=r2_pc2,r1_coin1=r2_coin2,coin1_s1_start=coin2_s2_start,coin1_s1_p1=coin2_s2_p1,coin1_s1_p2=coin2_s2_p2,counter1=counter2] endmodule
module r2_coin3 = r1_coin1[r1_start1=r2_start3,r1_pc1=r2_pc3,r1_coin1=r2_coin3,coin1_s1_start=coin2_s3_start,coin1_s1_p1=coin2_s3_p1,coin1_s1_p2=coin2_s3_p2,counter1=counter2] endmodule

label "agree1" = s1=4 & s2=4 & s3=4 & p1=1 & p2=1 & p3=1;
label "agree2" = s1=4 & s2=4 & s3=4 & p1=2 & p2=2 & p3=2;

// expected number of steps
rewards "steps"
	[] true : 1;

	[coin1_s1_start] true : 1;
	[coin1_s2_start] true : 1;
	[coin1_s3_start] true : 1;
	[coin1_s1_p1] true : 1;
	[coin1_s1_p2] true : 1;
	[coin1_s2_p1] true : 1;
	[coin1_s2_p2] true : 1;
	[coin1_s3_p1] true : 1;
	[coin1_s3_p2] true : 1;

	[coin2_s1_start] true : 1;
	[coin2_s2_start] true : 1;
	[coin2_s3_start] true : 1;
	[coin2_s1_p1] true : 1;
	[coin2_s1_p2] true : 1;
	[coin2_s2_p1] true : 1;
	[coin2_s2_p2] true : 1;
	[coin2_s3_p1] true : 1;
	[coin2_s3_p2] true : 1;

	[coin3_s1_start] true : 1;
	[coin3_s2_start] true : 1;
	[coin3_s3_start] true : 1;
	[coin3_s1_end] true : 1;
	[coin3_s2_end] true : 1;
	[coin3_s3_end] true : 1;

endrewards