projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
action: add get_node() accessor
[model-checker.git]
/
tree.cc
diff --git
a/tree.cc
b/tree.cc
index ce79f755eeea010897bc117f47deab11bb53786e..c161ca838de4947fbfc1ca486aaaf0400ca1475e 100644
(file)
--- a/
tree.cc
+++ b/
tree.cc
@@
-1,11
+1,19
@@
#include "tree.h"
#include "tree.h"
+#include "action.h"
int TreeNode::totalNodes = 0;
int TreeNode::totalNodes = 0;
-TreeNode::TreeNode(TreeNode *par)
+TreeNode::TreeNode(TreeNode *par
, ModelAction *act
)
{
TreeNode::totalNodes++;
this->parent = par;
{
TreeNode::totalNodes++;
this->parent = par;
+ if (!parent) {
+ num_threads = 1;
+ } else {
+ num_threads = parent->num_threads;
+ if (act && act->get_type() == THREAD_CREATE)
+ num_threads++;
+ }
}
TreeNode::~TreeNode() {
}
TreeNode::~TreeNode() {
@@
-15,14
+23,15
@@
TreeNode::~TreeNode() {
delete it->second;
}
delete it->second;
}
-TreeNode * TreeNode::explore
Child(thread_id_t id
)
+TreeNode * TreeNode::explore
_child(ModelAction *act
)
{
TreeNode *n;
std::set<int>::iterator it;
{
TreeNode *n;
std::set<int>::iterator it;
+ thread_id_t id = act->get_tid();
int i = id_to_int(id);
if (!hasBeenExplored(id)) {
int i = id_to_int(id);
if (!hasBeenExplored(id)) {
- n = new TreeNode(this);
+ n = new TreeNode(this
, act
);
children[i] = n;
} else {
n = children[i];
children[i] = n;
} else {
n = children[i];
@@
-55,3
+64,8
@@
TreeNode * TreeNode::getRoot()
return parent->getRoot();
return this;
}
return parent->getRoot();
return this;
}
+
+bool TreeNode::is_enabled(Thread *t)
+{
+ return id_to_int(t->get_id()) < num_threads;
+}