main, model: move main execution loop into ModelChecker class

[c11tester.git] / model.h

diff --git a/model.h b/model.h
index dc6ef6add21045042ed42a29882e3ad9a38ac34e..2b878b3f3ae71b475db5466c27b2c817b1118506 100644 (file)
--- a/model.h
+++ b/model.h
@@ -70,6 +70,8 @@ public:
        bool isfinalfeasible();
        void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 
+       void finish_execution();
+
        MEMALLOC
 private:
        int next_thread_id;
@@ -86,6 +88,8 @@ private:
         */
        void set_current_action(ModelAction *act) { current_action = act; }
 
+       bool take_step();
+
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
        thread_id_t get_next_replay_thread();