diff --git a/prism-examples/self-stabilisation/beauquier/auto b/prism-examples/self-stabilisation/beauquier/auto index d5f0ad8a..fc220e90 100755 --- a/prism-examples/self-stabilisation/beauquier/auto +++ b/prism-examples/self-stabilisation/beauquier/auto @@ -1,7 +1,7 @@ #!/bin/csh -prism beauquier3.nm beauquier3.pctl -prop 1 -const k=0 -prism beauquier3.nm beauquier3.pctl -prop 2 -const k=1:1:100 -m -prism beauquier3.nm beauquier3.pctl -prop 3 -const k=0 -m -prism beauquier3.nm beauquier3.pctl -prop 4 -const k=1:2:3 -m -prism beauquier3.nm beauquier3.pctl -prop 5 -const k=1:2:3 -m +prism beauquier3.nm beauquier.pctl -prop 1 -const k=0,K=0 +prism beauquier3.nm beauquier.pctl -prop 2 -const k=0,K=0 -m +prism beauquier3.nm beauquier.pctl -prop 3 -const k=1:2:3,K=0 -m +prism beauquier3.nm beauquier.pctl -prop 4 -const k=1:2:3,K=0 -m +prism beauquier3.nm beauquier.pctl -prop 5 -const k=3,K=1:1:100 -m diff --git a/prism-examples/self-stabilisation/beauquier/beauquier.pctl b/prism-examples/self-stabilisation/beauquier/beauquier.pctl new file mode 100644 index 00000000..69c0b591 --- /dev/null +++ b/prism-examples/self-stabilisation/beauquier/beauquier.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/beauquier/beauquier11.nm b/prism-examples/self-stabilisation/beauquier/beauquier11.nm index 0e72529f..677549d6 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier11.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier11.nm @@ -27,16 +27,15 @@ module process9 =process1[p1=p9 ,p11=p8, d1=d9 ,d11=d8] endmodule module process10=process1[p1=p10,p11=p9, d1=d10,d11=d9] endmodule module process11=process1[p1=p11,p11=p10,d1=d11,d11=d10] endmodule -// cost in any state is 1 (expected number of steps) -rewards - - true : 1; - -endrewards - +// cost - 1 in each state (expected steps) +rewards + true : 1; +endrewards + // initial states - any state with more than 1 token, that is all states -init - - true - -endinit +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0); diff --git a/prism-examples/self-stabilisation/beauquier/beauquier11.pctl b/prism-examples/self-stabilisation/beauquier/beauquier11.pctl deleted file mode 100644 index 421e340a..00000000 --- a/prism-examples/self-stabilisation/beauquier/beauquier11.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 (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=1 ] -// minimum probability a stable state is reached within k steps -Pmin=? [ true U<=k (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=1 {"init"}{min} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=1 {"init"}{max} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=1 {(p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=k}{max} ] -// minimum expected time to reach a stable state for a subset of initial states -Rmin=? [ F (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=1 {(p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)=k}{min} ] diff --git a/prism-examples/self-stabilisation/beauquier/beauquier3.nm b/prism-examples/self-stabilisation/beauquier/beauquier3.nm index eb02df43..afc6c3f8 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier3.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier3.nm @@ -19,16 +19,15 @@ endmodule module process2 =process1[p1=p2 ,p3=p1, d1=d2 ,d3=d1] endmodule module process3 =process1[p1=p3 ,p3=p2, d1=d3 ,d3=d2] endmodule -// cost in any state is 1 (expected number of steps) -rewards - - true : 1; - -endrewards - +// cost - 1 in each state (expected steps) +rewards + true : 1; +endrewards + // initial states - any state with more than 1 token, that is all states -init - - true - -endinit +init + true +endinit + +// formula for use in properties: number of tokens +formula num_tokens = (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0); diff --git a/prism-examples/self-stabilisation/beauquier/beauquier3.pctl b/prism-examples/self-stabilisation/beauquier/beauquier3.pctl deleted file mode 100644 index 3452c2e6..00000000 --- a/prism-examples/self-stabilisation/beauquier/beauquier3.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 (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=1 ] -// minimum probability a stable state is reached within k steps -Pmin=? [ true U<=k (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=1 {"init"}{min} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=1 {"init"}{max} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=1 {(p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=k}{max} ] -// minimum expected time to reach a stable state for a subset of initial states -Rmin=? [ F (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=1 {(p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)=k}{min} ] diff --git a/prism-examples/self-stabilisation/beauquier/beauquier5.nm b/prism-examples/self-stabilisation/beauquier/beauquier5.nm index babb5710..5f74632d 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier5.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier5.nm @@ -21,16 +21,15 @@ module process3 =process1[p1=p3 ,p5=p2, d1=d3 ,d5=d2] endmodule module process4 =process1[p1=p4 ,p5=p3, d1=d4 ,d5=d3] endmodule module process5 =process1[p1=p5 ,p5=p4, d1=d5 ,d5=d4] endmodule -// cost in any state is 1 (expected number of steps) -rewards - - true : 1; - -endrewards - +// cost - 1 in each state (expected steps) +rewards + true : 1; +endrewards + // initial states - any state with more than 1 token, that is all states -init - - true - -endinit +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0); diff --git a/prism-examples/self-stabilisation/beauquier/beauquier5.pctl b/prism-examples/self-stabilisation/beauquier/beauquier5.pctl deleted file mode 100644 index 5d1d8915..00000000 --- a/prism-examples/self-stabilisation/beauquier/beauquier5.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 (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=1 ] -// minimum probability a stable state is reached within k steps -Pmin=? [ true U<=k (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=1 {"init"}{min} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=1 {"init"}{max} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=1 {(p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=k}{max} ] -// minimum expected time to reach a stable state for a subset of initial states -Rmin=? [ F (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=1 {(p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)=k}{min} ] diff --git a/prism-examples/self-stabilisation/beauquier/beauquier7.nm b/prism-examples/self-stabilisation/beauquier/beauquier7.nm index 4267d93a..16b11020 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier7.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier7.nm @@ -23,16 +23,15 @@ module process5 =process1[p1=p5 ,p7=p4, d1=d5 ,d7=d4] endmodule module process6 =process1[p1=p6 ,p7=p5, d1=d6 ,d7=d5] endmodule module process7 =process1[p1=p7 ,p7=p6, d1=d7 ,d7=d6] endmodule -// cost in any state is 1 (expected number of steps) -rewards - - true : 1; - -endrewards - +// cost - 1 in each state (expected steps) +rewards + true : 1; +endrewards + // initial states - any state with more than 1 token, that is all states -init - - true - -endinit +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0); diff --git a/prism-examples/self-stabilisation/beauquier/beauquier7.pctl b/prism-examples/self-stabilisation/beauquier/beauquier7.pctl deleted file mode 100644 index a467084f..00000000 --- a/prism-examples/self-stabilisation/beauquier/beauquier7.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 (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=1 ] -// minimum probability a stable state is reached within k steps -Pmin=? [ true U<=k (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=1 {"init"}{min} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=1 {"init"}{max} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=1 {(p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=k}{max} ] -// minimum expected time to reach a stable state for a subset of initial states -Rmin=? [ F (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=1 {(p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)=k}{min} ] diff --git a/prism-examples/self-stabilisation/beauquier/beauquier9.nm b/prism-examples/self-stabilisation/beauquier/beauquier9.nm index 4249067c..d7fc4df0 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier9.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier9.nm @@ -25,16 +25,15 @@ module process7 =process1[p1=p7 ,p9=p6, d1=d7 ,d9=d6] endmodule module process8 =process1[p1=p8 ,p9=p7, d1=d8 ,d9=d7] endmodule module process9 =process1[p1=p9 ,p9=p8, d1=d9 ,d9=d8] endmodule -// cost in any state is 1 (expected number of steps) -rewards - - true : 1; - -endrewards - +// cost - 1 in each state (expected steps) +rewards + true : 1; +endrewards + // initial states - any state with more than 1 token, that is all states -init - - true - -endinit +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0); diff --git a/prism-examples/self-stabilisation/beauquier/beauquier9.pctl b/prism-examples/self-stabilisation/beauquier/beauquier9.pctl deleted file mode 100644 index 566c066c..00000000 --- a/prism-examples/self-stabilisation/beauquier/beauquier9.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 (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=1 ] -// minimum probability a stable state is reached within k steps -Pmin=? [ true U<=k (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=1 {"init"}{min} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=1 {"init"}{max} ] -// maximum expected time to reach a stable state -Rmax=? [ F (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=1 {(p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=k}{max} ] -// minimum expected time to reach a stable state for a subset of initial states -Rmin=? [ F (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=1 {(p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)=k}{min} ]