Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix an external ref
[simgrid.git] / src / mc / mc_dpor.c
index c67d36d..bdc859e 100644 (file)
@@ -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)