// herman's self stabilising algorithm [Her90]
// gxn/dxp 13/07/02

// the procotol is synchronous with no nondeterminism (a DTMC)
dtmc

// module for process 1
module process1

	x1 : [0..1] init 1;
	
	[step] (x1=x7) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
	[step] !(x1=x7) -> (x1'=x7);
	
endmodule

// add further processes through renaming
module process2 = process1[x1=x2, x7=x1 ] endmodule
module process3 = process1[x1=x3, x7=x2 ] endmodule
module process4 = process1[x1=x4, x7=x3 ] endmodule
module process5 = process1[x1=x5, x7=x4 ] endmodule
module process6 = process1[x1=x6, x7=x5 ] endmodule
module process7 = process1[x1=x7, x7=x6 ] endmodule

// formula, for use in properties: number of tokens
// (i.e. number of processes that have the same value as the process to their left)
formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x5?1:0)+(x5=x6?1:0)+(x6=x7?1:0)+(x7=x1?1:0);

// rewards (to calculate expected number of steps)
rewards "steps"
	true : 1;
endrewards