tmp (model)

diff --git a/model.cc b/model.cc
index 4f87da3efdd6b630973901a0f40e09b6420f55af..85ad11aacbf9b255a8372b11e82fc1ad8ad74a7e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -30,6 +30,21 @@ ModelChecker::~ModelChecker()
        delete rootNode;
 }
 
+void ModelChecker::reset_to_initial_state()
+{
+       DEBUG("+++ Resetting to initial state +++\n");
+       std::map<thread_id_t, class Thread *>::iterator it;
+       for (it = thread_map.begin(); it != thread_map.end(); it++) {
+               delete (*it).second;
+       }
+       thread_map.clear();
+       action_trace = new action_list_t();
+       currentNode = rootNode;
+       current_action = NULL;
+       used_thread_id = 1; // ?
+       /* scheduler reset ? */
+}
+
 int ModelChecker::get_next_id()
 {
        return ++used_thread_id;
@@ -163,6 +178,16 @@ void ModelChecker::set_backtracking(ModelAction *act)
        backtrack_list.push_back(back);
 }
 
+Backtrack * ModelChecker::get_next_backtrack()
+{
+       Backtrack *next;
+       if (backtrack_list.empty())
+               return NULL;
+       next = backtrack_list.back();
+       backtrack_list.pop_back();
+       return next;
+}
+
 void ModelChecker::check_current_action(void)
 {
        ModelAction *next = this->current_action;

diff --git a/model.h b/model.h
index ca1de85c980cfa19b2179f9f68ee779bc90097e7..8cfd66f7e3d9dc896e9531fe884e6f74d9ea52a3 100644 (file)
--- a/model.h
+++ b/model.h
@@ -95,6 +95,8 @@ private:
        void set_backtracking(ModelAction *act);
        thread_id_t advance_backtracking_state();
        thread_id_t get_next_replay_thread();
+       Backtrack * get_next_backtrack();
+       void reset_to_initial_state();
 
        class ModelAction *current_action;
        Backtrack *exploring;