model-checker : factorization of code for model-checking of safety properties in...

diff --git a/include/msg/msg.h b/include/msg/msg.h
index e62db85..4a37ef4 100644 (file)
--- a/include/msg/msg.h
+++ b/include/msg/msg.h
@@ -58,7 +58,6 @@ XBT_PUBLIC(void) MSG_config(const char *name, ...);
 
 XBT_PUBLIC(void) MSG_init_nocheck(int *argc, char **argv);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
 
 XBT_PUBLIC(void) MSG_init_nocheck(int *argc, char **argv);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);

-XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);

 XBT_PUBLIC(MSG_error_t) MSG_main_liveness(xbt_automaton_t a);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
 XBT_PUBLIC(MSG_error_t) MSG_main_liveness(xbt_automaton_t a);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 30d97c3..2752cbd 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -18,7 +18,6 @@ extern int _surf_do_model_check;
 #define MC_IS_ENABLED _surf_do_model_check
 
 XBT_PUBLIC(void) MC_assert(int);
 #define MC_IS_ENABLED _surf_do_model_check
 
 XBT_PUBLIC(void) MC_assert(int);

-XBT_PUBLIC(void) MC_assert_stateful(int);

 XBT_PUBLIC(int) MC_random(int min, int max);
 XBT_PUBLIC(void) MC_diff(void);
 XBT_PUBLIC(xbt_automaton_t) MC_create_automaton(const char *file);
 XBT_PUBLIC(int) MC_random(int min, int max);
 XBT_PUBLIC(void) MC_diff(void);
 XBT_PUBLIC(xbt_automaton_t) MC_create_automaton(const char *file);


@@ -27,7 +26,6 @@ XBT_PUBLIC(xbt_automaton_t) MC_create_automaton(const char *file);
 
 #define MC_IS_ENABLED 0
 #define MC_assert(a) xbt_assert(a)
 
 #define MC_IS_ENABLED 0
 #define MC_assert(a) xbt_assert(a)

-#define MC_assert_stateful(a) xbt_assert(a)

 
 #endif
 
 
 #endif
 

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 4b34fd6..cf0bab6 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -20,12 +20,10 @@
 SG_BEGIN_DECL()
 
 /********************************* Global *************************************/
 SG_BEGIN_DECL()
 
 /********************************* Global *************************************/

-XBT_PUBLIC(void) MC_init_safety_stateless(void);
-XBT_PUBLIC(void) MC_init_safety_stateful(void);
+XBT_PUBLIC(void) MC_init_safety(void);

 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
 XBT_PUBLIC(void) MC_modelcheck(void);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
 XBT_PUBLIC(void) MC_modelcheck(void);

-XBT_PUBLIC(void) MC_modelcheck_stateful(void);

 XBT_PUBLIC(void) MC_modelcheck_liveness(xbt_automaton_t a);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
 XBT_PUBLIC(void) MC_modelcheck_liveness(xbt_automaton_t a);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 6b737a4..6443295 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -19,7 +19,6 @@ void MC_dpor_init()
   /* Create the initial state and push it into the exploration stack */
   MC_SET_RAW_MEM;
   initial_state = MC_state_new();
   /* Create the initial state and push it into the exploration stack */
   MC_SET_RAW_MEM;
   initial_state = MC_state_new();

-  xbt_fifo_unshift(mc_stack_safety_stateless, initial_state);

   MC_UNSET_RAW_MEM;
 
   XBT_DEBUG("**************************************************");
   MC_UNSET_RAW_MEM;
 
   XBT_DEBUG("**************************************************");


@@ -36,6 +35,12 @@ void MC_dpor_init()
       break;
     }
   }
       break;
     }
   }

+
+  initial_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot(initial_state->system_state);
+
+  xbt_fifo_unshift(mc_stack_safety, initial_state);
+

   MC_UNSET_RAW_MEM;
     
   /* FIXME: Update Statistics 
   MC_UNSET_RAW_MEM;
     
   /* FIXME: Update Statistics 


@@ -53,19 +58,20 @@ void MC_dpor(void)
   char *req_str;
   int value;
   smx_simcall_t req = NULL, prev_req = NULL;
   char *req_str;
   int value;
   smx_simcall_t req = NULL, prev_req = NULL;

-  mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
+  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;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;

+  int pos, i = 1;

 
 

-  while (xbt_fifo_size(mc_stack_safety_stateless) > 0) {
+  while (xbt_fifo_size(mc_stack_safety) > 0) {

 
     /* Get current state */
     state = (mc_state_t) 
 
     /* Get current state */
     state = (mc_state_t) 

