From cf799d4b83e1fda76b512c50bb781eca63d283da Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Mon, 17 Dec 2012 10:13:29 +0100
Subject: [PATCH] model-checker : remove restriction of DPOR if several
 requests for same process

---
 src/mc/mc_dpor.c | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 2f479a0dd3..03d6ec115f 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -134,8 +134,7 @@ void MC_dpor(void)
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
-  int pos, i;
-  int proc_eval[simix_process_maxpid];
+  int pos;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -234,10 +233,6 @@ void MC_dpor(void)
          state that executed that previous request. */
       
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
-
-        for(i=0; i<simix_process_maxpid; i++)
-          proc_eval[i] = 0;
-
         if(MC_state_interleave_size(state) == 0){
           req = MC_state_get_internal_request(state);
           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
@@ -260,14 +255,12 @@ void MC_dpor(void)
 
               break;
 
-            }else if(proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] == 0){
+            }else{
 
-              MC_state_remove_interleave_process(prev_state, MC_state_get_executed_request(prev_state, &value)->issuer);
+              MC_state_remove_interleave_process(prev_state, req->issuer);
 
             }
 
-            proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] = 1;
-
           }
         }
 
-- 
2.20.1