MC LTL : add statistics

diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c
index fa9ec05..ba03974 100644 (file)
--- a/src/mc/mc_dfs.c
+++ b/src/mc/mc_dfs.c
@@ -55,7 +55,7 @@ int reached(mc_state_t gs, xbt_state_t as ){
       }
       if(different_process==0){
        MC_UNSET_RAW_MEM;
-       XBT_DEBUG("Pair (graph=%p, automaton=%p, interleave=%d) already reached (graph=%p)!", gs, as, MC_state_interleave_size(gs), rp->graph_state);
+       XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached (graph=%p)!", gs, as, as->id, rp->graph_state);
        return 1;
       }
       /* XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached !", gs, as, as->id); */
@@ -69,7 +69,7 @@ int reached(mc_state_t gs, xbt_state_t as ){
 void set_pair_reached(mc_state_t gs, xbt_state_t as){
 
   //XBT_DEBUG("Set pair (graph=%p, automaton=%p) reached ", gs, as);
-  if(reached(gs, as) == 0){
+  //if(reached(gs, as) == 0){
     MC_SET_RAW_MEM;
     mc_reached_pairs_t p = NULL;
     p = xbt_new0(s_mc_reached_pairs_t, 1);
@@ -78,7 +78,7 @@ void set_pair_reached(mc_state_t gs, xbt_state_t as){
     xbt_dynar_push(reached_pairs, &p); 
     XBT_DEBUG("New reached pair : graph=%p, automaton=%p(%s)", gs, as, as->id);
     MC_UNSET_RAW_MEM;
-  }
+    //}
 
 }
 
@@ -129,7 +129,7 @@ void MC_dfs_init(xbt_automaton_t a){
 
   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 
-  initial_graph_state = MC_state_new();
+  initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
       MC_state_interleave_process(initial_graph_state, process);
@@ -328,6 +328,8 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
   
   //sleep(1);
 
+  mc_stats_pair->visited_pairs++;
+
   int value;
   mc_state_t next_graph_state = NULL;
   smx_req_t req = NULL;
@@ -362,7 +364,6 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
     }
 
     MC_state_set_executed_request(current_pair->graph_state, req, value);
-    //mc_stats->executed_transitions++;
 
     /* Answer the request */
     SIMIX_request_pre(req, value);
@@ -374,7 +375,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
     /* Create the new expanded graph_state */
     MC_SET_RAW_MEM;
 
-    next_graph_state = MC_state_new();
+    next_graph_state = MC_state_pair_new();
     
     /* Get enabled process and insert it in the interleave set of the next graph_state */
     xbt_swag_foreach(process, simix_global->process_list){
@@ -403,6 +404,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
        
       if((res == 1) || (res == 2)){ // enabled transition in automaton
        xbt_dynar_push(successors, &next_pair);
+       mc_stats_pair->expanded_pairs++;
       }
 
       MC_UNSET_RAW_MEM;
@@ -414,6 +416,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
       MC_SET_RAW_MEM;
       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
       xbt_dynar_push(successors, &next_pair);
+      mc_stats_pair->expanded_pairs++;
       MC_UNSET_RAW_MEM;
        
     }
@@ -435,12 +438,15 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
          XBT_INFO("Counter-example that violates formula :");
          MC_show_snapshot_stack(mc_snapshot_stack);
          MC_dump_snapshot_stack(mc_snapshot_stack);
+         MC_print_statistics_pairs(mc_stats_pair);
          exit(0);
        }
        
        if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
 
          //XBT_DEBUG("Unvisited pair !");
+
+         mc_stats_pair->executed_transitions++;
  
          MC_SET_RAW_MEM;
          xbt_fifo_unshift(mc_snapshot_stack, pair_succ);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 508ef28..d363a57 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -15,6 +15,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
 mc_snapshot_t initial_snapshot = NULL;
 xbt_fifo_t mc_stack = NULL;
 mc_stats_t mc_stats = NULL;
+mc_stats_pair_t mc_stats_pair = NULL;
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
@@ -65,8 +66,8 @@ void MC_init_with_automaton(xbt_automaton_t a){
   MC_SET_RAW_MEM;
 
   /* Initialize statistics */
-  mc_stats = xbt_new0(s_mc_stats_t, 1);
-  mc_stats->state_size = 1;
+  mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
+  //mc_stats_pair->pair_size = 1;
 
   XBT_DEBUG("Creating snapshot_stack");
 
@@ -88,7 +89,14 @@ void MC_modelcheck(void)
 
 void MC_modelcheck_with_automaton(xbt_automaton_t a){
   MC_init_with_automaton(a);
-  MC_exit();
+  MC_exit_with_automaton();
+}
+
+void MC_exit_with_automaton(void)
+{
+  MC_print_statistics_pairs(mc_stats_pair);
+  xbt_free(mc_time);
+  MC_memory_exit();
 }
 
 void MC_exit(void)
@@ -255,6 +263,17 @@ void MC_print_statistics(mc_stats_t stats)
      (double)stats->expanded_states / stats->state_size); */
 }
 
+void MC_print_statistics_pairs(mc_stats_pair_t stats)
+{
+  XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+  XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+  XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
+  XBT_INFO("Expanded / Visited = %lf",
+        (double) stats->visited_pairs / stats->expanded_pairs);
+  /*XBT_INFO("Exploration coverage = %lf",
+     (double)stats->expanded_states / stats->state_size); */
+}
+
 void MC_assert(int prop)
 {
   if (MC_IS_ENABLED && !prop) {

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 8588cb8..08d7b59 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -19,6 +19,18 @@ mc_state_t MC_state_new(void)
   return state;
 }
 
+mc_state_t MC_state_pair_new(void)
+{
+  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_stats->expanded_states++;
+  return state;
+}
+
 /**
  * \brief Deletes a state data structure
  * \param trans The state to be deleted

diff --git a/src/mc/private.h b/src/mc/private.h
index ee8df4e..a815f64 100644 (file)
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -112,9 +112,18 @@ typedef struct mc_stats {
   unsigned long executed_transitions;
 } s_mc_stats_t, *mc_stats_t;
 
+typedef struct mc_stats_pair {
+  //unsigned long pair_size;
+  unsigned long visited_pairs;
+  unsigned long expanded_pairs;
+  unsigned long executed_transitions;
+} s_mc_stats_pair_t, *mc_stats_pair_t;
+
 extern mc_stats_t mc_stats;
+extern mc_stats_pair_t mc_stats_pair;
 
 void MC_print_statistics(mc_stats_t);
+void MC_print_statistics_pairs(mc_stats_pair_t);
 
 /********************************** MEMORY ******************************/
 /* The possible memory modes for the modelchecker are standard and raw. */
@@ -202,6 +211,8 @@ void set_pair_reached(mc_state_t gs, xbt_state_t as);
 void MC_show_snapshot_stack(xbt_fifo_t stack);
 void MC_dump_snapshot_stack(xbt_fifo_t stack);
 void MC_pair_delete(mc_pairs_t pair);
+void MC_exit_with_automaton(void);
+mc_state_t MC_state_pair_new(void);
 
 
 #endif