model-checker : remove restriction of DPOR if several requests for same process

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index f039aff..03d6ec1 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -14,7 +14,7 @@ static int is_visited_state(void);
 
 static int is_visited_state(){
 
-  if(_surf_mc_visited == 0)
+  if(_sg_mc_visited == 0)
     return 0;
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -57,7 +57,7 @@ static int is_visited_state(){
       }   
     }
 
-    if(xbt_dynar_length(visited_states) == _surf_mc_visited){
+    if(xbt_dynar_length(visited_states) == _sg_mc_visited){
       mc_snapshot_t state_to_remove = NULL;
       xbt_dynar_shift(visited_states, &state_to_remove);
       MC_free_snapshot(state_to_remove);
@@ -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) {
 
@@ -153,7 +152,7 @@ void MC_dpor(void)
 
     /* If there are processes to interleave and the maximum depth has not been reached
        then perform one step of the exploration algorithm */
-    if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
+    if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
         (req = MC_state_get_request(state, &value))) {
 
       /* Debug information */
@@ -186,7 +185,7 @@ void MC_dpor(void)
           }
         }
 
-        if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
+        if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
           next_state->system_state = MC_take_snapshot();
         }
 
@@ -208,7 +207,7 @@ void MC_dpor(void)
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
     } else {
 
-      if(xbt_fifo_size(mc_stack_safety) == _surf_mc_max_depth)  
+      if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)  
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       else
         XBT_DEBUG("There are no more processes to interleave.");
@@ -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,20 +255,18 @@ 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;
-
           }
         }
 
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */
-          if(_surf_mc_checkpoint){
+          if(_sg_mc_checkpoint){
             if(state->system_state != NULL){
               MC_restore_snapshot(state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);