+/**
+ * Checks if the backtracking set is empty.
+ * @return true if the backtracking set is empty
+ */
+bool Node::backtrack_empty() const
+{
+ return (numBacktracks == 0);
+}
+
+void Node::explore(thread_id_t tid)
+{
+ int i = id_to_int(tid);
+ ASSERT(i < ((int)backtrack.size()));
+ if (backtrack[i]) {
+ backtrack[i] = false;
+ numBacktracks--;
+ }
+ explored_children[i] = true;
+}
+
+/**
+ * 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;
+ }
+
+ explore(act->get_tid());
+}
+
+/**
+ * Records a backtracking reference for a thread choice within this Node.
+ * Provides feedback as to whether this thread choice is already set for
+ * backtracking.
+ * @return false if the thread was already set to be backtracked, true
+ * otherwise
+ */
+bool Node::set_backtrack(thread_id_t id)
+{
+ int i = id_to_int(id);
+ ASSERT(i < ((int)backtrack.size()));
+ if (backtrack[i])
+ return false;
+ backtrack[i] = true;
+ numBacktracks++;
+ return true;
+}
+
+thread_id_t Node::get_next_backtrack()
+{
+ /** @todo Find next backtrack */
+ unsigned int i;
+ for (i = 0; i < backtrack.size(); i++)
+ if (backtrack[i] == true)
+ break;
+ /* Backtrack set was empty? */
+ ASSERT(i != backtrack.size());
+
+ backtrack[i] = false;
+ numBacktracks--;
+ return int_to_id(i);
+}
+
+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 **********************************/
+