switch everything over to our own hashtable

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index 5a65821188fa0698de88a3c03684abea0f12adc8..e8f377b51a6dfbca7e59dc69b1a81a5b19cac196 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -77,6 +77,11 @@ bool Node::backtrack_empty()
        return (numBacktracks == 0);
 }
 
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
 bool Node::readsfrom_empty() {
        return ((read_from_index+1)>=may_read_from.size());
 }
@@ -148,6 +153,10 @@ const ModelAction * Node::get_read_from() {
        return may_read_from[read_from_index];
 }
 
+/**
+ * Increments the index into the readsfrom set to explore the next item.
+ * @return Returns false if we have explored all items.
+ */
 bool Node::increment_read_from() {
        read_from_index++;
        return (read_from_index<may_read_from.size());
@@ -220,7 +229,14 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        return NULL;
 }
 
-
+/**
+ * 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 gives the number of Nodes (including this Node) to skip over
+ * before removing nodes.
+ */
 void NodeStack::pop_restofstack(int numAhead)
 {
        /* Diverging from previous execution; clear out remainder of list */
@@ -230,7 +246,6 @@ void NodeStack::pop_restofstack(int numAhead)
        clear_node_list(&node_list, it, node_list.end());
 }
 
-
 Node * NodeStack::get_head()
 {
        if (node_list.empty())