From 0135c4017ef24515b75e8d79be18a3cc68dea73f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 21 May 2009 13:17:42 +0000 Subject: [PATCH] Moved "stable" label in israeli-jalfon. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1080 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp | 5 ++++- prism-examples/self-stabilisation/israeli-jalfon/ij.pctl | 1 - prism-examples/self-stabilisation/israeli-jalfon/ij10.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij11.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij12.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij13.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij14.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij15.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij16.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij17.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij18.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij19.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij20.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij21.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij3.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij4.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij5.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij6.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij7.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij8.nm | 3 +++ prism-examples/self-stabilisation/israeli-jalfon/ij9.nm | 3 +++ 21 files changed, 61 insertions(+), 2 deletions(-) diff --git a/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp b/prism-examples/self-stabilisation/israeli-jalfon/.ijN.nm.pp index c02d46b9..d658dc6e 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl index 69c0b591..f88a5731 100644 --- 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" ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm index 1898540f..200e21bd 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm index a9ce8e76..6b0d1f74 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm index e894b174..85d9f6b1 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm index 60d204ab..f02a1dc3 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm index 89736cfd..e86d5357 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm index 04fb5689..ffb73196 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm index a83ae245..8df14c40 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm index 4c316caa..ebb8214d 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm index 5dd2ffa2..78035c8e 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm index 725550d1..14c959a9 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm index a5b9c798..4fbb5c13 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm index 1f434e6d..c7708760 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm index b2c29472..40ae819f 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm index bcce25d6..3c1fd5e6 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm index 9154ebbc..39330c0a 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm index 0fe50a03..8b1cb355 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm index 70a79ac7..e8a13b0e 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm index 263b8549..6d131aeb 100644 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm index 7b9e0240..e5fad828 100644 --- 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