Undefined probability and moved label to model.

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

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

@@ -5,7 +5,7 @@
 // the procotol is synchronous with no nondeterminism (a DTMC)
 dtmc
 
-const double p;
+const double p = 0.5;
 
 // module for process 1
 module process1
@@ -36,3 +36,7 @@ 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 = #+ i=1:N#(x#i#=x#func(mod, i, N)+1#?1:0)#end#;
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -3,7 +3,6 @@ const int K; // number of steps
 
 // labels
 label "k_tokens" = num_tokens=k; // configurations with k tokens
-label "stable" = num_tokens=1;   // stable configurations (1 token)
 
 // From any configuration, a stable configuration is reached with probability 1
 "init" => P>=1 [ F "stable" ]

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

@@ -42,3 +42,7 @@ 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=x10?1:0)+(x10=x11?1:0)+(x11=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -44,3 +44,7 @@ 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=x10?1:0)+(x10=x11?1:0)+(x11=x12?1:0)+(x12=x13?1:0)+(x13=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -46,3 +46,7 @@ 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=x10?1:0)+(x10=x11?1:0)+(x11=x12?1:0)+(x12=x13?1:0)+(x13=x14?1:0)+(x14=x15?1:0)+(x15=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -48,3 +48,7 @@ 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=x10?1:0)+(x10=x11?1:0)+(x11=x12?1:0)+(x12=x13?1:0)+(x13=x14?1:0)+(x14=x15?1:0)+(x15=x16?1:0)+(x16=x17?1:0)+(x17=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -50,3 +50,7 @@ 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=x10?1:0)+(x10=x11?1:0)+(x11=x12?1:0)+(x12=x13?1:0)+(x13=x14?1:0)+(x14=x15?1:0)+(x15=x16?1:0)+(x16=x17?1:0)+(x17=x18?1:0)+(x18=x19?1:0)+(x19=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -52,3 +52,7 @@ 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=x10?1:0)+(x10=x11?1:0)+(x11=x12?1:0)+(x12=x13?1:0)+(x13=x14?1:0)+(x14=x15?1:0)+(x15=x16?1:0)+(x16=x17?1:0)+(x17=x18?1:0)+(x18=x19?1:0)+(x19=x20?1:0)+(x20=x21?1:0)+(x21=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -34,3 +34,7 @@ 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=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -36,3 +36,7 @@ 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=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -38,3 +38,7 @@ 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=x1?1:0);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+

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

@@ -40,3 +40,7 @@ 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);
+
+// label - stable configurations (1 token)
+label "stable" = num_tokens=1;
+