+ 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;
+}
+
+Thread * ModelChecker::schedule_next_thread()
+{
+ Thread *t;
+ if (nextThread == THREAD_ID_T_NONE)
+ return NULL;
+ t = thread_map[nextThread];
+ if (t == NULL)
+ DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+ return t;