-      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateless));
+      xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));

 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",

-              xbt_fifo_size(mc_stack_safety_stateless), state,
+              xbt_fifo_size(mc_stack_safety), state,

               MC_state_interleave_size(state));
 
     /* Update statistics */
               MC_state_interleave_size(state));
 
     /* Update statistics */


@@ -73,7 +79,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 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_stateless) < MAX_DEPTH &&
+    if (xbt_fifo_size(mc_stack_safety) < MAX_DEPTH &&

         (req = MC_state_get_request(state, &value))) {
 
       /* Debug information */
         (req = MC_state_get_request(state, &value))) {
 
       /* Debug information */


@@ -94,9 +100,9 @@ void MC_dpor(void)
 
       /* Create the new expanded state */
       MC_SET_RAW_MEM;
 
       /* Create the new expanded state */
       MC_SET_RAW_MEM;

-      next_state = MC_state_new();
-      xbt_fifo_unshift(mc_stack_safety_stateless, next_state);

 
 

+      next_state = MC_state_new();
+      

       /* 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)){
       /* 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)){


@@ -104,6 +110,13 @@ void MC_dpor(void)
           break;
         }
       }
           break;
         }
       }

+
+      if(_surf_do_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_do_mc_checkpoint == 0)){
+        next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
+        MC_take_snapshot(next_state->system_state);
+      }
+
+      xbt_fifo_unshift(mc_stack_safety, next_state);

       MC_UNSET_RAW_MEM;
 
       /* FIXME: Update Statistics
       MC_UNSET_RAW_MEM;
 
       /* FIXME: Update Statistics


@@ -118,7 +131,7 @@ void MC_dpor(void)
 
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;
 
       /* Trash the current state, no longer needed */
       MC_SET_RAW_MEM;

-      xbt_fifo_shift(mc_stack_safety_stateless);
+      xbt_fifo_shift(mc_stack_safety);

       MC_state_delete(state);
       MC_UNSET_RAW_MEM;
 
       MC_state_delete(state);
       MC_UNSET_RAW_MEM;
 


@@ -135,9 +148,9 @@ 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. */
          (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_stateless)) != NULL) {
+      while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {

         req = MC_state_get_internal_request(state);
         req = MC_state_get_internal_request(state);

-        xbt_fifo_foreach(mc_stack_safety_stateless, item, prev_state, mc_state_t) {
+        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:");
           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:");


@@ -161,10 +174,36 @@ void MC_dpor(void)
         }
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */
         }
         if (MC_state_interleave_size(state)) {
           /* We found a back-tracking point, let's loop */

-          xbt_fifo_unshift(mc_stack_safety_stateless, state);
-          XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateless));
-          MC_UNSET_RAW_MEM;
-          MC_replay(mc_stack_safety_stateless);
+          if(_surf_do_mc_checkpoint){
+            if(state->system_state != NULL){
+              MC_restore_snapshot(state->system_state);
+              xbt_fifo_unshift(mc_stack_safety, state);
+              XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
+              MC_UNSET_RAW_MEM;
+            }else{
+              pos = xbt_fifo_size(mc_stack_safety);
+              item = xbt_fifo_get_last_item(mc_stack_safety);
+              while(pos>0){
+                restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
+                if(restore_state->system_state != NULL){
+                  break;
+                }else{
+                  item = xbt_fifo_get_prev_item(item);
+                  pos--;
+                }
+              }
+              MC_restore_snapshot(restore_state->system_state);
+              xbt_fifo_unshift(mc_stack_safety, state);
+              XBT_DEBUG("Back-tracking to depth %d", pos);
+              MC_UNSET_RAW_MEM;
+              MC_replay(mc_stack_safety, pos);
+            }
+          }else{
+            xbt_fifo_unshift(mc_stack_safety, state);
+            XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
+            MC_UNSET_RAW_MEM;
+            MC_replay(mc_stack_safety, 1);
+          }

           break;
         } else {
           MC_state_delete(state);
           break;
         } else {
           MC_state_delete(state);


@@ -179,179 +218,5 @@ void MC_dpor(void)
 }
 
 
 }
 
 

