+ MC_UNSET_RAW_MEM;
+
+ /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
+ MC_ignore_local_variable("e", "*");
+ MC_ignore_local_variable("__ex_cleanup", "*");
+ MC_ignore_local_variable("__ex_mctx_en", "*");
+ MC_ignore_local_variable("__ex_mctx_me", "*");
+ MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
+ MC_ignore_local_variable("_log_ev", "*");
+ MC_ignore_local_variable("_throw_ctx", "*");
+ MC_ignore_local_variable("ctx", "*");
+
+ MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
+
+ /* Ignore local variable about time used for tracing */
+ MC_ignore_local_variable("start_time", "*");
+
+ MC_ignore_global_variable("mc_comp_times");
+ MC_ignore_global_variable("mc_snapshot_comparison_time");
+ MC_ignore_global_variable("mc_time");
+ MC_ignore_global_variable("smpi_current_rank");
+ MC_ignore_global_variable("counter"); /* Static variable used for tracing */
+ MC_ignore_global_variable("maestro_stack_start");
+ MC_ignore_global_variable("maestro_stack_end");
+
+ MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
+ MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
+ MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
+ MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
+
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list){
+ MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+ }
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+}
+
+static void MC_init_dot_output(){ /* FIXME : more colors */
+
+ colors[0] = "blue";
+ colors[1] = "red";
+ colors[2] = "green3";
+ colors[3] = "goldenrod";
+ colors[4] = "brown";
+ colors[5] = "purple";
+ colors[6] = "magenta";
+ colors[7] = "turquoise4";
+ colors[8] = "gray25";
+ colors[9] = "forestgreen";
+ colors[10] = "hotpink";
+ colors[11] = "lightblue";
+ colors[12] = "tan";
+
+ 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=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+
+}
+
+/******************************* Core of MC *******************************/
+/**************************************************************************/
+
+void MC_do_the_modelcheck_for_real() {
+
+ MC_SET_RAW_MEM;
+ mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
+ MC_UNSET_RAW_MEM;
+
+ if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
+ if (mc_reduce_kind==e_mc_reduce_unset)
+ mc_reduce_kind=e_mc_reduce_dpor;
+
+ XBT_INFO("Check a safety property");
+ MC_modelcheck_safety();
+
+ } else {
+
+ if (mc_reduce_kind==e_mc_reduce_unset)
+ mc_reduce_kind=e_mc_reduce_none;
+
+ XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
+ MC_automaton_load(_sg_mc_property_file);
+ MC_modelcheck_liveness();
+ }
+}
+
+void MC_modelcheck_safety(void)
+{
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ /* Check if MC is already initialized */
+ if (initial_state_safety)
+ return;
+
+ 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) */
+
+ MC_SET_RAW_MEM;
+
+ /* Initialize statistics */
+ mc_stats = xbt_new0(s_mc_stats_t, 1);
+ mc_stats->state_size = 1;
+
+ /* Create exploration stack */
+ mc_stack_safety = xbt_fifo_new();
+
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
+
+ MC_UNSET_RAW_MEM;
+
+ if(_sg_mc_visited > 0){
+ MC_init();
+ }else{
+ MC_SET_RAW_MEM;
+ MC_init_memory_map_info();
+ MC_get_libsimgrid_plt_section();
+ MC_get_binary_plt_section();
+ MC_UNSET_RAW_MEM;
+ }
+
+ MC_dpor_init();
+
+ MC_SET_RAW_MEM;
+ /* Save the initial state */
+ initial_state_safety = xbt_new0(s_mc_global_t, 1);
+ initial_state_safety->snapshot = MC_take_snapshot(0);
+ MC_UNSET_RAW_MEM;
+
+ MC_dpor();
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ xbt_abort();
+ //MC_exit();
+}
+
+void MC_modelcheck_liveness(){
+
+ 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;
+
+ /* Initialize statistics */
+ mc_stats = xbt_new0(s_mc_stats_t, 1);
+ mc_stats->state_size = 1;
+
+ /* Create exploration stack */
+ mc_stack_liveness = xbt_fifo_new();
+
+ /* Create the initial state */
+ initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+
+ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+ MC_init_dot_output();
+
+ MC_UNSET_RAW_MEM;
+
+ MC_ddfs_init();
+
+ /* We're done */
+ MC_print_statistics(mc_stats);
+ xbt_free(mc_time);
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+}
+
+
+void MC_exit(void)
+{
+ xbt_free(mc_time);
+ MC_memory_exit();
+ //xbt_abort();
+}
+
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
+
+ return simcall->mc_value;
+}
+
+
+int MC_random(int min, int max)
+{
+ /*FIXME: return mc_current_state->executed_transition->random.value;*/
+ return simcall_mc_random(min, max);
+}
+
+/**
+ * \brief Schedules all the process that are ready to run
+ */
+void MC_wait_for_requests(void)
+{
+ smx_process_t process;
+ smx_simcall_t req;
+ unsigned int iter;
+
+ while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
+ SIMIX_process_runall();
+ xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
+ req = &process->simcall;
+ if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
+ SIMIX_simcall_pre(req, 0);
+ }
+ }
+}
+
+int MC_deadlock_check()
+{
+ int deadlock = FALSE;
+ smx_process_t process;
+ if(xbt_swag_size(simix_global->process_list)){
+ deadlock = TRUE;
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(process->simcall.call != SIMCALL_NONE
+ && MC_request_is_enabled(&process->simcall)){
+ deadlock = FALSE;
+ break;
+ }
+ }
+ }
+ return deadlock;
+}
+
+/**
+ * \brief Re-executes from the state at position start all the transitions indicated by
+ * a given model-checker stack.
+ * \param stack The stack with the transitions to execute.
+ * \param start Start index to begin the re-execution.
+ */
+void MC_replay(xbt_fifo_t stack, int start)
+{
+ int raw_mem = (mmalloc_get_current_heap() == raw_heap);
+
+ int value, i = 1, count = 1;
+ char *req_str;
+ smx_simcall_t req = NULL, saved_req = NULL;
+ xbt_fifo_item_t item, start_item;
+ mc_state_t state;
+ smx_process_t process = NULL;
+
+ XBT_DEBUG("**** Begin Replay ****");
+
+ if(start == -1){
+ /* Restore the initial state */
+ MC_restore_snapshot(initial_state_safety->snapshot);
+ /* At the moment of taking the snapshot the raw heap was set, so restoring
+ * it will set it back again, we have to unset it to continue */
+ MC_UNSET_RAW_MEM;
+ }
+
+ start_item = xbt_fifo_get_last_item(stack);
+ if(start != -1){
+ while (i != start){
+ start_item = xbt_fifo_get_prev_item(start_item);
+ i++;
+ }
+ }
+
+ MC_SET_RAW_MEM;
+ xbt_dict_reset(first_enabled_state);
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ char *key = bprintf("%lu", process->pid);
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (item = start_item;
+ item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
+
+ state = (mc_state_t) xbt_fifo_get_item_content(item);
+ saved_req = MC_state_get_executed_request(state, &value);
+
+ MC_SET_RAW_MEM;
+ char *key = bprintf("%lu", saved_req->issuer->pid);
+ xbt_dict_remove(first_enabled_state, key);
+ xbt_free(key);
+ MC_UNSET_RAW_MEM;
+
+ if(saved_req){
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ req = &saved_req->issuer->simcall;
+
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Replay: %s (%p)", req_str, state);
+ xbt_free(req_str);
+ }
+ }
+
+ SIMIX_simcall_pre(req, value);
+ MC_wait_for_requests();
+
+ count++;
+
+ MC_SET_RAW_MEM;
+ /* Insert in dict all enabled processes */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+ char *key = bprintf("%lu", process->pid);
+ if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ }
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+ /* Update statistics */
+ mc_stats->visited_states++;
+ mc_stats->executed_transitions++;
+
+ }
+
+ XBT_DEBUG("**** End Replay ****");
+
+ if(raw_mem)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+
+}
+
+void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
+{
+
+ initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ int value;
+ char *req_str;
+ smx_simcall_t req = NULL, saved_req = NULL;
+ xbt_fifo_item_t item;
+ mc_state_t state;
+ mc_pair_t pair;
+ int depth = 1;
+
+ XBT_DEBUG("**** Begin Replay ****");
+
+ /* Restore the initial state */
+ MC_restore_snapshot(initial_state_liveness->snapshot);
+
+ /* At the moment of taking the snapshot the raw heap was set, so restoring
+ * it will set it back again, we have to unset it to continue */
+ if(!initial_state_liveness->raw_mem_set)
+ MC_UNSET_RAW_MEM;
+
+ if(all_stack){
+
+ item = xbt_fifo_get_last_item(stack);
+
+ while(depth <= xbt_fifo_size(stack)){
+
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+ state = (mc_state_t) pair->graph_state;
+
+ if(pair->requests > 0){
+
+ saved_req = MC_state_get_executed_request(state, &value);
+ //XBT_DEBUG("SavedReq->call %u", saved_req->call);