// Israeli-Jalfon algorithm
// dxp/gxn 10/06/02
// token of size 9

nondeterministic

// variables to represent whether a process has a token or not
// note they are global because they can be updated by other processes
global q1  : [0..1];
global q2  : [0..1];
global q3  : [0..1];
global q4  : [0..1];
global q5  : [0..1];
global q6  : [0..1];
global q7  : [0..1];
global q8  : [0..1];
global q9  : [0..1];

// module of process 1
module process1
	
	[] (q1=1) -> 0.5 : (q1'=0) & (q9'=1) + 0.5 : (q1'=0) & (q2'=1);
	
endmodule

// add further processes through renaming
module process2 =process1[q1=q2 ,q2=q3, q9=q1] endmodule
module process3 =process1[q1=q3 ,q2=q4, q9=q2] endmodule
module process4 =process1[q1=q4 ,q2=q5, q9=q3] endmodule
module process5 =process1[q1=q5 ,q2=q6, q9=q4] endmodule
module process6 =process1[q1=q6 ,q2=q7, q9=q5] endmodule
module process7 =process1[q1=q7 ,q2=q8, q9=q6] endmodule
module process8 =process1[q1=q8 ,q2=q9, q9=q7] endmodule
module process9 =process1[q1=q9 ,q2=q1, q9=q8] endmodule

// cost - 1 in each state (expected steps)
rewards
	
	true : 1;
	
endrewards

// initial states (at least one token)
init
	
	q1+q2+q3+q4+q5+q6+q7+q8+q9>=1
	
endinit