model-checker : rename cfg flag for state comparison reduction with storage of visite...

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

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1d698bd..0947844 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_stateful == 0)
+  if(_surf_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_stateful){
+    if(xbt_dynar_length(visited_states) == _surf_mc_visited){
       mc_snapshot_t state_to_remove = NULL;
       xbt_dynar_shift(visited_states, &state_to_remove);
       MC_free_snapshot(state_to_remove);
@@ -188,18 +188,12 @@ void MC_dpor(void)
       next_state = MC_state_new();
 
       if(!is_visited_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); 
-          }
-        }
-        
+     
         /* Get an enabled process and insert it in the interleave set of the next state */
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_state, process);
-            break;
+            XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
           }
         }
 
@@ -207,6 +201,10 @@ void MC_dpor(void)
           next_state->system_state = MC_take_snapshot();
         }
 
+      }else{
+
+        XBT_DEBUG("State already visited !");
+        
       }
 
       xbt_fifo_unshift(mc_stack_safety, next_state);
@@ -254,28 +252,35 @@ void MC_dpor(void)
          (from it's predecesor state), depends on any other previous request 
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
+      
       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
-        req = MC_state_get_internal_request(state);
-        xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
-          if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
-            if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
-              XBT_DEBUG("Dependent Transitions:");
-              prev_req = MC_state_get_executed_request(prev_state, &value);
-              req_str = MC_request_to_string(prev_req, value);
-              XBT_DEBUG("%s (state=%p)", req_str, prev_state);
-              xbt_free(req_str);
-              prev_req = MC_state_get_executed_request(state, &value);
-              req_str = MC_request_to_string(prev_req, value);
-              XBT_DEBUG("%s (state=%p)", req_str, state);
-              xbt_free(req_str);              
-            }
+        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) {
+            if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
+              if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+                XBT_DEBUG("Dependent Transitions:");
+                prev_req = MC_state_get_executed_request(prev_state, &value);
+                req_str = MC_request_to_string(prev_req, value);
+                XBT_DEBUG("%s (state=%p)", req_str, prev_state);
+                xbt_free(req_str);
+                prev_req = MC_state_get_executed_request(state, &value);
+                req_str = MC_request_to_string(prev_req, value);
+                XBT_DEBUG("%s (state=%p)", req_str, state);
+                xbt_free(req_str);              
+              }
+
+              break;
 
-            if(!MC_state_process_is_done(prev_state, req->issuer))
-              MC_state_interleave_process(prev_state, req->issuer);
-            else
-              XBT_DEBUG("Process %p is in done set", req->issuer);
+            }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
 
-            break;
+              break;
+
+            }else{
+              
+              MC_state_remove_interleave_process(prev_state, req->issuer);
+
+            }
           }
         }
         if (MC_state_interleave_size(state)) {