diff --git a/prism-examples/self-stabilisation/israeli-jalfon/auto b/prism-examples/self-stabilisation/israeli-jalfon/auto index dbd6f819..9fb9b40b 100755 --- 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 diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl new file mode 100644 index 00000000..69c0b591 --- /dev/null +++ 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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij10.nm index 39887dfa..26c8385e 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij10.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij10.pctl deleted file mode 100644 index a7423d06..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij10.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij11.nm index c85daaef..dd8e2374 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij11.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij11.pctl deleted file mode 100644 index da024c95..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij11.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij12.nm index ebac27ec..d27f7308 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij12.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij12.pctl deleted file mode 100644 index 54fca600..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij12.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij13.nm index f0805d5e..c4472a8e 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij13.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij13.pctl deleted file mode 100644 index 4739dd27..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij13.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij14.nm index 43492252..435eb1b3 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij14.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij14.pctl deleted file mode 100644 index bfae4ce0..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij14.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij15.nm index d7dd3bb9..ed11e176 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij15.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij15.pctl deleted file mode 100644 index 5ff28c25..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij15.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij16.nm index bdc176e3..8d4eed8e 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij16.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij16.pctl deleted file mode 100644 index b859e4f5..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij16.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij17.nm index 421d1a5b..8fb82b89 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij17.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij17.pctl deleted file mode 100644 index d700c50a..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij17.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij18.nm index a526f7ad..4174e025 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij18.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij18.pctl deleted file mode 100644 index 6d4c7217..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij18.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij19.nm index 2ce7c4b7..73f4a270 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij19.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij19.pctl deleted file mode 100644 index 0d630368..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij19.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij20.nm index dcb8acb8..9a20d04b 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij20.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij20.pctl deleted file mode 100644 index 9dd7be72..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij20.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij21.nm index 8f464bd7..b08c3b3d 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij21.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij21.pctl deleted file mode 100644 index 45c5eadb..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij21.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij3.nm index 95db3338..7e6f128e 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij3.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij3.pctl deleted file mode 100644 index f65e9a90..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij3.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij4.nm index dfd1cd56..50762233 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij4.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij4.pctl deleted file mode 100644 index 134bd216..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij4.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij5.nm index 49cd9f72..6f2fe5b2 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij5.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij5.pctl deleted file mode 100644 index af0060fb..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij5.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij6.nm index 195fe226..49ec18b6 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij6.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij6.pctl deleted file mode 100644 index 00ce6aa3..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij6.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij7.nm index 952b13fe..7444245c 100644 --- 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; + diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij7.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij7.pctl deleted file mode 100644 index c8aedb6d..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij7.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij8.nm index 99fc9ed2..0ea4c7aa 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij8.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij8.pctl deleted file mode 100644 index 619fa9e6..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij8.pctl +++ /dev/null @@ -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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm b/prism-examples/self-stabilisation/israeli-jalfon/ij9.nm index 1d46e2f0..8d470653 100644 --- 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; diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij9.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij9.pctl deleted file mode 100644 index df8b5e53..00000000 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij9.pctl +++ /dev/null @@ -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} ] -