From: Mathieu Desnoyers Date: Wed, 14 Oct 2009 15:59:38 +0000 (-0400) Subject: better lock-free test X-Git-Url: http://git.liburcu.org/?p=userspace-rcu.git;a=commitdiff_plain;h=08e5a09d6dcc497e88d6f79b9d8c33198c515acd better lock-free test Signed-off-by: Mathieu Desnoyers --- diff --git a/ticketlock-testwait/lock_progress.ltl b/ticketlock-testwait/lock_progress.ltl index 4bc3952..a2d91d7 100644 --- 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_))