node: do not use static member variable

Static member variables of a class are going to be snapshotted. Move them so
they aren't static in order to prevent this.

(This can create interesting behavior, where the "total number of nodes
created" is decreasing at times!)

diff --git a/model.cc b/model.cc
index 2ffa22a1028a8008c1c60e52e8e9fee627fac766..70440f5050b3c3bc0adaf157e44db0959f3c6476 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -265,7 +265,7 @@ void ModelChecker::print_summary(void)
 {
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
-       printf("Total nodes created: %d\n", Node::get_total_nodes());
+       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 
        scheduler->print();
 

diff --git a/nodestack.cc b/nodestack.cc
index df5fc633ac37aba0b6df464f51be996ab8403eb6..74e6a11a43bbeacab4cc0e3dc39a9ee0dc279760 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -3,15 +3,12 @@
 #include "common.h"
 #include "model.h"
 
-int Node::total_nodes = 0;
-
 Node::Node(ModelAction *act, int nthreads)
        : action(act),
        num_threads(nthreads),
        explored_children(num_threads),
        backtrack(num_threads)
 {
-       total_nodes++;
 }
 
 Node::~Node()
@@ -94,8 +91,10 @@ static void clear_node_list(node_list_t *list, node_list_t::iterator start,
 }
 
 NodeStack::NodeStack()
+       : total_nodes(0)
 {
        node_list.push_back(new Node());
+       total_nodes++;
        iter = node_list.begin();
 }
 
@@ -136,6 +135,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
                /* Record action */
                get_head()->explore_child(act);
                node_list.push_back(new Node(act, model->get_num_threads()));
+               total_nodes++;
                iter++;
        }
        return (*iter)->get_action();

diff --git a/nodestack.h b/nodestack.h
index cf3c6db146675c0cb7f41d994f988925209fc976..59da8a1f1f04971f709cfe0dd7b79d187ed4593b 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -26,13 +26,10 @@ public:
 
        void print();
 
-       static int get_total_nodes() { return total_nodes; }
-
        MEMALLOC
 private:
        void explore(thread_id_t tid);
 
-       static int total_nodes;
        ModelAction *action;
        int num_threads;
        std::vector< bool, MyAlloc<bool> > explored_children;
@@ -50,12 +47,16 @@ public:
        Node * get_next();
        void reset_execution();
 
+       int get_total_nodes() { return total_nodes; }
+
        void print();
 
        MEMALLOC
 private:
        node_list_t node_list;
        node_list_t::iterator iter;
+
+       int total_nodes;
 };
 
 #endif /* __NODESTACK_H__ */