X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.h;h=62b227e4bcdce915125e9c8b7f9a877c94ee9529;hp=882ca069b32a9d8d7903805bba0986daa96d9f3e;hb=d02738576d6be6a387d1aaf903b98c94a0a329c6;hpb=286195618e981ea2b31036bc4f403382a2dd4835

diff --git a/model.h b/model.h
index 882ca069..62b227e4 100644
--- a/model.h
+++ b/model.h
@@ -16,6 +16,7 @@
 #include "context.h"
 #include "params.h"
 #include "classlist.h"
+#include "snapshot-interface.h"
 
 typedef SnapList<ModelAction *> action_list_t;
 
@@ -34,9 +35,6 @@ public:
 	model_params * getParams();
 	void run();
 
-	/** Restart the model checker, intended for pluggins. */
-	void restart();
-
 	/** Exit the model checker, intended for pluggins. */
 	void exit_model_checker();
 
@@ -63,14 +61,13 @@ public:
 	model_params params;
 	void add_trace_analysis(TraceAnalysis *a) {     trace_analyses.push_back(a); }
 	void set_inspect_plugin(TraceAnalysis *a) {     inspect_plugin=a;       }
-	void startMainThread();
 	void startChecker();
 	Thread * getInitThread() {return init_thread;}
 	Scheduler * getScheduler() {return scheduler;}
 	MEMALLOC
 private:
-	/** Flag indicates whether to restart the model checker. */
-	bool restart_flag;
+	/** Snapshot id we return to restart. */
+	snapshot_id snapshot;
 
 	/** The scheduler to use: tracks the running/ready Threads */
 	Scheduler * const scheduler;
@@ -82,7 +79,7 @@ private:
 
 	unsigned int get_num_threads() const;
 
-	bool next_execution();
+	void finish_execution(bool moreexecutions);
 	bool should_terminate_execution();
 
 	Thread * get_next_thread();
@@ -92,8 +89,6 @@ private:
 
 	ModelVector<TraceAnalysis *> trace_analyses;
 
-	/** @bref Implement restart. */
-	void do_restart();
 	/** @bref Plugin that can inspect new actions. */
 	TraceAnalysis *inspect_plugin;
 	/** @brief The cumulative execution stats */