model: flesh out check_current_action()

Relies on a stub set_backtracking() function.

diff --git a/model.cc b/model.cc
index 88f6b339231cf6a51df50288e92313682158825a..67222e9f0c5cdf1be3a22edf882910439c72dc39 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -37,10 +37,16 @@ void ModelChecker::add_system_thread(Thread *t)
 
 void ModelChecker::check_current_action(void)
 {
-       if (this->current_action)
-               this->action_trace.push_back(this->current_action);
-       else
+       ModelAction *next = this->current_action;
+
+       if (!next) {
                DEBUG("trying to push NULL action...\n");
+               return;
+       }
+       next->set_node(currentNode);
+       set_backtracking(next);
+       currentNode = currentNode->exploreChild(next->get_tid());
+       this->action_trace.push_back(next);
 }
 
 void ModelChecker::print_trace(void)

diff --git a/model.h b/model.h
index 2762e107f7f66f1b8a34529ec29c2aea3915e565..b6a0004d5a3d119e413d01e5184741930ac5e505 100644 (file)
--- a/model.h
+++ b/model.h
@@ -52,6 +52,7 @@ public:
 
        void set_current_action(ModelAction *act) { current_action = act; }
        void check_current_action(void);
+       void set_backtracking(ModelAction *act);
        void print_trace(void);
 
        int add_thread(Thread *t);