projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
nodestack: add Node::get_parent() function
[model-checker.git]
/
nodestack.h
diff --git
a/nodestack.h
b/nodestack.h
index 74ac245f3b3b00331a3328482d7c21c47bdc7cdb..11440e5ae5680af381842c3ef81e637dd0e16ee9 100644
(file)
--- a/
nodestack.h
+++ b/
nodestack.h
@@
-18,7
+18,7
@@
typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction
class Node {
public:
class Node {
public:
- 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);
@@
-31,6
+31,10
@@
public:
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();
@@
-40,6
+44,7
@@
private:
void explore(thread_id_t tid);
ModelAction *action;
void explore(thread_id_t tid);
ModelAction *action;
+ Node *parent;
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;