Cleanup promela code for wakeup verif

[urcu.git] / formal-model / futex-wakeup / futex.spin

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;
 }