Herman missing for N=9.

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

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

@@ -1,6 +1,6 @@
 #!/bin/csh
 
-foreach N ( 3 5 7 11 13 15 17 19 21 )
+foreach N ( 3 5 7 9 11 13 15 17 19 21 )
 	echo "Generating for N=$N"
 	prismpp .hermanN.pm.pp $N >! herman$N.pm
 	unix2dos herman$N.pm

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

@@ -1,7 +1,7 @@
 // herman's self stabilising algorithm [Her90]
 // gxn/dxp 13/07/02
 
-// the procotol is synchronous with no non-determinism (a DTMC)
+// the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
 // module for process 1
@@ -16,26 +16,17 @@ module process1
 endmodule
 
 // add further processes through renaming
-module process2 = process1[x1=x2, x9=x1 ] endmodule
-module process3 = process1[x1=x3, x9=x2 ] endmodule
-module process4 = process1[x1=x4, x9=x3 ] endmodule
-module process5 = process1[x1=x5, x9=x4 ] endmodule
-module process6 = process1[x1=x6, x9=x5 ] endmodule
-module process7 = process1[x1=x7, x9=x6 ] endmodule
-module process8 = process1[x1=x8, x9=x7 ] endmodule
-module process9 = process1[x1=x9, x9=x8 ] endmodule
-
-// cost - 1 in each state (expected steps)
-rewards
-	true : 1;
-endrewards
+module process2 = process1 [ x1=x2, x9=x1 ] endmodule
+module process3 = process1 [ x1=x3, x9=x2 ] endmodule
+module process4 = process1 [ x1=x4, x9=x3 ] endmodule
+module process5 = process1 [ x1=x5, x9=x4 ] endmodule
+module process6 = process1 [ x1=x6, x9=x5 ] endmodule
+module process7 = process1 [ x1=x7, x9=x6 ] endmodule
+module process8 = process1 [ x1=x8, x9=x7 ] endmodule
+module process9 = process1 [ x1=x9, x9=x8 ] endmodule
 
-// any initial state (consider any possible initial configuration of tokens)
-init
-	true
-endinit
 // cost - 1 in each state (expected number of steps)
-rewards
+rewards "steps"
 	true : 1;
 endrewards
 
@@ -44,6 +35,6 @@ 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, for use in properties: number of tokens
+// (i.e. number of processes that have the same value as 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);