void _mc_cfg_cb_property(const char *name, int pos);
void _mc_cfg_cb_timeout(const char *name, int pos);
void _mc_cfg_cb_max_depth(const char *name, int pos);
-void _mc_cfg_cb_stateful(const char *name, int pos);
+void _mc_cfg_cb_visited(const char *name, int pos);
XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
}
}
- if(_surf_mc_stateful > 0 || _surf_mc_property_file)
+ if(_surf_mc_visited > 0 || _surf_mc_property_file)
snapshot->stacks = take_snapshot_stacks(heap);
free_memory_map(maps);
static int is_visited_state(){
- if(_surf_mc_stateful == 0)
+ if(_surf_mc_visited == 0)
return 0;
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
}
}
- if(xbt_dynar_length(visited_states) == _surf_mc_stateful){
+ if(xbt_dynar_length(visited_states) == _surf_mc_visited){
mc_snapshot_t state_to_remove = NULL;
xbt_dynar_shift(visited_states, &state_to_remove);
MC_free_snapshot(state_to_remove);
xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
}
-void _mc_cfg_cb_stateful(const char *name, int pos) {
+void _mc_cfg_cb_visited(const char *name, int pos) {
if (_surf_init_status && !_surf_do_model_check) {
- xbt_die("You are trying to change stateful mode after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
}
- _surf_mc_stateful= xbt_cfg_get_int(_surf_cfg_set, name);
+ _surf_mc_visited= xbt_cfg_get_int(_surf_cfg_set, name);
xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
}
MC_UNSET_RAW_MEM;
- if(_surf_mc_stateful > 0){
+ if(_surf_mc_visited > 0){
MC_init();
}else{
MC_init_memory_map_info();
int visited(xbt_state_t st){
- if(_surf_mc_stateful == 0)
+ if(_surf_mc_visited == 0)
return 0;
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
}
}
- if(xbt_dynar_length(visited_pairs) == _surf_mc_stateful){
+ if(xbt_dynar_length(visited_pairs) == _surf_mc_visited){
xbt_dynar_remove_at(visited_pairs, 0, NULL);
}
extern char* _surf_mc_property_file;
extern int _surf_mc_timeout;
extern int _surf_mc_max_depth;
-extern int _surf_mc_stateful;
+extern int _surf_mc_visited;
/****** Core dump ******/
_mc_cfg_cb_max_depth, NULL);
xbt_cfg_setdefault_int(_surf_cfg_set, "model-check/max_depth", 1000);
- /* Set number of visited state stored in stateful mode */
- xbt_cfg_register(&_surf_cfg_set, "model-check/stateful",
- "Specify the number of visited state stored in stateful mode. If value=5, the last 5 visited states are stored",
+ /* Set number of visited state stored for state comparison reduction*/
+ xbt_cfg_register(&_surf_cfg_set, "model-check/visited",
+ "Specify the number of visited state stored for state comparison reduction. If value=5, the last 5 visited states are stored",
xbt_cfgelm_int, NULL, 0, 1,
- _mc_cfg_cb_stateful, NULL);
- xbt_cfg_setdefault_int(_surf_cfg_set, "model-check/stateful", 0);
+ _mc_cfg_cb_visited, NULL);
+ xbt_cfg_setdefault_int(_surf_cfg_set, "model-check/visited", 0);
#endif
/* do verbose-exit */
char* _surf_mc_property_file=NULL;
int _surf_mc_timeout=0;
int _surf_mc_max_depth=1000;
-int _surf_mc_stateful=0;
+int _surf_mc_visited=0;
/* Declare xbt_preinit and xbt_postexit as constructor/destructor of the library.
* This is crude and rather compiler-specific, unfortunately.