model: refactor process_read logic

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 9e476a95f76a68d1f3395b271c83b0b70c0cc387..63ff36386a1db6425ce124700d6c776349779cc0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -864,21 +864,20 @@ bool ModelChecker::process_read(ModelAction *curr)
                        mo_graph->startChanges();
 
                        ASSERT(!is_infeasible());
-                       if (!check_recency(curr, rf))
-                               priv->too_many_reads = true;
-                       updated = r_modification_order(curr, rf);
-
-                       if (is_infeasible() && node->increment_read_from()) {
-                               mo_graph->rollbackChanges();
-                               priv->too_many_reads = false;
-                               continue;
+                       if (!check_recency(curr, rf)) {
+                               if (node->increment_read_from()) {
+                                       mo_graph->rollbackChanges();
+                                       continue;
+                               } else {
+                                       priv->too_many_reads = true;
+                               }
                        }
 
+                       updated = r_modification_order(curr, rf);
                        value = rf->get_value();
                        read_from(curr, rf);
                        mo_graph->commitChanges();
                        mo_check_promises(curr, true);
-
                        break;
                }
                case READ_FROM_PROMISE: {