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

@@ -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

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

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

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

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

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

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

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

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

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

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