From 7f4ddbae21152c88ff81ffbc208e052f7a76b5f9 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 29 Feb 2008 07:48:57 +0000
Subject: [PATCH] Added probability p to herman models.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@575 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/self-stabilisation/herman/.hermanN.pm.pp | 4 +++-
 prism-examples/self-stabilisation/herman/herman11.pm    | 4 +++-
 prism-examples/self-stabilisation/herman/herman13.pm    | 4 +++-
 prism-examples/self-stabilisation/herman/herman15.pm    | 4 +++-
 prism-examples/self-stabilisation/herman/herman17.pm    | 4 +++-
 prism-examples/self-stabilisation/herman/herman19.pm    | 4 +++-
 prism-examples/self-stabilisation/herman/herman21.pm    | 4 +++-
 prism-examples/self-stabilisation/herman/herman3.pm     | 4 +++-
 prism-examples/self-stabilisation/herman/herman5.pm     | 4 +++-
 prism-examples/self-stabilisation/herman/herman7.pm     | 4 +++-
 prism-examples/self-stabilisation/herman/herman9.pm     | 4 +++-
 11 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/prism-examples/self-stabilisation/herman/.hermanN.pm.pp b/prism-examples/self-stabilisation/herman/.hermanN.pm.pp
index aa62c7c7..4c29823b 100644
--- a/prism-examples/self-stabilisation/herman/.hermanN.pm.pp
+++ b/prism-examples/self-stabilisation/herman/.hermanN.pm.pp
@@ -5,13 +5,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x#N#) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x#N#) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x#N#) -> (x1'=x#N#);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman11.pm b/prism-examples/self-stabilisation/herman/herman11.pm
index f133a8da..0d5399a0 100644
--- a/prism-examples/self-stabilisation/herman/herman11.pm
+++ b/prism-examples/self-stabilisation/herman/herman11.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x11) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x11) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x11) -> (x1'=x11);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman13.pm b/prism-examples/self-stabilisation/herman/herman13.pm
index e945cc9e..3e28c832 100644
--- a/prism-examples/self-stabilisation/herman/herman13.pm
+++ b/prism-examples/self-stabilisation/herman/herman13.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x13) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x13) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x13) -> (x1'=x13);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman15.pm b/prism-examples/self-stabilisation/herman/herman15.pm
index c75e6d83..d0a70885 100644
--- a/prism-examples/self-stabilisation/herman/herman15.pm
+++ b/prism-examples/self-stabilisation/herman/herman15.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x15) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x15) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x15) -> (x1'=x15);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman17.pm b/prism-examples/self-stabilisation/herman/herman17.pm
index 0412a460..3428dcb4 100644
--- a/prism-examples/self-stabilisation/herman/herman17.pm
+++ b/prism-examples/self-stabilisation/herman/herman17.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x17) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x17) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x17) -> (x1'=x17);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman19.pm b/prism-examples/self-stabilisation/herman/herman19.pm
index 4c9c2931..7f603893 100644
--- a/prism-examples/self-stabilisation/herman/herman19.pm
+++ b/prism-examples/self-stabilisation/herman/herman19.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x19) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x19) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x19) -> (x1'=x19);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman21.pm b/prism-examples/self-stabilisation/herman/herman21.pm
index 5887db71..ebb8ac2e 100644
--- a/prism-examples/self-stabilisation/herman/herman21.pm
+++ b/prism-examples/self-stabilisation/herman/herman21.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x21) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x21) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x21) -> (x1'=x21);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman3.pm b/prism-examples/self-stabilisation/herman/herman3.pm
index 6a4a06e0..cc6e8119 100644
--- a/prism-examples/self-stabilisation/herman/herman3.pm
+++ b/prism-examples/self-stabilisation/herman/herman3.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x3) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x3) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x3) -> (x1'=x3);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman5.pm b/prism-examples/self-stabilisation/herman/herman5.pm
index e028d98c..cde72df2 100644
--- a/prism-examples/self-stabilisation/herman/herman5.pm
+++ b/prism-examples/self-stabilisation/herman/herman5.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x5) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x5) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x5) -> (x1'=x5);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman7.pm b/prism-examples/self-stabilisation/herman/herman7.pm
index 1c280e15..0d6ef0bd 100644
--- a/prism-examples/self-stabilisation/herman/herman7.pm
+++ b/prism-examples/self-stabilisation/herman/herman7.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // module for process 1
 module process1
 
 	// Boolean variable for process 1
 	x1 : [0..1];
 	
-	[step]  (x1=x7) -> 0.5 : (x1'=0) + 0.5 : (x1'=1);
+	[step]  (x1=x7) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x7) -> (x1'=x7);
 	
 endmodule
diff --git a/prism-examples/self-stabilisation/herman/herman9.pm b/prism-examples/self-stabilisation/herman/herman9.pm
index 3c8c4402..664854dc 100644
--- a/prism-examples/self-stabilisation/herman/herman9.pm
+++ b/prism-examples/self-stabilisation/herman/herman9.pm
@@ -4,13 +4,15 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
+const double p;
+
 // 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) -> p : (x1'=0) + 1-p : (x1'=1);
 	[step] !(x1=x9) -> (x1'=x9);
 	
 endmodule