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)

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 1d698bd..1fe4044 100644 (file)
--- 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 c76bb7a..92f7d93 100644 (file)
--- 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 822d17a..39eef8a 100644 (file)
--- 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;