clean out includes, etc.
[model-checker.git] / execution.cc
index 0ec13900b4e56b4bde68db8978bd9d5202b28946..f0288d2e7de1eb2d23bc32c95a3c01fb8c7d1683 100644 (file)
@@ -5,18 +5,15 @@
 #include <stdarg.h>
 
 #include "execution.h"
-#include "model.h"
 #include "action.h"
 #include "nodestack.h"
 #include "schedule.h"
-#include "snapshot-interface.h"
 #include "common.h"
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
 #include "datarace.h"
 #include "threads-model.h"
-#include "output.h"
 #include "bugmessage.h"
 
 #define INITIAL_THREAD_ID      0
@@ -31,7 +28,6 @@ struct model_snapshot_members {
                used_sequence_numbers(0),
                next_backtrack(NULL),
                bugs(),
-               stats(),
                failed_promise(false),
                too_many_reads(false),
                no_valid_reads(false),
@@ -49,7 +45,6 @@ struct model_snapshot_members {
        modelclock_t used_sequence_numbers;
        ModelAction *next_backtrack;
        SnapVector<bug_message *> bugs;
-       struct execution_stats stats;
        bool failed_promise;
        bool too_many_reads;
        bool no_valid_reads;
@@ -82,6 +77,7 @@ ModelExecution::ModelExecution(struct model_params *params, Scheduler *scheduler
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
        thread_map->put(id_to_int(model_thread->get_id()), model_thread);
+       scheduler->register_engine(this);
 }
 
 /** @brief Destructor */
@@ -911,7 +907,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
        case THREAD_CREATE: {
                thrd_t *thrd = (thrd_t *)curr->get_location();
                struct thread_params *params = (struct thread_params *)curr->get_value();
-               Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
+               Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
                add_thread(th);
                th->set_creation(curr);
                /* Promises can be satisfied by children */