From f9556e6ddcc7bf980706868d4ce53fb68438d7b2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 18 Mar 2008 17:07:34 +0000 Subject: [PATCH] Props: "true U" -> "F". git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@690 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/rabin/rabin.pctl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism-examples/rabin/rabin.pctl b/prism-examples/rabin/rabin.pctl index e33f84db..14724378 100644 --- a/prism-examples/rabin/rabin.pctl +++ b/prism-examples/rabin/rabin.pctl @@ -2,4 +2,4 @@ num_procs_in_crit <= 1 // Liveness: if a process is trying, then eventually a process enters the critical section -"one_trying" => P>=1 [ true U "one_critical" ] +"one_trying" => P>=1 [ F "one_critical" ]