X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d18b8e9f99926675bc2ae15d0b0ee1adf504633c..e9efa61bd5941f4d58bb736d74b4348942cadb0a:/src/mc/mc_dpor.c diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index c67d36de1f..bdc859e6e5 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -27,7 +27,11 @@ void MC_dpor_init() /* Schedule all the processes to detect the transitions of the initial state */ DEBUG0("**************************************************"); DEBUG0("Initial state"); - MC_schedule_enabled_processes(); + + while(xbt_swag_size(simix_global->process_to_run)){ + MC_schedule_enabled_processes(); + MC_execute_surf_actions(); + } MC_SET_RAW_MEM; MC_trans_compute_enabled(initial_state->enabled_transitions, @@ -102,8 +106,12 @@ void MC_dpor(void) of the transition */ DEBUG1("Executing transition %s", trans->name); SIMIX_process_schedule(trans->process); - MC_execute_surf_actions(); /* Do surf's related black magic */ - MC_schedule_enabled_processes(); + MC_execute_surf_actions(); + + while(xbt_swag_size(simix_global->process_to_run)){ + MC_schedule_enabled_processes(); + MC_execute_surf_actions(); + } /* Calculate the enabled transitions set of the next state */ MC_SET_RAW_MEM; @@ -145,7 +153,8 @@ void MC_dpor(void) INFO0("**************************"); INFO0("Locked transitions:"); xbt_setset_foreach(mc_current_state->transitions, cursor, trans){ - INFO1("%s", trans->name); + INFO3("%s [src=%p, dst=%p]", trans->name, trans->wait.comm->src_proc, + trans->wait.comm->dst_proc); } INFO0("Counter-example execution trace:"); @@ -158,8 +167,10 @@ void MC_dpor(void) mc_transition_t q = NULL; xbt_fifo_item_t item = NULL; mc_state_t state = NULL; - - //MC_show_stack(mc_stack); + + /* + INFO0("*********************************"); + MC_show_stack(mc_stack);*/ /* Trash the current state, no longer needed */ MC_SET_RAW_MEM; @@ -176,10 +187,10 @@ void MC_dpor(void) q = mc_current_state->executed_transition; xbt_fifo_foreach(mc_stack, item, state, mc_state_t){ if(MC_transition_depend(q, state->executed_transition)){ - DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q); xbt_setset_foreach(state->enabled_transitions, cursor, trans){ if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){ - DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans); + DEBUG3("%s depend with %s at %p", q->name, + state->executed_transition->name, state); xbt_setset_foreach(state->enabled_transitions, cursor, trans){ if(trans->process == q->process)