+ 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;
+}
+
+
+/**
+ * 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(uint64_t value, modelclock_t expiration)
+{
+ 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) {
+ 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 + model->params.expireslop) {
+ /* Future value has been explored and is within the "sloppy" window */
+ return false;
+ }
+
+ /* Limit the size of the future-values set */
+ if (model->params.maxfuturevalues > 0 &&
+ (int)future_values.size() >= model->params.maxfuturevalues)
+ return false;
+
+ struct future_value newfv = {value, expiration};
+ future_values.push_back(newfv);
+ return true;
+}
+
+/**
+ * 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()));
+}
+
+/**
+ * Checks if the Thread associated with this thread ID has been explored from
+ * this Node already.
+ * @param tid is the thread ID to check
+ * @return true if this thread choice has been explored already, false
+ * otherwise
+ */
+bool Node::has_been_explored(thread_id_t tid) const
+{
+ int id = id_to_int(tid);
+ return explored_children[id];
+}
+
+/**
+ * Checks if the backtracking set is empty.
+ * @return true if the backtracking set is empty
+ */
+bool Node::backtrack_empty() const
+{
+ return (numBacktracks == 0);
+}
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
+bool Node::read_from_empty() const
+{
+ return ((read_from_index + 1) >= may_read_from.size());
+}
+
+/**
+ * Mark the appropriate backtracking information for exploring a thread choice.
+ * @param act The ModelAction to explore
+ */
+void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled)
+{
+ if (!enabled_array)
+ enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads);
+ if (is_enabled != NULL)
+ memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads);
+ else {
+ for (int i = 0; i < num_threads; i++)
+ enabled_array[i] = THREAD_DISABLED;
+ }
+