diff --git a/prism-examples/self-stabilisation/herman/.hermanN.pm.pp b/prism-examples/self-stabilisation/herman/.hermanN.pm.pp
index 4c29823b..ae3b0f78 100644
--- a/prism-examples/self-stabilisation/herman/.hermanN.pm.pp
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman.pctl b/prism-examples/self-stabilisation/herman/herman.pctl
index 3261167a..a9501003 100644
--- a/prism-examples/self-stabilisation/herman/herman.pctl
+++ b/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" ]
diff --git a/prism-examples/self-stabilisation/herman/herman11.pm b/prism-examples/self-stabilisation/herman/herman11.pm
index 46a7334c..9eba8488 100644
--- a/prism-examples/self-stabilisation/herman/herman11.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman13.pm b/prism-examples/self-stabilisation/herman/herman13.pm
index d238c378..4d304ea1 100644
--- a/prism-examples/self-stabilisation/herman/herman13.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman15.pm b/prism-examples/self-stabilisation/herman/herman15.pm
index 1188c67f..87013227 100644
--- a/prism-examples/self-stabilisation/herman/herman15.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman17.pm b/prism-examples/self-stabilisation/herman/herman17.pm
index f9f4f1f6..fe03ef13 100644
--- a/prism-examples/self-stabilisation/herman/herman17.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman19.pm b/prism-examples/self-stabilisation/herman/herman19.pm
index 413f3687..92ac87a4 100644
--- a/prism-examples/self-stabilisation/herman/herman19.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman21.pm b/prism-examples/self-stabilisation/herman/herman21.pm
index 2535f5f9..6f87aba1 100644
--- a/prism-examples/self-stabilisation/herman/herman21.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman3.pm b/prism-examples/self-stabilisation/herman/herman3.pm
index de78ae18..da805870 100644
--- a/prism-examples/self-stabilisation/herman/herman3.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman5.pm b/prism-examples/self-stabilisation/herman/herman5.pm
index 0f257b8f..fa4f9401 100644
--- a/prism-examples/self-stabilisation/herman/herman5.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman7.pm b/prism-examples/self-stabilisation/herman/herman7.pm
index 04e34c4a..236b366a 100644
--- a/prism-examples/self-stabilisation/herman/herman7.pm
+++ b/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;
+
diff --git a/prism-examples/self-stabilisation/herman/herman9.pm b/prism-examples/self-stabilisation/herman/herman9.pm
index f1d95c7a..43e90c66 100644
--- a/prism-examples/self-stabilisation/herman/herman9.pm
+++ b/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;
+