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 f42202ec1bfd46f9935805eceafbc8930f4d7aff..c161ca838de4947fbfc1ca486aaaf0400ca1475e 100644
(file)
--- a/
tree.cc
+++ b/
tree.cc
@@
-1,55
+1,71
@@
#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() {
- std::map<
tree_
t, class TreeNode *>::iterator it;
+ std::map<
in
t, class TreeNode *>::iterator it;
for (it = children.begin(); it != children.end(); it++)
delete it->second;
}
for (it = children.begin(); it != children.end(); it++)
delete it->second;
}
-TreeNode *
TreeNode::exploreChild(tree_t id
)
+TreeNode *
TreeNode::explore_child(ModelAction *act
)
{
TreeNode *n;
{
TreeNode *n;
- std::set<tree_t >::iterator it;
+ std::set<int>::iterator it;
+ thread_id_t id = act->get_tid();
+ int i = id_to_int(id);
if (!hasBeenExplored(id)) {
if (!hasBeenExplored(id)) {
- n = new TreeNode(this);
- children[i
d
] = n;
+ n = new TreeNode(this
, act
);
+ children[i] = n;
} else {
} else {
- n = children[i
d
];
+ n = children[i];
}
}
- if ((it = backtrack.find(i
d
)) != backtrack.end())
+ if ((it = backtrack.find(i)) != backtrack.end())
backtrack.erase(it);
return n;
}
backtrack.erase(it);
return n;
}
-int TreeNode::setBacktrack(t
ree
_t id)
+int TreeNode::setBacktrack(t
hread_id
_t id)
{
{
- if (backtrack.find(id) == backtrack.end())
+ int i = id_to_int(id);
+ if (backtrack.find(i) != backtrack.end())
return 1;
return 1;
- backtrack.insert(i
d
);
+ backtrack.insert(i);
return 0;
}
return 0;
}
-t
ree
_t TreeNode::getNextBacktrack()
+t
hread_id
_t TreeNode::getNextBacktrack()
{
if (backtrack.empty())
{
if (backtrack.empty())
- return
NULL
;
- return
*backtrack.begin(
);
+ return
THREAD_ID_T_NONE
;
+ return
int_to_id(*backtrack.begin()
);
}
}
-TreeNode *TreeNode::getRoot()
+TreeNode *
TreeNode::getRoot()
{
if (parent)
return parent->getRoot();
return this;
}
{
if (parent)
return parent->getRoot();
return this;
}
+
+bool TreeNode::is_enabled(Thread *t)
+{
+ return id_to_int(t->get_id()) < num_threads;
+}