From 40054ea0ed7cba9e2bdc53fb5b71af7043561d47 Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Mon, 8 Dec 2008 11:04:14 +0000 Subject: [PATCH] updated rabin spec file git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@880 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/rabin/rabin.pctl | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prism-examples/rabin/rabin.pctl b/prism-examples/rabin/rabin.pctl index 81363510..3db25f61 100644 --- a/prism-examples/rabin/rabin.pctl +++ b/prism-examples/rabin/rabin.pctl @@ -22,5 +22,6 @@ Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical"}{min} ] //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} ] - +// are restricted,i.e. where the values of the bi variables are bounded +const int k; + Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<=k}{min} ]