// Israeli-Jalfon algorithm
// dxp/gxn 10/06/02

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];
global q10 : [0..1];
global q11 : [0..1];
global q12 : [0..1];
global q13 : [0..1];
global q14 : [0..1];
global q15 : [0..1];
global q16 : [0..1];
global q17 : [0..1];
global q18 : [0..1];
global q19 : [0..1];
global q20 : [0..1];

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

// add further processes through renaming
module process2 =process1[s1=s2 ,q1=q2 ,q2=q3 ,q20=q1 ] endmodule
module process3 =process1[s1=s3 ,q1=q3 ,q2=q4 ,q20=q2 ] endmodule
module process4 =process1[s1=s4 ,q1=q4 ,q2=q5 ,q20=q3 ] endmodule
module process5 =process1[s1=s5 ,q1=q5 ,q2=q6 ,q20=q4 ] endmodule
module process6 =process1[s1=s6 ,q1=q6 ,q2=q7 ,q20=q5 ] endmodule
module process7 =process1[s1=s7 ,q1=q7 ,q2=q8 ,q20=q6 ] endmodule
module process8 =process1[s1=s8 ,q1=q8 ,q2=q9 ,q20=q7 ] endmodule
module process9 =process1[s1=s9 ,q1=q9 ,q2=q10,q20=q8 ] endmodule
module process10=process1[s1=s10,q1=q10,q2=q11,q20=q9 ] endmodule
module process11=process1[s1=s11,q1=q11,q2=q12,q20=q10] endmodule
module process12=process1[s1=s12,q1=q12,q2=q13,q20=q11] endmodule
module process13=process1[s1=s13,q1=q13,q2=q14,q20=q12] endmodule
module process14=process1[s1=s14,q1=q14,q2=q15,q20=q13] endmodule
module process15=process1[s1=s15,q1=q15,q2=q16,q20=q14] endmodule
module process16=process1[s1=s16,q1=q16,q2=q17,q20=q15] endmodule
module process17=process1[s1=s17,q1=q17,q2=q18,q20=q16] endmodule
module process18=process1[s1=s18,q1=q18,q2=q19,q20=q17] endmodule
module process19=process1[s1=s19,q1=q19,q2=q20,q20=q18] endmodule
module process20=process1[s1=s20,q1=q20,q2=q1 ,q20=q19] 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+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20>=1
	
endinit