model-checker : add debug information on processes enabled for each state

[simgrid.git] / src / mc / mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index e1b7444..8464bff 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -394,6 +394,13 @@ void MC_ddfs(int search_cycle){
         next_graph_state = MC_state_pair_new();
 
         /* Get enabled process and insert it in the interleave set of the next graph_state */
         next_graph_state = MC_state_pair_new();
 
         /* Get enabled process and insert it in the interleave set of the next graph_state */

+
+        xbt_swag_foreach(process, simix_global->process_list){
+          if(MC_process_is_enabled(process)){
+            XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
+          }
+        }
+

         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_graph_state, process);
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_graph_state, process);