updated ij (labels)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@490 bbc10eb1-c90d-0410-af57-cb519fbb1720
18 years ago · 1e48f16ab1
40 changed files with 93 additions and 310 deletions
--- a/prism-examples/self-stabilisation/israeli-jalfon/auto
+++ b/prism-examples/self-stabilisation/israeli-jalfon/auto
@ -1,7 +1,7 @@
 #!/bin/csh

-prism ij3.nm ij3.pctl -prop 1 -const k=0
-prism ij3.nm ij3.pctl -prop 2 -const k=1:1:100 -m
-prism ij3.nm ij3.pctl -prop 3 -const k=0 -m
-prism ij3.nm ij3.pctl -prop 4 -const k=1:1:3 -m
-prism ij3.nm ij3.pctl -prop 5 -const k=1:1:3 -m
+prism ij3.nm ij.pctl -prop 1 -const k=0,K=0
+prism ij3.nm ij.pctl -prop 2 -const k=0,K=0 -m
+prism ij3.nm ij.pctl -prop 3 -const k=1:1:3,K=0 -m
+prism ij3.nm ij.pctl -prop 4 -const k=1:1:3,K=0 -m
+prism ij3.nm ij.pctl -prop 5 -const k=0,K=1:1:100 -m
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl
@ -0,0 +1,19 @@
+const int k; // number of tokens
+const int K; // number of steps
+
+// labels
+label "k_tokens" = num_tokens=k; // configurations with k tokens
+label "stable" = num_tokens=1;   // stable configurations (1 token)
+
+// From any configuration, a stable configuration is reached with probability 1
+"init" => P>=1 [ F "stable" ]
+
+// Maximum expected time to reach a stable configuration (for all configurations)
+Rmax=? [ F "stable" {"init"}{max} ]
+
+// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations)
+Rmax=? [ F "stable" {"k_tokens"}{max} ]
+Rmin=? [ F "stable" {"k_tokens"}{min} ]
+
+// Minimum probability reached a stable configuration within K steps (for all configurations)
+Pmin=? [ F<=K "stable" {"init"}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm
@ -36,15 +36,14 @@ module process10=process1[q1=q10,q2=q1 ,q10=q9] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10;

--- a/prism-examples/self-stabilisation/israeli-jalfon/ij10.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij10.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm
@ -38,14 +38,14 @@ module process11=process1[q1=q11,q2=q1 ,q11=q10] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij11.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij11.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm
@ -40,14 +40,14 @@ module process12=process1[q1=q12,q2=q1 ,q12=q11] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij12.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij12.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm
@ -42,14 +42,14 @@ module process13=process1[q1=q13,q2=q1 ,q13=q12] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij13.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij13.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-Pmin=? [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm
@ -44,14 +44,14 @@ module process14=process1[q1=q14,q2=q1 ,q14=q13] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij14.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij14.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm
@ -46,14 +46,13 @@ module process15=process1[q1=q15,q2=q1 ,q15=q14] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15;
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij15.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij15.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm
@ -48,14 +48,14 @@ module process16=process1[q1=q16,q2=q1 ,q16=q15] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij16.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij16.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm
@ -50,14 +50,14 @@ module process17=process1[q1=q17,q2=q1 ,q17=q16] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij17.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij17.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm
@ -52,14 +52,13 @@ module process18=process1[q1=q18,q2=q1 ,q18=q17] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18;
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij18.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij18.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm
@ -54,14 +54,14 @@ module process19=process1[q1=q19,q2=q1 ,q19=q18] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij19.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij19.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm
@ -56,14 +56,13 @@ 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
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20;
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij20.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij20.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm
@ -58,14 +58,13 @@ module process21=process1[q1=q21,q2=q1 ,q21=q20] 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+q21>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21;
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij21.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij21.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=1) ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm
@ -23,14 +23,14 @@ module process3=process1[q1=q3, q2=q1, q3=q2] endmodule

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

 // initial states (at least one token)
 init
-	
 	q1+q2+q3>=1
-	
 endinit
+
+// formula for use in properties: number of tokens
+formula num_tokens = q1+q2+q3;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij3.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij3.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3=1) {q1+q2+q3=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3=1) {q1+q2+q3=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm
@ -25,14 +25,14 @@ module process4 =process1[q1=q4 ,q2=q1, q4=q3] endmodule

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

 // initial states (at least one token)
 init
-	
 	q1+q2+q3+q4>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij4.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij4.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4=1) {q1+q2+q3+q4=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4=1) {q1+q2+q3+q4=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm
@ -27,14 +27,14 @@ module process5 =process1[q1=q5 ,q2=q1, q5=q4] endmodule

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

 // initial states (at least one token)
 init
-	
 	q1+q2+q3+q4+q5>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij5.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij5.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5=1) {q1+q2+q3+q4+q5=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5=1) {q1+q2+q3+q4+q5=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm
@ -29,14 +29,14 @@ module process6 =process1[q1=q6 ,q2=q1, q6=q5] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij6.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij6.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6=1) {(q1+q2+q3+q4+q5+q6=k)}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6=1) {(q1+q2+q3+q4+q5+q6=k)}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm
@ -31,14 +31,14 @@ module process7 =process1[q1=q7 ,q2=q1 ,q7=q6] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7;
+
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij7.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij7.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7=1) {q1+q2+q3+q4+q5+q6+q7=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7=1) {q1+q2+q3+q4+q5+q6+q7=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm
@ -33,14 +33,13 @@ module process8 =process1[q1=q8 ,q2=q1 ,q8=q7] 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>=1
-	
 endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8;
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij8.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij8.pctl
@ -1,12 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8=1) ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8=1){"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8=1) {q1+q2+q3+q4+q5+q6+q7+q8=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8=1) {q1+q2+q3+q4+q5+q6+q7+q8=k}{min} ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm
@ -35,14 +35,13 @@ 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
+
+// formula, for use in properties: number of tokens
+formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9;
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij9.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij9.pctl
@ -1,13 +0,0 @@
-// constant used for time bounded until and for specifying a subset of initial states
-const int k;
-// a stable state is reached with probability 1
-P>=1 [ true U (q1+q2+q3+q4+q5+q6+q7+q8+q9=1)  ]
-// minimum probability a stable state is reached within k steps
-Pmin=? [ true U<=k (q1+q2+q3+q4+q5+q6+q7+q8+q9=1) {"init"}{min} ]
-// maximum expected time to reach a stable state
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9=1) {"init"}{max} ]
-// maximum expected time to reach a stable state for a subset of initial states
-Rmax=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9=k}{max} ]
-// minimum expected time to reach a stable state for a subset of initial states
-Rmin=? [ F (q1+q2+q3+q4+q5+q6+q7+q8+q9=1) {q1+q2+q3+q4+q5+q6+q7+q8+q9=k}{min} ]
-