model-checker : compare the pid of enabled processes before memory introspection

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 72ab536..809f877 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -278,21 +278,13 @@ void MC_init()
     MC_ignore_global_variable("maestro_stack_end");
     MC_ignore_global_variable("smx_total_comms");
 
-    MC_ignore_heap(&(simix_global->process_to_run),
-                   sizeof(simix_global->process_to_run));
-    MC_ignore_heap(&(simix_global->process_that_ran),
-                   sizeof(simix_global->process_that_ran));
-    MC_ignore_heap(simix_global->process_to_run,
-                   sizeof(*(simix_global->process_to_run)));
-    MC_ignore_heap(simix_global->process_that_ran,
-                   sizeof(*(simix_global->process_that_ran)));
     MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
     smx_process_t process;
     xbt_swag_foreach(process, simix_global->process_list) {
       MC_ignore_heap(&(process->process_hookup),
                      sizeof(process->process_hookup));
-    }
+                     }
   }
 
   if (raw_mem_set)
@@ -516,7 +508,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 
   MC_SET_MC_HEAP;
 
-  if (mc_reduce_kind == e_mc_reduce_dpor) {
+  if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
     xbt_dict_reset(first_enabled_state);
     xbt_swag_foreach(process, simix_global->process_list) {
       if (MC_process_is_enabled(process)) {
@@ -544,7 +536,7 @@ void MC_replay(xbt_fifo_t stack, int start)
     state = (mc_state_t) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
 
-    if (mc_reduce_kind == e_mc_reduce_dpor) {
+    if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
       MC_SET_MC_HEAP;
       char *key = bprintf("%lu", saved_req->issuer->pid);
       xbt_dict_remove(first_enabled_state, key);
@@ -604,12 +596,11 @@ void MC_replay(xbt_fifo_t stack, int start)
 
       count++;
 
-      if (mc_reduce_kind == e_mc_reduce_dpor) {
+      if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
         MC_SET_MC_HEAP;
         /* Insert in dict all enabled processes */
         xbt_swag_foreach(process, simix_global->process_list) {
-          if (MC_process_is_enabled(process)
-              /*&& !MC_state_process_is_done(state, process) */ ) {
+          if (MC_process_is_enabled(process) ) {
             char *key = bprintf("%lu", process->pid);
             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
               char *data = bprintf("%d", count);