From ead8b3a1775defecebc316cb5e4fcddbd283df4c Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Fri, 16 Nov 2012 17:04:05 +0100
Subject: [PATCH 1/1] model-checker : fix dpor algorithm

  - Interleave all enabled processes for each state
  - If max_depth reached and last state still have processes interleaved, backtrack on this state (reduction not applied)"
  - If independant transitions, corresponding process interleaved in previous state is disabled (MC_DONE)
---
 src/mc/mc_dpor.c    | 63 ++++++++++++++++++++++++++-------------------
 src/mc/mc_private.h |  1 +
 src/mc/mc_state.c   |  6 +++++
 3 files changed, 43 insertions(+), 27 deletions(-)

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1d698bd651..1fe4044cca 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -188,18 +188,13 @@ 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); 
+            //break;
           }
         }
 
@@ -207,6 +202,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 +253,38 @@ 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);              
+              }
 
-            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);
+              /*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);*/
+              
 
-            break;
+              break;
+
+            }else{
+              
+              //XBT_DEBUG("Independant transitions : (%lu) %d - (%lu) %d", req->issuer->pid, req->call, MC_state_get_internal_request(prev_state)->issuer->pid, MC_state_get_internal_request(prev_state)->call);
+              MC_state_remove_interleave_process(prev_state, req->issuer);
+
+            }
           }
         }
         if (MC_state_interleave_size(state)) {
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index c76bb7a470..92f7d93c8b 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -114,6 +114,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu
 smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
 smx_simcall_t MC_state_get_internal_request(mc_state_t state);
 smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
+void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
 
 /****************************** Statistics ************************************/
 typedef struct mc_stats {
diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 822d17a431..39eef8ad70 100644
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -51,6 +51,12 @@ void MC_state_interleave_process(mc_state_t state, smx_process_t process)
   state->proc_status[process->pid].interleave_count = 0;
 }
 
+void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process)
+{
+  if(state->proc_status[process->pid].state == MC_INTERLEAVE)
+    state->proc_status[process->pid].state = MC_DONE;
+}
+
 unsigned int MC_state_interleave_size(mc_state_t state)
 {
   unsigned int i, size=0;
-- 
2.20.1