diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp
index 2ea483d7..8e357b64 100644
--- a/prism-examples/rabin/.rabinN.nm.pp
+++ b/prism-examples/rabin/.rabinN.nm.pp
@@ -3,18 +3,15 @@
 // 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"
-
-// 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