Moved "stable" label in israeli-jalfon.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1080 bbc10eb1-c90d-0410-af57-cb519fbb1720
17 years ago · 0135c4017e
21 changed files with 61 additions and 2 deletions
--- a/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp
+++ b/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp
@ -29,7 +29,10 @@ endrewards

 // formula, for use here and in properties: number of tokens
 formula num_tokens = #+ i=1:N#q#i##end#;
-
// initial states (at least one token)
+
// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
+// initial states (at least one token)
 init
 	num_tokens >= 1
 endinit
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl
@ -3,7 +3,6 @@ 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" ]
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm
@ -42,6 +42,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm
@ -44,6 +44,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm
@ -46,6 +46,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm
@ -48,6 +48,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm
@ -50,6 +50,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm
@ -52,6 +52,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm
@ -54,6 +54,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm
@ -56,6 +56,9 @@ endrewards
 // formula, for use here and 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;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm
@ -58,6 +58,9 @@ endrewards
 // formula, for use here and 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;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm
@ -60,6 +60,9 @@ endrewards
 // formula, for use here and 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;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm
@ -62,6 +62,9 @@ endrewards
 // formula, for use here and 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;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm
@ -64,6 +64,9 @@ endrewards
 // formula, for use here and 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;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm
@ -28,6 +28,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm
@ -30,6 +30,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm
@ -32,6 +32,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm
@ -34,6 +34,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm
@ -36,6 +36,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm
@ -38,6 +38,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1
--- a/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm
+++ b/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm
@ -40,6 +40,9 @@ endrewards
 // formula, for use here and in properties: number of tokens
 formula num_tokens = q1+q2+q3+q4+q5+q6+q7+q8+q9;

+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+
 // initial states (at least one token)
 init
 	num_tokens >= 1