/* 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,
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;
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:");
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;
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)