+static void param_defaults(struct model_params *params)
+{
+ params->maxreads = 0;
+ params->maxfuturedelay = 6;
+ params->fairwindow = 0;
+ params->yieldon = false;
+ params->yieldblock = false;
+ params->enabledcount = 1;
+ params->bound = 0;
+ params->maxfuturevalues = 0;
+ params->expireslop = 4;
+ params->verbose = !!DBG_ENABLED();
+ params->uninitvalue = 0;
+ params->maxexecutions = 0;
+}
+
+static void model_main()
+{
+ struct model_params params;
+
+ param_defaults(¶ms);
+
+ //parse_options(¶ms, main_argc, main_argv);
+
+ //Initialize race detector
+ initRaceDetector();
+
+ snapshot_stack_init();
+
+ model = new ModelChecker(params); // L: Model thread is created
+// install_trace_analyses(model->get_execution()); L: disable plugin
+
+ snapshot_record(0);
+ model->run();
+ delete model;
+
+ DEBUG("Exiting\n");
+}
+