better lock-free test

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

diff --git a/ticketlock-testwait/lock_progress.ltl b/ticketlock-testwait/lock_progress.ltl
index 4bc3952985ae1fe36195d2202f564d40a65e03e6..a2d91d7ceeeeabfe70db740ec1524264bbbdcd26 100644 (file)
--- a/ticketlock-testwait/lock_progress.ltl
+++ b/ticketlock-testwait/lock_progress.ltl
@@ -1 +1 @@
-(([] <> !np_) || (!(<> [] is_one_enabled -> [] <> last_is_one)))
+((<> [] is_one_enabled -> [] <> last_is_one) -> ([] <> !np_))