updated pctl file

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@840 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/rabin/modified/mod_rabin.pctl

@@ -1,4 +1,6 @@
-//minimum probability process enters the criticial section
+// mention that Rabin property is not well defined (see Saias thesis)
+
+// minimum probability process enters the criticial section
 // only interested in the probability in states for which
 // - process is going to make a draw (draw1=1)
 // - no process is in the critical section (otherwise probability is clearly 0
@@ -7,6 +9,12 @@ Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical"}{min} ]
 
 // probability above is zero which is due to the fact that the adversary can use the values
 // of the state variables of the other processes
+// this does not quite disprove Rabin's bounded waiting property as one is starting
+// from the state the process decides to enter the round and one doesnot take into account
+// the probability of reaching this state (this does have an influence as the results
+// for the properties below show that to get the probability 0 one of the other processes
+//must have already randomly picked a high value for its bi)
+
 // to demonstrate this fact we restrict attention to states where these values
 // are restricted,i.e. where the values of the bi variables are bounded
Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<6}{min} ]
Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<5}{min} ]
Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<4}{min} ]
Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<3}{min} ]
Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<2}{min} ]
Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<1}{min} ]
 // liveness (eventially a process enters its critical section