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" ]