int _sg_mc_timeout=0;
int _sg_mc_max_depth=1000;
int _sg_mc_visited=0;
+char *_sg_mc_dot_output_file = NULL;
extern int _sg_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
_sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
}
+void _mc_cfg_cb_dot_output(const char *name, int pos) {
+ if (_sg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a file name for a dot output of graph state 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.");
+ }
+ _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
+}
/* MC global data structures */
extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
+FILE *dot_output = NULL;
+const char* colors[10];
+
xbt_automaton_t _mc_property_automaton = NULL;
/* Static functions */
MC_SET_RAW_MEM;
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
MC_UNSET_RAW_MEM;
+
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
if (mc_reduce_kind==e_mc_reduce_unset)
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- mc_time = xbt_new0(double, simix_process_maxpid);
-
- /* mc_time refers to clock for each process -> ignore it for heap comparison */
- int i;
- for(i = 0; i<simix_process_maxpid; i++)
- MC_ignore_heap(&(mc_time[i]), sizeof(double));
-
compare = 0;
/* Initialize the data structures that must be persistent across every
MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time));
+ MC_ignore_data_bss(&mc_time, sizeof(mc_time));
if(raw_mem_set)
MC_SET_RAW_MEM;
}
+void MC_init_dot_output(){
+
+ colors[0] = "blue";
+ colors[1] = "red";
+ colors[2] = "green";
+ colors[3] = "pink";
+ colors[4] = "brown";
+ colors[5] = "purple";
+ colors[6] = "yellow";
+ colors[7] = "orange";
+
+ dot_output = fopen(_sg_mc_dot_output_file, "w");
+
+ if(dot_output == NULL){
+ perror("Error open dot output file");
+ xbt_abort();
+ }
+
+ fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.20; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+
+}
+
void MC_modelcheck_safety(void)
{
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
mc_time = xbt_new0(double, simix_process_maxpid);
+ /* mc_time refers to clock for each process -> ignore it for heap comparison */
+ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
MC_init();
+
+ mc_time = xbt_new0(double, simix_process_maxpid);
+
+ /* mc_time refers to clock for each process -> ignore it for heap comparison */
+ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
MC_SET_RAW_MEM;
void MC_exit(void)
{
+ MC_SET_RAW_MEM;
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+ fprintf(dot_output, "}\n");
+ fclose(dot_output);
+ }
+ MC_UNSET_RAW_MEM;
+
xbt_free(mc_time);
MC_memory_exit();
xbt_abort();
}
-int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+int SIMIX_pre_mc_random(smx_simcall_t simcall){
return simcall->mc_value;
}
-int MC_random(int min, int max)
+int MC_random(void)
{
/*FIXME: return mc_current_state->executed_transition->random.value;*/
- return simcall_mc_random(min, max);
+ return simcall_mc_random();
}
/**