check wait free

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

diff --git a/ticketlock-testwait/DEFINES b/ticketlock-testwait/DEFINES
index 4eb5315a812de41d544530159c5424fca246c2e8..6997f17d547554cb868461fd4d703cd691774d7c 100644 (file)
--- a/ticketlock-testwait/DEFINES
+++ b/ticketlock-testwait/DEFINES
@@ -1 +1,3 @@
 #define refcount_gt_one (refcount > 1)
+#define is_one_enabled (enabled(1))
+#define last_is_one    (_last == 1)

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