import header file from specification

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index 725bc5399f0fb84322b9ad90c161c8a386123fd4..1de51693eea6ecd606fe3fd616536fa152cfdc4f 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -24,7 +24,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
        explored_children(num_threads),
        backtrack(num_threads),
        numBacktracks(0),
-       may_read_from()
+       may_read_from(),
+       read_from_index(0)
 {
        if (act)
                act->set_node(this);
@@ -73,7 +74,11 @@ bool Node::has_been_explored(thread_id_t tid)
  */
 bool Node::backtrack_empty()
 {
-       return numBacktracks == 0;
+       return (numBacktracks == 0);
+}
+
+bool Node::readsfrom_empty() {
+       return ((read_from_index+1)>=may_read_from.size());
 }
 
 /**
@@ -138,13 +143,14 @@ void Node::add_read_from(const ModelAction *act)
  * may remove elements from may_read_from
  * @return The first element in may_read_from
  */
-const ModelAction * Node::get_next_read_from() {
-       const ModelAction *act;
-       ASSERT(!may_read_from.empty());
-       act = may_read_from.front();
-       /* TODO: perform reads_from replay properly */
-       /* may_read_from.pop_front(); */
-       return act;
+const ModelAction * Node::get_read_from() {
+       ASSERT(read_from_index<may_read_from.size());
+       return may_read_from[read_from_index];
+}
+
+bool Node::increment_read_from() {
+       read_from_index++;
+       return (read_from_index<may_read_from.size());
 }
 
 void Node::explore(thread_id_t tid)
@@ -214,16 +220,22 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        return NULL;
 }
 
-
-void NodeStack::pop_restofstack()
+/**
+ * Empties the stack of all trailing nodes after a given position and calls the
+ * destructor for each. This function is provided an offset which determines
+ * how many nodes (relative to the current replay state) to save before popping
+ * the stack.
+ * @param numAhead The number of nodes to skip forward before popping the stack.
+ */
+void NodeStack::pop_restofstack(int numAhead)
 {
        /* Diverging from previous execution; clear out remainder of list */
        node_list_t::iterator it = iter;
-       it++;
+       while (numAhead--)
+               it++;
        clear_node_list(&node_list, it, node_list.end());
 }
 
-
 Node * NodeStack::get_head()
 {
        if (node_list.empty())