From 6b3cc5b800966b58d330bf516d92a17b4e2bee9d Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 3 May 2012 23:27:46 -0700
Subject: [PATCH] tree: revise arguments (use Thread, ModelAction)
Preparation for other changes to the TreeNode.
---
model.cc | 11 ++++++-----
tree.cc | 8 +++++---
tree.h | 6 ++++--
3 files changed, 15 insertions(+), 10 deletions(-)
diff --git a/model.cc b/model.cc
index aba3e8b..0084e74 100644
--- a/model.cc
+++ b/model.cc
@@ -43,7 +43,7 @@ ModelChecker::ModelChecker()
this->exploring = NULL;
this->nextThread = THREAD_ID_T_NONE;
- rootNode = new TreeNode(NULL);
+ rootNode = new TreeNode();
currentNode = rootNode;
action_trace = new action_list_t();
}
@@ -182,6 +182,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
{
ModelAction *prev;
TreeNode *node;
+ Thread *t = get_thread(act->get_tid());
prev = get_last_conflict(act);
if (prev == NULL)
@@ -190,14 +191,14 @@ void ModelChecker::set_backtracking(ModelAction *act)
node = prev->get_node();
/* Check if this has been explored already */
- if (node->hasBeenExplored(act->get_tid()))
+ if (node->hasBeenExplored(t->get_id()))
return;
/* If this is a new backtracking point, mark the tree */
- if (node->setBacktrack(act->get_tid()) != 0)
+ if (node->setBacktrack(t->get_id()) != 0)
return;
DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
- prev->get_tid(), act->get_tid());
+ prev->get_tid(), t->get_id());
if (DBG_ENABLED()) {
prev->print();
act->print();
@@ -229,7 +230,7 @@ void ModelChecker::check_current_action(void)
nextThread = advance_backtracking_state();
next->set_node(currentNode);
set_backtracking(next);
- currentNode = currentNode->exploreChild(next->get_tid());
+ currentNode = currentNode->explore_child(next);
this->action_trace->push_back(next);
}
diff --git a/tree.cc b/tree.cc
index ce79f75..57e0c13 100644
--- a/tree.cc
+++ b/tree.cc
@@ -1,8 +1,9 @@
#include "tree.h"
+#include "action.h"
int TreeNode::totalNodes = 0;
-TreeNode::TreeNode(TreeNode *par)
+TreeNode::TreeNode(TreeNode *par, ModelAction *act)
{
TreeNode::totalNodes++;
this->parent = par;
@@ -15,14 +16,15 @@ TreeNode::~TreeNode() {
delete it->second;
}
-TreeNode * TreeNode::exploreChild(thread_id_t id)
+TreeNode * TreeNode::explore_child(ModelAction *act)
{
TreeNode *n;
std::set<int>::iterator it;
+ thread_id_t id = act->get_tid();
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];
diff --git a/tree.h b/tree.h
index 9fba203..1752d3f 100644
--- a/tree.h
+++ b/tree.h
@@ -5,6 +5,8 @@
#include <map>
#include "threads.h"
+class ModelAction;
+
/*
* An n-ary tree
*
@@ -13,10 +15,10 @@
*/
class TreeNode {
public:
- TreeNode(TreeNode *par);
+ TreeNode(TreeNode *par = NULL, ModelAction *act = NULL);
~TreeNode();
bool hasBeenExplored(thread_id_t id) { return children.find(id_to_int(id)) != children.end(); }
- TreeNode * exploreChild(thread_id_t id);
+ TreeNode * explore_child(ModelAction *act);
thread_id_t getNextBacktrack();
/* Return 1 if already in backtrack, 0 otherwise */
--
2.34.1