projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Doxyfile: exclude malloc.c
[model-checker.git]
/
nodestack.cc
diff --git
a/nodestack.cc
b/nodestack.cc
index 379fb3b1fc15f219cdd870b4976af0e394fd2263..74e6a11a43bbeacab4cc0e3dc39a9ee0dc279760 100644
(file)
--- a/
nodestack.cc
+++ b/
nodestack.cc
@@
-1,21
+1,14
@@
#include "nodestack.h"
#include "action.h"
#include "common.h"
#include "nodestack.h"
#include "action.h"
#include "common.h"
+#include "model.h"
-int Node::total_nodes = 0;
-
-Node::Node(ModelAction *act, Node *parent)
+Node::Node(ModelAction *act, int nthreads)
: action(act),
: action(act),
- num_threads(
parent ? parent->num_threads : 1
),
+ num_threads(
nthreads
),
explored_children(num_threads),
backtrack(num_threads)
{
explored_children(num_threads),
backtrack(num_threads)
{
- total_nodes++;
- if (act && act->get_type() == THREAD_CREATE) {
- num_threads++;
- explored_children.resize(num_threads);
- backtrack.resize(num_threads);
- }
}
Node::~Node()
}
Node::~Node()
@@
-98,8
+91,10
@@
static void clear_node_list(node_list_t *list, node_list_t::iterator start,
}
NodeStack::NodeStack()
}
NodeStack::NodeStack()
+ : total_nodes(0)
{
node_list.push_back(new Node());
{
node_list.push_back(new Node());
+ total_nodes++;
iter = node_list.begin();
}
iter = node_list.begin();
}
@@
-139,7
+134,8
@@
ModelAction * NodeStack::explore_action(ModelAction *act)
/* Record action */
get_head()->explore_child(act);
/* Record action */
get_head()->explore_child(act);
- node_list.push_back(new Node(act, get_head()));
+ node_list.push_back(new Node(act, model->get_num_threads()));
+ total_nodes++;
iter++;
}
return (*iter)->get_action();
iter++;
}
return (*iter)->get_action();