-/** 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());