+/************************* end read_from_promises *****************************/
+
+/****************************** future values *********************************/
+
+/**
+ * Adds a value from a weakly ordered future write to backtrack to. This
+ * operation may "fail" if the future value has already been run (within some
+ * sloppiness window of this expiration), or if the futurevalues set has
+ * reached its maximum.
+ * @see model_params.maxfuturevalues
+ *
+ * @param value is the value to backtrack to.
+ * @return True if the future value was successully added; false otherwise
+ */
+bool Node::add_future_value(struct future_value fv)
+{
+ uint64_t value = fv.value;
+ modelclock_t expiration = fv.expiration;
+ thread_id_t tid = fv.tid;
+ int idx = -1; /* Highest index where value is found */
+ for (unsigned int i = 0; i < future_values.size(); i++) {
+ if (future_values[i].value == value && future_values[i].tid == tid) {
+ if (expiration <= future_values[i].expiration)
+ return false;
+ idx = i;
+ }
+ }
+ if (idx > future_index) {
+ /* Future value hasn't been explored; update expiration */
+ future_values[idx].expiration = expiration;
+ return true;
+ } else if (idx >= 0 && expiration <= future_values[idx].expiration + get_params()->expireslop) {
+ /* Future value has been explored and is within the "sloppy" window */
+ return false;
+ }
+
+ /* Limit the size of the future-values set */
+ if (get_params()->maxfuturevalues > 0 &&
+ (int)future_values.size() >= get_params()->maxfuturevalues)
+ return false;
+
+ future_values.push_back(fv);
+ return true;
+}
+
+/**
+ * Gets the next 'future_value' from this Node. Only valid for a node where
+ * this->action is a 'read'.
+ * @return The first element in future_values
+ */
+struct future_value Node::get_future_value() const
+{
+ ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
+ return future_values[future_index];
+}
+
+/**
+ * Checks whether the future_values set for this node is empty.
+ * @return true if the future_values set is empty.
+ */
+bool Node::future_value_empty() const
+{
+ return ((future_index + 1) >= ((int)future_values.size()));
+}
+
+/**
+ * Increments the index into the future_values set to explore the next item.
+ * @return Returns false if we have explored all values.
+ */
+bool Node::increment_future_value()
+{
+ DBG();
+ if (future_index < ((int)future_values.size())) {
+ future_index++;
+ return (future_index < ((int)future_values.size()));
+ }
+ return false;
+}
+
+/************************** end future values *********************************/
+
+/*********************** breaking release sequences ***************************/
+
+/**
+ * Add a write ModelAction to the set of writes that may break the release
+ * sequence. This is used during replay exploration of pending release
+ * sequences. This Node must correspond to a release sequence fixup action.
+ *
+ * @param write The write that may break the release sequence. NULL means we
+ * allow the release sequence to synchronize.
+ */
+void Node::add_relseq_break(const ModelAction *write)
+{
+ relseq_break_writes.push_back(write);
+}
+
+/**
+ * Get the write that may break the current pending release sequence,
+ * according to the replay / divergence pattern.
+ *
+ * @return A write that may break the release sequence. If NULL, that means
+ * the release sequence should not be broken.
+ */
+const ModelAction * Node::get_relseq_break() const
+{
+ if (relseq_break_index < (int)relseq_break_writes.size())
+ return relseq_break_writes[relseq_break_index];
+ else
+ return NULL;
+}
+
+/**
+ * Increments the index into the relseq_break_writes set to explore the next
+ * item.
+ * @return Returns false if we have explored all values.
+ */
+bool Node::increment_relseq_break()
+{
+ DBG();
+ if (relseq_break_index < ((int)relseq_break_writes.size())) {
+ relseq_break_index++;
+ return (relseq_break_index < ((int)relseq_break_writes.size()));
+ }
+ return false;
+}
+
+/**
+ * @return True if all writes that may break the release sequence have been
+ * explored
+ */
+bool Node::relseq_break_empty() const
+{
+ return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
+}
+
+/******************* end breaking release sequences ***************************/
+
+/**
+ * Increments some behavior's index, if a new behavior is available
+ * @return True if there is a new behavior available; otherwise false
+ */
+bool Node::increment_behaviors()
+{
+ /* satisfy a different misc_index values */
+ if (increment_misc())
+ return true;
+ /* satisfy a different set of promises */
+ if (increment_promise())
+ return true;
+ /* read from a different value */
+ if (increment_read_from())
+ return true;
+ /* resolve a release sequence differently */
+ if (increment_relseq_break())
+ return true;
+ return false;
+}
+
+NodeStack::NodeStack() :
+ node_list(),
+ head_idx(-1),
+ total_nodes(0)
+{
+ total_nodes++;
+}
+
+NodeStack::~NodeStack()
+{
+ for (unsigned int i = 0; i < node_list.size(); i++)
+ delete node_list[i];
+}
+
+/**
+ * @brief Register the model-checker object with this NodeStack
+ * @param exec The execution structure for the ModelChecker
+ */
+void NodeStack::register_engine(const ModelExecution *exec)
+{
+ this->execution = exec;
+}
+
+const struct model_params * NodeStack::get_params() const
+{
+ return execution->get_params();
+}
+
+void NodeStack::print() const
+{
+ model_print("............................................\n");
+ model_print("NodeStack printing node_list:\n");
+ for (unsigned int it = 0; it < node_list.size(); it++) {
+ if ((int)it == this->head_idx)
+ model_print("vvv following action is the current iterator vvv\n");
+ node_list[it]->print();
+ }
+ model_print("............................................\n");
+}
+
+/** Note: The is_enabled set contains what actions were enabled when
+ * act was chosen. */
+ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
+{
+ DBG();
+
+ if ((head_idx + 1) < (int)node_list.size()) {
+ head_idx++;
+ return node_list[head_idx]->get_action();
+ }