+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;
+ numBacktracks = 0;
+}
+
+/************************** end threads backtracking **************************/
+
+/*********************************** promise **********************************/
+
+/**
+ * Sets a promise to explore meeting with the given node.
+ * @param i is the promise index.
+ */
+void Node::set_promise(unsigned int i)
+{
+ if (i >= resolve_promise.size())
+ resolve_promise.resize(i + 1, false);
+ resolve_promise[i] = true;
+}
+
+/**
+ * Looks up whether a given promise should be satisfied by this node.
+ * @param i The promise index.
+ * @return true if the promise should be satisfied by the given ModelAction.
+ */
+bool Node::get_promise(unsigned int i) const
+{
+ return (i < resolve_promise.size()) && (int)i == resolve_promise_idx;
+}
+
+/**
+ * Increments to the next promise to resolve.
+ * @return true if we have a valid combination.
+ */
+bool Node::increment_promise()
+{
+ DBG();
+ if (resolve_promise.empty())
+ return false;
+ int prev_idx = resolve_promise_idx;
+ resolve_promise_idx++;
+ for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++)
+ if (resolve_promise[resolve_promise_idx])
+ return true;
+ resolve_promise_idx = prev_idx;
+ return false;
+}
+
+/**
+ * Returns whether the promise set is empty.
+ * @return true if we have explored all promise combinations.
+ */
+bool Node::promise_empty() const
+{
+ for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
+ if (i >= 0 && resolve_promise[i])
+ return false;
+ return true;
+}
+
+/** @brief Clear any promise-resolution information for this Node */
+void Node::clear_promise_resolutions()
+{
+ resolve_promise.clear();
+ resolve_promise_idx = -1;
+}
+
+/******************************* end promise **********************************/
+
+void Node::set_misc_max(int i)
+{
+ misc_max = i;
+}
+
+int Node::get_misc() const
+{
+ return misc_index;
+}
+
+bool Node::increment_misc()
+{
+ return (misc_index < misc_max) && ((++misc_index) < misc_max);
+}
+
+bool Node::misc_empty() const
+{
+ return (misc_index + 1) >= misc_max;
+}
+
+bool Node::is_enabled(Thread *t) const
+{
+ int thread_id = id_to_int(t->get_id());
+ return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
+}
+
+enabled_type_t Node::enabled_status(thread_id_t tid) const
+{
+ int thread_id = id_to_int(tid);
+ if (thread_id < num_threads)
+ return enabled_array[thread_id];
+ else
+ return THREAD_DISABLED;
+}
+
+bool Node::is_enabled(thread_id_t tid) const
+{
+ int thread_id = id_to_int(tid);
+ return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
+}
+
+bool Node::has_priority(thread_id_t tid) const
+{
+ return fairness[id_to_int(tid)].priority;
+}
+
+bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
+{
+ return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P;
+}
+
+/*********************************** read from ********************************/
+
+/**
+ * Get the current state of the may-read-from set iteration
+ * @return The read-from type we should currently be checking (past or future)
+ */
+read_from_type_t Node::get_read_from_status()