updated herman (rewards)

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

prism-examples/self-stabilisation/herman/.hermanN.pm.pp

@@ -23,13 +23,13 @@ module process#i# = process1 [ x1=x#i#, x#N#=x#i-1# ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/auto

@@ -1,6 +1,7 @@
 #!/bin/csh
 
-prism herman7.pm herman.pctl -prop 1 -const k=0
-prism herman7.pm herman.pctl -prop 2 -const k=0
-prism herman7.pm herman.pctl -prop 3 -const k=1:2:7
-prism herman7.pm herman.pctl -prop 4 -const k=1:2:7
+prism herman7.pm herman.pctl -prop 1 -const k=0,K=0
+prism herman7.pm herman.pctl -prop 2 -const k=0,K=0
+prism herman7.pm herman.pctl -prop 3 -const k=1:2:7,K=0
+prism herman7.pm herman.pctl -prop 4 -const k=1:2:7,K=0
+prism herman7.pm herman.pctl -prop 5 -const k=0,K=1:1:100

prism-examples/self-stabilisation/herman/herman.pctl

@@ -1,19 +1,20 @@
-const int k;
+const int k; // number of tokens
+const int K; // number of steps
 
-// States with k tokens
-label "k_tokens" = num_tokens=k;
+// labels
+label "k_tokens" = num_tokens=k; // configurations with k tokens
+label "stable" = num_tokens=1;   // stable configurations (1 token)
 
-// Stable states - where only one process has a token
-label "stable" = num_tokens=1;
-
-// A stable state is reached with probability 1
+// From any configuration, a stable configuration is reached with probability 1
 "init" => P>=1 [ F "stable" ]
 
-// Maximum expected time to reach a stable state (for all configurations)
+// Maximum expected time to reach a stable configuration (for all configurations)
 R=? [ F "stable" {"init"}{max} ]
 
-// Maximum expected time to reach a stable state (for all k-token configurations)
+// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations)
 R=? [ F "stable" {"k_tokens"}{max} ]
-
-// Minimum expected time to reach a stable state (for all k-token configurations)
 R=? [ F "stable" {"k_tokens"}{min} ]
+
+// Minimum probability reached a stable configuration within K steps (for all configurations)
+P=? [ F<=K "stable" {"init"}{min} ]
+

prism-examples/self-stabilisation/herman/herman11.pm

@@ -29,13 +29,13 @@ module process11 = process1 [ x1=x11, x11=x10 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman13.pm

@@ -31,13 +31,13 @@ module process13 = process1 [ x1=x13, x13=x12 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman15.pm

@@ -33,13 +33,13 @@ module process15 = process1 [ x1=x15, x15=x14 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman17.pm

@@ -35,13 +35,13 @@ module process17 = process1 [ x1=x17, x17=x16 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman19.pm

@@ -37,13 +37,13 @@ module process19 = process1 [ x1=x19, x19=x18 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman21.pm

@@ -39,13 +39,13 @@ module process21 = process1 [ x1=x21, x21=x20 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman3.pm

@@ -21,13 +21,13 @@ module process3 = process1 [ x1=x3, x3=x2 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman5.pm

@@ -23,13 +23,13 @@ module process5 = process1 [ x1=x5, x5=x4 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman7.pm

@@ -25,13 +25,13 @@ module process7 = process1 [ x1=x7, x7=x6 ] endmodule
 
 // cost - 1 in each state (expected number of steps)
 rewards "steps"
-	
 	true : 1;
-	
 endrewards
 
 // set of initial states: all (i.e. any possible initial configuration of tokens)
-init true endinit
+init
+	true
+endinit
 
 // formula, for use in properties: number of tokens
 // (i.e. number of processes that have the same value as the process to their left)

prism-examples/self-stabilisation/herman/herman9.pm

@@ -27,14 +27,23 @@ module process9 = process1[x1=x9, x9=x8 ] endmodule
 
 // cost - 1 in each state (expected steps)
 rewards
-	
 	true : 1;
-	
 endrewards
 
 // any initial state (consider any possible initial configuration of tokens)
 init
-	
 	true
-	
 endinit
+// cost - 1 in each state (expected number of steps)
+rewards
+	true : 1;
+endrewards
+
+// set of initial states: all (i.e. any possible initial configuration of tokens)
+init
+	true
+endinit
+
+// formula for use in properties: number of tokens
+// (i.e. number of processes whose variable has the same value as that of the process to their left)
+formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x5?1:0)+(x5=x6?1:0)+(x6=x7?1:0)+(x7=x8?1:0)+(x8=x9?1:0)+(x9=x1?1:0);