-/********************* DPOR stateful *********************/
-
-mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
-  mc_state_ws_t sws = NULL;
-  sws = xbt_new0(s_mc_state_ws_t, 1);
-  sws->system_state = s;
-  sws->graph_state = gs;
-  return sws;
-}
-
-void MC_dpor_stateful_init(){
-
-  XBT_DEBUG("**************************************************");
-  XBT_DEBUG("DPOR (stateful) init");
-  XBT_DEBUG("**************************************************");
-
-  mc_state_t initial_graph_state;
-  smx_process_t process; 
-  mc_snapshot_t initial_system_snapshot;
-  mc_state_ws_t initial_state ;
-  
-  MC_wait_for_requests();
-
-  MC_SET_RAW_MEM;
-
-  initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-
-  initial_graph_state = MC_state_new();
-  xbt_swag_foreach(process, simix_global->process_list){
-    if(MC_process_is_enabled(process)){
-      MC_state_interleave_process(initial_graph_state, process);
-      break;
-    }
-  }
-
-  MC_take_snapshot(initial_system_snapshot);
-
-  initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
-  xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
-
-  MC_UNSET_RAW_MEM;
-
-}
-
-void MC_dpor_stateful(){
-
-  smx_process_t process = NULL;
-  
-  if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
-    return;
-
-  int value;
-  mc_state_t next_graph_state = NULL;
-  smx_simcall_t req = NULL, prev_req = NULL;
-  char *req_str;
-  xbt_fifo_item_t item = NULL;
-
-  mc_snapshot_t next_snapshot;
-  mc_state_ws_t current_state;
-  mc_state_ws_t prev_state;
-  mc_state_ws_t next_state;
- 
-  while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
-
-    current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
-
-    
-    XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_stack_safety_stateful),current_state, MC_state_interleave_size(current_state->graph_state));
-
-    mc_stats->visited_states++;
-    if(mc_stats->expanded_states>1100)
-      exit(0);
-    //sleep(1);
-
-    if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
-
-      /* Debug information */
-      if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
-        req_str = MC_request_to_string(req, value);
-        //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
-        XBT_DEBUG("Execute: %s",req_str);
-        xbt_free(req_str);
-      }
-
-      MC_state_set_executed_request(current_state->graph_state, req, value);
-      mc_stats->executed_transitions++;
-      
-      /* Answer the request */
-      SIMIX_simcall_pre(req, value);
-      
-      /* Wait for requests (schedules processes) */
-      MC_wait_for_requests();
-      
-      /* Create the new expanded graph_state */
-      MC_SET_RAW_MEM;
-      
-      next_graph_state = MC_state_new();
-      
-      /* Get an enabled process and insert it in the interleave set of the next graph_state */
-      xbt_swag_foreach(process, simix_global->process_list){
-        if(MC_process_is_enabled(process)){
-          MC_state_interleave_process(next_graph_state, process);
-          break;
-        }
-      }
-
-      next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-      MC_take_snapshot(next_snapshot);
-
-      next_state = new_state_ws(next_snapshot, next_graph_state);
-      xbt_fifo_unshift(mc_stack_safety_stateful, next_state);
-      
-      MC_UNSET_RAW_MEM;
-
-    }else{
-      XBT_DEBUG("There are no more processes to interleave.");
-      
-      /* Trash the current state, no longer needed */
-      MC_SET_RAW_MEM;
-      xbt_fifo_shift(mc_stack_safety_stateful);
-      MC_UNSET_RAW_MEM;
-
-      /* Check for deadlocks */
-      if(MC_deadlock_check()){
-        MC_show_deadlock_stateful(NULL);
-        return;
-      }
-
-      MC_SET_RAW_MEM;
-      while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
-        req = MC_state_get_internal_request(current_state->graph_state);
-        xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
-          if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
-            if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
-              XBT_DEBUG("Dependent Transitions:");
-              prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
-              req_str = MC_request_to_string(prev_req, value);
-              XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
-              xbt_free(req_str);
-              prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
-              req_str = MC_request_to_string(prev_req, value);
-              XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
-              xbt_free(req_str);              
-            }
-
-            if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
-              MC_state_interleave_process(prev_state->graph_state, req->issuer);
-        
-            } else {
-              XBT_DEBUG("Process %p is in done set", req->issuer);
-            }
-
-            break;
-          }
-        }
-
-        if(MC_state_interleave_size(current_state->graph_state)){
-          MC_restore_snapshot(current_state->system_state);
-          xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
-          XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
-          MC_UNSET_RAW_MEM;
-          break;
-        }
-      }
-
-      MC_UNSET_RAW_MEM;
-
-    } 
-  }
-  MC_UNSET_RAW_MEM;
-  return;
-}
-

 
 
 
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index f55b44f..70fa118 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -27,8 +27,7 @@ mc_snapshot_t initial_snapshot = NULL;
 
 /* Safety */
 
 
 /* Safety */
 

