};
static void ensureModel(ModelAction * action) {
- if (!model) {
- if (!model_init) {
+ if (!modelchecker_started) {
+ if (!model) {
snapshot_system_init(10000, 1024, 1024, 40000);
- model_init = new ModelChecker();
+ model = new ModelChecker();
}
- model_init->get_execution()->check_current_action(action);
+ model->get_execution()->check_current_action(action);
} else {
model->switch_to_master(action);
}
/** The model_main function contains the main model checking loop. */
static void model_main()
{
+ modelchecker_started = true;
snapshot_record(0);
model->run();
delete model;
redirect_output();
//Initialize snapshotting library
- if (!model_init)
+ if (!model)
snapshot_system_init(10000, 1024, 1024, 40000);
struct model_params params;
snapshot_stack_init();
- if (!model_init)
+ if (!model)
model = new ModelChecker();
- else
- model = model_init;
model->setParams(params);
install_trace_analyses(model->get_execution());
#include "bugmessage.h"
ModelChecker *model = NULL;
-ModelChecker *model_init = NULL;
+bool modelchecker_started = false;
/** Wrapper to run the user's main function, with appropriate arguments */
void user_main_wrapper(void *)
};
extern ModelChecker *model;
-extern ModelChecker *model_init;
-
+extern bool modelchecker_started;
#endif /* __MODEL_H__ */
int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
cdsc::mutex *m = new cdsc::mutex();
- ModelExecution *execution;
if (!model) {
- if (!model_init) {
- snapshot_system_init(10000, 1024, 1024, 40000);
- model_init = new ModelChecker();
- }
- execution = model_init->get_execution();
- } else
- execution = model->get_execution();
+ snapshot_system_init(10000, 1024, 1024, 40000);
+ model = new ModelChecker();
+ }
+
+ ModelExecution *execution = model->get_execution();
execution->getMutexMap()->put(p_mutex, m);
return 0;