model: hook up 'read-from-promise' backtracking in ModelChecker

Now we iterate over the read-from-promise set. Some things are still
missing.

diff --git a/model.cc b/model.cc
index ced34316234020eca13efcbb7346d1ee523002e9..d3ebf4d2e3fd99b0628d9577b95ff7e846b4867a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -871,6 +871,15 @@ bool ModelChecker::process_read(ModelAction *curr)
                        updated |= r_status;
                        break;
                }
+               case READ_FROM_PROMISE: {
+                       const Promise *promise = curr->get_node()->get_read_from_promise();
+                       value = promise->get_value();
+                       curr->set_read_from_promise(promise);
+                       mo_graph->startChanges();
+                       updated = r_modification_order(curr, promise);
+                       mo_graph->commitChanges();
+                       break;
+               }
                case READ_FROM_FUTURE: {
                        /* Read from future value */
                        struct future_value fv = node->get_future_value();
@@ -2652,10 +2661,8 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
                        /* Only add feasible future-values */
                        mo_graph->startChanges();
                        r_modification_order(curr, promise);
-                       if (!is_infeasible()) {
-                               const struct future_value fv = promise->get_fv();
-                               curr->get_node()->add_future_value(fv);
-                       }
+                       if (!is_infeasible())
+                               curr->get_node()->add_read_from_promise(promise_read);
                        mo_graph->rollbackChanges();
                }
        }

diff --git a/nodestack.cc b/nodestack.cc
index 3cde3456bb9363bc08f2549035166b6f7fe3bd15..66869ab12b2f2c0e17ba7b7c740e62391ba0b99a 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -365,7 +365,9 @@ bool Node::increment_read_from()
  */
 bool Node::read_from_empty() const
 {
-       return read_from_past_empty() && future_value_empty();
+       return read_from_past_empty() &&
+               read_from_promise_empty() &&
+               future_value_empty();
 }
 
 /**
@@ -375,7 +377,9 @@ bool Node::read_from_empty() const
  */
 unsigned int Node::read_from_size() const
 {
-       return read_from_past.size() + future_values.size();
+       return read_from_past.size() +
+               read_from_promises.size() +
+               future_values.size();
 }
 
 /******************************* end read from ********************************/