From 6dc4684a347695670803a70b7e50986fb75ec0ec Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Wed, 14 Oct 2009 11:07:18 -0400 Subject: [PATCH] check wait free Signed-off-by: Mathieu Desnoyers --- ticketlock-testwait/DEFINES | 2 ++ ticketlock-testwait/lock_progress.ltl | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/ticketlock-testwait/DEFINES b/ticketlock-testwait/DEFINES index 4eb5315..6997f17 100644 --- 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 8718641..4bc3952 100644 --- a/ticketlock-testwait/lock_progress.ltl +++ b/ticketlock-testwait/lock_progress.ltl @@ -1 +1 @@ -([] <> !np_) +(([] <> !np_) || (!(<> [] is_one_enabled -> [] <> last_is_one))) -- 2.34.1