projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
nodestack: bugfix - reset backtracking points on diverging paths
[model-checker.git]
/
nodestack.cc
diff --git
a/nodestack.cc
b/nodestack.cc
index 59e9b5dcad8f9630b2e9dd7ad25a97728ea25458..9c0df20b5de89bd2876cde69ca281502506f4709 100644
(file)
--- a/
nodestack.cc
+++ b/
nodestack.cc
@@
-348,6
+348,14
@@
thread_id_t Node::get_next_backtrack()
return int_to_id(i);
}
return int_to_id(i);
}
+void Node::clear_backtracking()
+{
+ for (unsigned int i = 0; i < backtrack.size(); i++)
+ backtrack[i] = false;
+ for (unsigned int i = 0; i < explored_children.size(); i++)
+ explored_children[i] = false;
+}
+
bool Node::is_enabled(Thread *t) const
{
int thread_id = id_to_int(t->get_id());
bool Node::is_enabled(Thread *t) const
{
int thread_id = id_to_int(t->get_id());
@@
-581,6
+589,7
@@
void NodeStack::pop_restofstack(int numAhead)
for (unsigned int i = it; i < node_list.size(); i++)
delete node_list[i];
node_list.resize(it);
for (unsigned int i = it; i < node_list.size(); i++)
delete node_list[i];
node_list.resize(it);
+ node_list.back()->clear_backtracking();
}
Node * NodeStack::get_head() const
}
Node * NodeStack::get_head() const