model-checker : use the right heap

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

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index d034675..37a6f90 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -248,11 +248,6 @@ void MC_pre_modelcheck_comm_determinism(void)
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 

-  if (_sg_mc_visited > 0) {
-    MC_ignore_heap(simix_global->process_to_run->data, 0);
-    MC_ignore_heap(simix_global->process_that_ran->data, 0);
-  }
-

   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */


@@ -398,7 +393,7 @@ void MC_modelcheck_comm_determinism(void)
       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       } else if (visited_state != -1) {
       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       } else if (visited_state != -1) {

-        XBT_DEBUG("State already visited, stop the exploration");
+        XBT_DEBUG("State already visited, exploration stopped on this path.");

       } else {
         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
                   xbt_fifo_size(mc_stack) + 1);
       } else {
         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
                   xbt_fifo_size(mc_stack) + 1);


@@ -420,6 +415,7 @@ void MC_modelcheck_comm_determinism(void)
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);

+            MC_SET_STD_HEAP;

             return;
           } else if (initial_global_state->send_deterministic == 0
                      && _sg_mc_send_determinism) {
             return;
           } else if (initial_global_state->send_deterministic == 0
                      && _sg_mc_send_determinism) {


@@ -434,6 +430,7 @@ void MC_modelcheck_comm_determinism(void)
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);
             XBT_INFO("Communications pattern counter-example:");
             print_communications_pattern(communications_pattern);
             MC_print_statistics(mc_stats);

+            MC_SET_STD_HEAP;

             return;
           }
         } else {
             return;
           }
         } else {