updated properties in rabin

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@534 bbc10eb1-c90d-0410-af57-cb519fbb1720
18 years ago · 0569ba33b0
1 changed files with 2 additions and 2 deletions
--- 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" ]