Cleanup promela code for wakeup verif

[urcu.git] / formal-model / futex-wakeup / futex.ltl

diff --git a/formal-model/futex-wakeup/futex.ltl b/formal-model/futex-wakeup/futex.ltl
index 87186413c9ba4e59e8b4c3814696692c1f974418..3d6842e5d9971e1212a77a2fab94f764d6aa0cf6 100644 (file)
--- a/formal-model/futex-wakeup/futex.ltl
+++ b/formal-model/futex-wakeup/futex.ltl
@@ -1 +1 @@
-([] <> !np_)
+([] <> ((!np_) || (!queue_has_entry)))