projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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;
break;
:: tmp < 4 && reader_progress[tmp] != 0 ->
tmp = tmp + 1;
- :: tmp >= 4 ->
+ :: tmp >= 4 &&
+ reader_progress[0] == reader_progress[3] ->
done = 1;
break;
done = 1;
break;
+ :: tmp >= 4 &&
+ reader_progress[0] != reader_progress[3] ->
+ break;
od;
do
:: tmp < 4 && reader_progress[tmp] == 0 ->
od;
do
:: tmp < 4 && reader_progress[tmp] == 0 ->
This page took
0.021911 seconds
and
4
git commands to generate.