From 8afe95aa67927b0afde92acb88956e6c1c952985 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 26 Feb 2013 16:15:50 -0800 Subject: [PATCH] model: hook up 'read-from-promise' backtracking in ModelChecker Now we iterate over the read-from-promise set. Some things are still missing. --- model.cc | 15 +++++++++++---- nodestack.cc | 8 ++++++-- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/model.cc b/model.cc index ced34316..d3ebf4d2 100644 --- 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 3cde3456..66869ab1 100644 --- 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 ********************************/ -- 2.34.1