From 85a95f863b750196c5c8048f597c579163672e7e Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 1 Nov 2007 14:01:16 +0000
Subject: [PATCH] Herman missing for N=9.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@499 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../self-stabilisation/herman/.autopp         |  2 +-
 .../self-stabilisation/herman/herman9.pm      | 89 +++++++++----------
 2 files changed, 41 insertions(+), 50 deletions(-)

diff --git a/prism-examples/self-stabilisation/herman/.autopp b/prism-examples/self-stabilisation/herman/.autopp
index 9e11e6f6..64f52b34 100755
--- a/prism-examples/self-stabilisation/herman/.autopp
+++ b/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
diff --git a/prism-examples/self-stabilisation/herman/herman9.pm b/prism-examples/self-stabilisation/herman/herman9.pm
index 5f207a78..3c8c4402 100644
--- a/prism-examples/self-stabilisation/herman/herman9.pm
+++ b/prism-examples/self-stabilisation/herman/herman9.pm
@@ -1,49 +1,40 @@
-// herman's self stabilising algorithm [Her90]
-// gxn/dxp 13/07/02
-
-// the procotol is synchronous with no non-determinism (a DTMC)
-dtmc
-
-// module for process 1
-module process1
-
-	// Boolean variable for process 1
-	x1 : [0..1];
-	
-	[step]  (x1=x9) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
-	[step] !(x1=x9) -> (x1'=x9);
-	
-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
-
-// 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);
+// herman's self stabilising algorithm [Her90]
+// gxn/dxp 13/07/02
+
+// the procotol is synchronous with no nondeterminism (a DTMC)
+dtmc
+
+// module for process 1
+module process1
+
+	// Boolean variable for process 1
+	x1 : [0..1];
+	
+	[step]  (x1=x9) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step] !(x1=x9) -> (x1'=x9);
+	
+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 number of steps)
+rewards "steps"
+	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 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);