diff --git a/prism-examples/rabin/rabin.pctl b/prism-examples/rabin/rabin.pctl
index 1812c520..e33f84db 100644
--- a/prism-examples/rabin/rabin.pctl
+++ b/prism-examples/rabin/rabin.pctl
@@ -1,5 +1,5 @@
-// Mutual exclusion
+// Mutual exclusion: at any time t there is at most one process in its critical section phase
 num_procs_in_crit <= 1
 
-// Liveness: If a process is trying, then eventually a process enters the critical section
+// Liveness: if a process is trying, then eventually a process enters the critical section
 "one_trying" => P>=1 [ true U "one_critical" ]