Fix formal model nesting

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

diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
index e5bfff32464c0e4d6d0985df50cb8fa6db2555b0..611464b3eb660b61d6269b5c64210afe6754d950 100644 (file)
--- a/formal-model/urcu.spin
+++ b/formal-model/urcu.spin
@@ -124,9 +124,13 @@ proctype urcu_reader()
                                break;
                        :: tmp < 4 && reader_progress[tmp] != 0 ->
                                tmp = tmp + 1;
-                       :: tmp >= 4 ->
+                       :: tmp >= 4 &&
+                          reader_progress[0] == reader_progress[3] ->
                                done = 1;
                                break;
+                       :: tmp >= 4 &&
+                          reader_progress[0] != reader_progress[3] ->
+                               break;
                        od;
                        do
                        :: tmp < 4 && reader_progress[tmp] == 0 ->