diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp
index 8e357b64..85cc9242 100644
--- a/prism-examples/rabin/.rabinN.nm.pp
+++ b/prism-examples/rabin/.rabinN.nm.pp
@@ -3,7 +3,8 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
 // the step corresponding to a process making a draw has been split into two steps
 // to allow us to identify states where a process will draw without knowing the value
@@ -19,12 +20,10 @@ mdp
 const int K = #K#; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 

 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
-

+
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin10.nm b/prism-examples/rabin/rabin10.nm
index 6d39b325..63a1a310 100644
--- a/prism-examples/rabin/rabin10.nm
+++ b/prism-examples/rabin/rabin10.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 8; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin3.nm b/prism-examples/rabin/rabin3.nm
index 84d40bb9..21442614 100644
--- a/prism-examples/rabin/rabin3.nm
+++ b/prism-examples/rabin/rabin3.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 6; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin4.nm b/prism-examples/rabin/rabin4.nm
index 23f9f4dd..02588de0 100644
--- a/prism-examples/rabin/rabin4.nm
+++ b/prism-examples/rabin/rabin4.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 6; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin5.nm b/prism-examples/rabin/rabin5.nm
index dfdb2a3f..9c9e8be9 100644
--- a/prism-examples/rabin/rabin5.nm
+++ b/prism-examples/rabin/rabin5.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 7; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin6.nm b/prism-examples/rabin/rabin6.nm
index 4a8f18fc..53e842e7 100644
--- a/prism-examples/rabin/rabin6.nm
+++ b/prism-examples/rabin/rabin6.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 7; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin7.nm b/prism-examples/rabin/rabin7.nm
index 6f0cf342..b648224b 100644
--- a/prism-examples/rabin/rabin7.nm
+++ b/prism-examples/rabin/rabin7.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 7; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin8.nm b/prism-examples/rabin/rabin8.nm
index d10dff90..00de3519 100644
--- a/prism-examples/rabin/rabin8.nm
+++ b/prism-examples/rabin/rabin8.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 7; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);
 
diff --git a/prism-examples/rabin/rabin9.nm b/prism-examples/rabin/rabin9.nm
index 961536c0..73713f60 100644
--- a/prism-examples/rabin/rabin9.nm
+++ b/prism-examples/rabin/rabin9.nm
@@ -1,18 +1,16 @@
 // N-processor mutual exclusion [Rab82]
 // gxn/dxp 03/12/08
 
-// modified version to analyse the bounded waiting property
-// more precisely we analyse the waeker property:
-// "the minimum probability a process enters the critical section given the process tries"
+// to remove the need for fairness constraints for this model it is sufficent
+// to remove the self loops from the model 
 
-// we modify the model by dividing the step corresponding to a process making a draw into two steps
-// this allows one to identify states where a process will draw without knowing
-// what value the process will randomly pick
-// these two steps are atomic (i.e. no other process can move one the first step has been made)
-// as otherwise the adversary can prevent the process from actually drawing in the current round
-// by not scheduling it after it has performed the first step
-
-// to remove the need for fairness constraints we have also removed the self loops from the model 
+// the step corresponding to a process making a draw has been split into two steps
+// to allow us to identify states where a process will draw without knowing the value
+// randomly drawn
+// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic
+// (i.e. no other process can move one the first step has been made)
+// as for example otherwise an adversary can prevent the process from actually drawing
+// in the current round by not scheduling it after it has performed the first step
 
 mdp
 
@@ -20,14 +18,10 @@ mdp
 const int K = 8; // 4+ceil(log_2 N)
 
 // global variables (all modules can read and write)
-
- 
-
 global c : [0..1]; // 0/1 critical section free/taken
 global b : [0..K]; // current highest draw
 global r : [1..2]; // current round
 
-
 // formula for process 1 drawing
 formula draw = p1=1 & (b<b1 | r!=r1);