-xbt_fifo_t mc_stack_safety_stateful = NULL;
-xbt_fifo_t mc_stack_safety_stateless = NULL;
+xbt_fifo_t mc_stack_safety = NULL;

 mc_stats_t mc_stats = NULL;
 
 /* Liveness */
 mc_stats_t mc_stats = NULL;
 
 /* Liveness */


@@ -46,7 +45,7 @@ static void MC_assert_pair(int prop);
 /**
  *  \brief Initialize the model-checker data structures
  */
 /**
  *  \brief Initialize the model-checker data structures
  */

-void MC_init_safety_stateless(void)
+void MC_init_safety(void)

 {
 
   /* Check if MC is already initialized */
 {
 
   /* Check if MC is already initialized */


@@ -64,7 +63,7 @@ void MC_init_safety_stateless(void)
   mc_stats->state_size = 1;
 
   /* Create exploration stack */
   mc_stats->state_size = 1;
 
   /* Create exploration stack */

-  mc_stack_safety_stateless = xbt_fifo_new();
+  mc_stack_safety = xbt_fifo_new();

 
   MC_UNSET_RAW_MEM;
 
 
   MC_UNSET_RAW_MEM;
 


@@ -75,35 +74,10 @@ void MC_init_safety_stateless(void)
   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;

-}
-
-void MC_init_safety_stateful(void){
-
-  
-  /* Check if MC is already initialized */
-  if (initial_snapshot)
-    return;
-
-  mc_time = xbt_new0(double, simix_process_maxpid);
-
-  /* Initialize the data structures that must be persistent across every
-     iteration of the model-checker (in RAW memory) */
-  MC_SET_RAW_MEM;
-
-  /* Initialize statistics */
-  mc_stats = xbt_new0(s_mc_stats_t, 1);
-  mc_stats->state_size = 1;
-
-  /* Create exploration stack */
-  mc_stack_safety_stateful = xbt_fifo_new();
-
-  MC_UNSET_RAW_MEM;
-
-  MC_dpor_stateful_init();
-

 
 }
 
 
 }
 

