X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu.spin;h=611464b3eb660b61d6269b5c64210afe6754d950;hp=e5bfff32464c0e4d6d0985df50cb8fa6db2555b0;hb=f321bf383dd9b5940b31e4db6c9e18a5abaa0213;hpb=1eec319e7724ac54bb3174f367ca9391840fcdc1

diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
index e5bfff3..611464b 100644
--- 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 ->