updated beauqier (labels)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@489 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

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} ]

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);

prism-examples/self-stabilisation/beauquier/beauquier11.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 (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} ]

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);

prism-examples/self-stabilisation/beauquier/beauquier3.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 (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}  ]

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);

prism-examples/self-stabilisation/beauquier/beauquier5.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 (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} ]

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);

prism-examples/self-stabilisation/beauquier/beauquier7.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 (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} ]

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);

prism-examples/self-stabilisation/beauquier/beauquier9.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 (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} ]