-#define ensureModel(action) \
- if (!modelchecker_started) { \
- if (!model) { \
- snapshot_system_init(10000, 1024, 1024, 40000); \
- model = new ModelChecker(); \
- } \
- model->get_execution()->check_current_action(action); \
- }else { \
- model->switch_to_master(action); \
- }
-
-
-#define ensureModelValue(action, type) \
- if (!modelchecker_started) { \
- if (!model) { \
- snapshot_system_init(10000, 1024, 1024, 40000); \
- model = new ModelChecker(); \
- } \
- model->get_execution()->check_current_action(action); \
- return (type) thread_current()->get_return_value(); \
- } else { \
- return (type) model->switch_to_master(action); \
+static void ensureModel() {
+ if (!model) {
+ snapshot_system_init(10000, 1024, 1024, 40000);
+ model = new ModelChecker();
+ model->startChecker();