model: privatize some functions

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index fd893c78b42a85cec0bc2668102600f1a4fa63c8..72610f6581e500231941a1613274891556687f3f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2510,9 +2510,24 @@ bool ModelChecker::take_step() {
        return (Thread::swap(&system_context, next) == 0);
 }
 
-/** Runs the current execution until threre are no more steps to take. */
-void ModelChecker::finish_execution() {
-       DBG();
+/** Wrapper to run the user's main function, with appropriate arguments */
+void user_main_wrapper(void *)
+{
+       user_main(model->params.argc, model->params.argv);
+}
+
+/** @brief Run ModelChecker for the user program */
+void ModelChecker::run()
+{
+       do {
+               thrd_t user_thread;
+
+               /* Start user program */
+               add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+
+               /* Wait for all threads to complete */
+               while (take_step());
+       } while (next_execution());
 
-       while (take_step());
+       print_stats();
 }