Cleanup promela code for wakeup verif

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

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)))

diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin
index 9f6ddd46cdcb11d838d31144f732452a08736d2e..1cb6442ace3a1d5f0df16d82ab2135d6e0b0317d 100644 (file)
--- a/formal-model/futex-wakeup/futex.spin
+++ b/formal-model/futex-wakeup/futex.spin
@@ -98,13 +98,6 @@ active proctype waiter()
                                :: 1 ->
                                        if
                                        :: (fut == -1) ->
-                                               if
-                                               :: (queue == 0) ->
-progress_A:
-                                                       skip;
-                                               :: else
-                                                       skip;
-                                               fi;
                                                skip;
                                        :: else ->
                                                break;
@@ -114,7 +107,7 @@ progress_A:
                                skip;
                        fi;
                fi;
-progress_B:
+progress:
                queue = 0;
        od;
 }