// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
// 2 processes
// gxn/dxp 20/11/00

mdp

// CONSTANTS
const int N=2; // number of processes
const int K; // parameter of the protoc
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 coin
global counter : [0..range] init counter_init;

module process1
	
	start1 : [0..1];
	
	// program counter
	pc1 : [0..3];
	// 0 - flip
	// 1 - write 
	// 2 - check
	// 3 - finished
	
	// local coin
	coin1 : [0..1];	

	// wait to be initialised
	[wait1] start1=0 -> (start1'=0);
	// get called
	[coin_s1_start] start1=0 -> (start1'=1);
	
	// flip coin
	[] start1=1 & pc1=0  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
	// write tails -1  (reset coin to add regularity)
	[] start1=1 &  pc1=1  &  coin1=0  &  counter>0  -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
	// write heads +1 (reset coin to add regularity)
	[] start1=1 & pc1=1 & coin1=1 & counter<range -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
	// check
	// decide tails
	[coin_s1_p1] start1=1 & pc1=2 & counter<=left -> (pc1'=3) & (coin1'=0);
	//decide heads
	[coin_s1_p1] start1=1 & pc1=2 & counter>=right -> (pc1'=3) & (coin1'=1);
	// flip again
	[] start1=1 & pc1=2 & counter>left & counter<right -> (pc1'=0);
	// loop when finished
	[done] start1=1 & pc1=3 -> (pc1'=3);

endmodule

// construct remaining processes through renaming
module process2 = process1[pc1=pc2,
                                              coin1=coin2,
                                              start1=start2,  coin_s1_start=coin_s2_start,coin_s1_p1=coin_s2_p1,
                                              coin_s1_p2=coin_s2_p2,
                                              wait1=wait2]
endmodule

// reward structure only over independent coin transitions
rewards "coin_moves"
	[] true : 1;
endrewards