+

 static void MC_init_liveness(xbt_automaton_t a){
 
   XBT_DEBUG("Start init mc");
 static void MC_init_liveness(xbt_automaton_t a){
 
   XBT_DEBUG("Start init mc");


@@ -135,17 +109,11 @@ static void MC_init_liveness(xbt_automaton_t a){
 
 void MC_modelcheck(void)
 {
 
 void MC_modelcheck(void)
 {

-  MC_init_safety_stateless();
+  MC_init_safety();

   MC_dpor();
   MC_exit();
 }
 
   MC_dpor();
   MC_exit();
 }
 

-void MC_modelcheck_stateful(void)
-{
-  MC_init_safety_stateful();
-  MC_dpor_stateful();
-  MC_exit();
-}

 
 
 void MC_modelcheck_liveness(xbt_automaton_t a){
 
 
 void MC_modelcheck_liveness(xbt_automaton_t a){


@@ -213,11 +181,12 @@ int MC_deadlock_check()
 }
 
 /**
 }
 
 /**

- * \brief Re-executes from the initial state all the transitions indicated by
+ * \brief Re-executes from the start state all the transitions indicated by

  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.
  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.

+ * \param start Start index to begin the re-execution.

  */
  */

-void MC_replay(xbt_fifo_t stack)
+void MC_replay(xbt_fifo_t stack, int start)

 {
   int value;
   char *req_str;
 {
   int value;
   char *req_str;


@@ -373,20 +342,25 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
  *        execution trace
  * \param stack The stack to dump
  */
  *        execution trace
  * \param stack The stack to dump
  */

-void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
+void MC_dump_stack_safety(xbt_fifo_t stack)

 {
 {

-  mc_state_t state;

 
 

-  MC_show_stack_safety_stateless(stack);
+  MC_show_stack_safety(stack);

 
 

-  MC_SET_RAW_MEM;
-  while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
-    MC_state_delete(state);
-  MC_UNSET_RAW_MEM;
+  if(!_surf_do_mc_checkpoint){
+
+    mc_state_t state;
+
+    MC_SET_RAW_MEM;
+    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+      MC_state_delete(state);
+    MC_UNSET_RAW_MEM;
+
+  }

 }
 
 
 }
 
 

-void MC_show_stack_safety_stateless(xbt_fifo_t stack)
+void MC_show_stack_safety(xbt_fifo_t stack)

 {
   int value;
   mc_state_t state;
 {
   int value;
   mc_state_t state;


@@ -417,54 +391,7 @@ void MC_show_deadlock(smx_simcall_t req)
     XBT_INFO("%s", req_str);
     xbt_free(req_str);*/
   XBT_INFO("Counter-example execution trace:");
     XBT_INFO("%s", req_str);
     xbt_free(req_str);*/
   XBT_INFO("Counter-example execution trace:");

-  MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
-}
-
-void MC_show_deadlock_stateful(smx_simcall_t req)
-{
-  /*char *req_str = NULL;*/
-  XBT_INFO("**************************");
-  XBT_INFO("*** DEAD-LOCK DETECTED ***");
-  XBT_INFO("**************************");
-  XBT_INFO("Locked request:");
-  /*req_str = MC_request_to_string(req);
-    XBT_INFO("%s", req_str);
-    xbt_free(req_str);*/
-  XBT_INFO("Counter-example execution trace:");
-  MC_show_stack_safety_stateful(mc_stack_safety_stateful);
-}
-
-void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
-{
-  //mc_state_ws_t state;
-
-  MC_show_stack_safety_stateful(stack);
-
-  /*MC_SET_RAW_MEM;
-    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
-    MC_state_delete(state);
-    MC_UNSET_RAW_MEM;*/
-}
-
-
-void MC_show_stack_safety_stateful(xbt_fifo_t stack)
-{
-  int value;
-  mc_state_ws_t state;
-  xbt_fifo_item_t item;
-  smx_simcall_t req;
-  char *req_str = NULL;
-  
-  for (item = xbt_fifo_get_last_item(stack);
-       (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
-    req = MC_state_get_executed_request(state->graph_state, &value);
-    if(req){
-      req_str = MC_request_to_string(req, value);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
-    }
-  }
+  MC_dump_stack_safety(mc_stack_safety);

 }
 
 
 }
 
 


@@ -531,26 +458,12 @@ void MC_assert(int prop)
     XBT_INFO("*** PROPERTY NOT VALID ***");
     XBT_INFO("**************************");
     XBT_INFO("Counter-example execution trace:");
     XBT_INFO("*** PROPERTY NOT VALID ***");
     XBT_INFO("**************************");
     XBT_INFO("Counter-example execution trace:");

-    MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
-    MC_print_statistics(mc_stats);
-    xbt_abort();
-  }
-}
-
-void MC_assert_stateful(int prop)
-{
-  if (MC_IS_ENABLED && !prop) {
-    XBT_INFO("**************************");
-    XBT_INFO("*** PROPERTY NOT VALID ***");
-    XBT_INFO("**************************");
-    XBT_INFO("Counter-example execution trace:");
-    MC_dump_stack_safety_stateful(mc_stack_safety_stateful);
+    MC_dump_stack_safety(mc_stack_safety);

     MC_print_statistics(mc_stats);
     xbt_abort();
   }
 }
 
     MC_print_statistics(mc_stats);
     xbt_abort();
   }
 }
 

-

 static void MC_assert_pair(int prop){
   if (MC_IS_ENABLED && !prop) {
     XBT_INFO("**************************");
 static void MC_assert_pair(int prop){
   if (MC_IS_ENABLED && !prop) {
     XBT_INFO("**************************");

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index b088e88..f4e5499 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -49,16 +49,13 @@ extern double *mc_time;
 #define MAX_DEPTH_LIVENESS 500
 
 int MC_deadlock_check(void);
 #define MAX_DEPTH_LIVENESS 500
 
 int MC_deadlock_check(void);

-void MC_replay(xbt_fifo_t stack);
+void MC_replay(xbt_fifo_t stack, int start);

 void MC_replay_liveness(xbt_fifo_t stack, int all_stack);
 void MC_wait_for_requests(void);
 void MC_get_enabled_processes();
 void MC_show_deadlock(smx_simcall_t req);
 void MC_replay_liveness(xbt_fifo_t stack, int all_stack);
 void MC_wait_for_requests(void);
 void MC_get_enabled_processes();
 void MC_show_deadlock(smx_simcall_t req);

-void MC_show_deadlock_stateful(smx_simcall_t req);
-void MC_show_stack_safety_stateless(xbt_fifo_t stack);
-void MC_dump_stack_safety_stateless(xbt_fifo_t stack);
-void MC_show_stack_safety_stateful(xbt_fifo_t stack);
-void MC_dump_stack_safety_stateful(xbt_fifo_t stack);
+void MC_show_stack_safety(xbt_fifo_t stack);
+void MC_dump_stack_safety(xbt_fifo_t stack);

 
 /********************************* Requests ***********************************/
 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
 
 /********************************* Requests ***********************************/
 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);


@@ -95,6 +92,7 @@ typedef struct mc_state {
   s_smx_simcall_t executed_req;         /* The executed request of the state */
   int req_num;                      /* The request number (in the case of a
                                        multi-request like waitany ) */
   s_smx_simcall_t executed_req;         /* The executed request of the state */
   int req_num;                      /* The request number (in the case of a
                                        multi-request like waitany ) */

+  mc_snapshot_t system_state;      /* Snapshot of system state */

 } s_mc_state_t, *mc_state_t;
 
 extern xbt_fifo_t mc_stack_safety_stateless;
 } s_mc_state_t, *mc_state_t;
 
 extern xbt_fifo_t mc_stack_safety_stateless;


@@ -183,26 +181,12 @@ typedef struct s_memory_map {
 memory_map_t get_memory_map(void);
 
 
 memory_map_t get_memory_map(void);
 
 

-/********************************** DPOR for safety (stateless) **************************************/
+/********************************** DPOR for safety  **************************************/
+

 void MC_dpor_init(void);
 void MC_dpor(void);
 void MC_dpor_exit(void);
 void MC_dpor_init(void);
 void MC_dpor(void);
 void MC_dpor_exit(void);

-
-/***** DPOR for safety (stateful) **** */
-
-typedef struct s_mc_state_with_snapshot{
-  mc_snapshot_t system_state;
-  mc_state_t graph_state;
-}s_mc_state_ws_t, *mc_state_ws_t;
-
-extern xbt_fifo_t mc_stack_safety_stateful;
-
-void MC_init_stateful(void);
-void MC_modelcheck_stateful(void);
-mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs);
-void MC_dpor_stateful_init(void);
-void MC_dpor_stateful(void);
-void MC_exit_stateful(void);
+void MC_init_safety(void);

 
 
 /********************************** Double-DFS for liveness property**************************************/
 
 
 /********************************** Double-DFS for liveness property**************************************/

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 858cc93..822d17a 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -10,14 +10,15 @@
 /**
  * \brief Creates a state data structure used by the exploration algorithm
  */
 /**
  * \brief Creates a state data structure used by the exploration algorithm
  */

-mc_state_t MC_state_new(void)
+mc_state_t MC_state_new()

 {
   mc_state_t state = NULL;
   
   state = xbt_new0(s_mc_state_t, 1);
   state->max_pid = simix_process_maxpid;
   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
 {
   mc_state_t state = NULL;
   
   state = xbt_new0(s_mc_state_t, 1);
   state->max_pid = simix_process_maxpid;
   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);

-  
+  state->system_state = NULL;
+

   mc_stats->expanded_states++;
   return state;
 }
   mc_stats->expanded_states++;
   return state;
 }

diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index 243057c..879461f 100644 (file)
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -117,21 +117,6 @@ MSG_error_t MSG_main(void)
   return MSG_OK;
 }
 
   return MSG_OK;
 }
 

-MSG_error_t MSG_main_stateful(void)
-{
-  /* Clean IO before the run */
-  fflush(stdout);
-  fflush(stderr);
-
-  if (MC_IS_ENABLED) {
-    MC_modelcheck_stateful();
-  }
-  else {
-    SIMIX_run();
-  }
-  return MSG_OK;
-}
-

 
 MSG_error_t MSG_main_liveness(xbt_automaton_t a)
 {
 
 MSG_error_t MSG_main_liveness(xbt_automaton_t a)
 {