merging stuff...made need to clean up some stuff...but need to push it somewhere...

[model-checker.git] / tree.cc

diff --git a/tree.cc b/tree.cc
index f42202ec1bfd46f9935805eceafbc8930f4d7aff..263655c75330387b7fd006750de149f77c7df113 100644 (file)
--- a/tree.cc
+++ b/tree.cc
@@ -1,55 +1,71 @@
 #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;
+       if (!parent) {
+               num_threads = 1;
+       } else {
+               num_threads = parent->num_threads;
+               if (act && act->get_type() == THREAD_CREATE)
+                       num_threads++;
+       }
 }
 
 TreeNode::~TreeNode() {
-       std::map<tree_t, class TreeNode *>::iterator it;
+       std::map<int, class TreeNode *, std::less< int >, MyAlloc< std::pair< const int, class TreeNode * > > >::iterator it;
 
        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;
-       std::set<tree_t >::iterator it;
+       std::set<int, std::less< int >, MyAlloc< int > >::iterator it;
+       thread_id_t id = act->get_tid();
+       int i = id_to_int(id);
 
        if (!hasBeenExplored(id)) {
-               n = new TreeNode(this);
-               children[id] = n;
+               n = new TreeNode(this, act);
+               children[i] = n;
        } else {
-               n = children[id];
+               n = children[i];
        }
-       if ((it = backtrack.find(id)) != backtrack.end())
+       if ((it = backtrack.find(i)) != backtrack.end())
                backtrack.erase(it);
 
        return n;
 }
 
-int TreeNode::setBacktrack(tree_t id)
+int TreeNode::setBacktrack(thread_id_t id)
 {
-       if (backtrack.find(id) == backtrack.end())
+       int i = id_to_int(id);
+       if (backtrack.find(i) != backtrack.end())
                return 1;
-       backtrack.insert(id);
+       backtrack.insert(i);
        return 0;
 }
 
-tree_t TreeNode::getNextBacktrack()
+thread_id_t TreeNode::getNextBacktrack()
 {
        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;
 }
+
+bool TreeNode::is_enabled(Thread *t)
+{
+       return id_to_int(t->get_id()) < num_threads;
+}