As I add more complicated backtracking and may-read-from relationships,
each Node might need some structural information to be able to reach its
parent Node.
To support this:
* the NodeStack should provide the parent information via Node constructor
* the Node should provide a get_parent() method
#include "model.h"
/** @brief Node constructor */
#include "model.h"
/** @brief Node constructor */
-Node::Node(ModelAction *act, int nthreads)
+Node::Node(ModelAction *act, Node *par, int nthreads)
num_threads(nthreads),
explored_children(num_threads),
backtrack(num_threads),
num_threads(nthreads),
explored_children(num_threads),
backtrack(num_threads),
/* Record action */
get_head()->explore_child(act);
/* Record action */
get_head()->explore_child(act);
- node_list.push_back(new Node(act, model->get_num_threads()));
+ node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
total_nodes++;
iter++;
return NULL;
total_nodes++;
iter++;
return NULL;
- Node(ModelAction *act = NULL, int nthreads = 1);
+ Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1);
~Node();
/* return true = thread choice has already been explored */
bool has_been_explored(thread_id_t tid);
~Node();
/* return true = thread choice has already been explored */
bool has_been_explored(thread_id_t tid);
bool is_enabled(Thread *t);
ModelAction * get_action() { return action; }
bool is_enabled(Thread *t);
ModelAction * get_action() { return action; }
+ /** @return the parent Node to this Node; that is, the action that
+ * occurred previously in the stack. */
+ Node * get_parent() const { return parent; }
+
void add_read_from(ModelAction *act);
void print();
void add_read_from(ModelAction *act);
void print();
void explore(thread_id_t tid);
ModelAction *action;
void explore(thread_id_t tid);
ModelAction *action;
int num_threads;
std::vector< bool, MyAlloc<bool> > explored_children;
std::vector< bool, MyAlloc<bool> > backtrack;
int num_threads;
std::vector< bool, MyAlloc<bool> > explored_children;
std::vector< bool, MyAlloc<bool> > backtrack;