model-checker : cleanups

- remove (a part of) redundant code
- rename structs and variables
- update headers

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index 930c233..2ff4816 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -423,6 +423,7 @@ set(MC_SRC
   src/mc/mc_request.c
   src/mc/mc_state.c
   src/mc/memory_map.c
   src/mc/mc_request.c
   src/mc/mc_state.c
   src/mc/memory_map.c

+  src/mc/mc_pair.c

   )
 
 set(headers_to_install
   )
 
 set(headers_to_install

diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h
index 9f57747..0cdf31f 100644 (file)
--- a/include/xbt/automaton.h
+++ b/include/xbt/automaton.h
@@ -9,111 +9,111 @@
 
 SG_BEGIN_DECL()
 
 
 SG_BEGIN_DECL()
 

-typedef struct xbt_state {
+typedef struct xbt_automaton_state {

   char* id;
   int type; /* -1 = init, 0 = inter, 1 = final */
   xbt_dynar_t in;
   xbt_dynar_t out;
   char* id;
   int type; /* -1 = init, 0 = inter, 1 = final */
   xbt_dynar_t in;
   xbt_dynar_t out;

-} s_xbt_state;
+} s_xbt_automaton_state;

 
 

-typedef struct xbt_state* xbt_state_t;
+typedef struct xbt_automaton_state* xbt_automaton_state_t;

 
 typedef struct xbt_automaton {
   xbt_dynar_t propositional_symbols;
   xbt_dynar_t transitions;
   xbt_dynar_t states;
 
 typedef struct xbt_automaton {
   xbt_dynar_t propositional_symbols;
   xbt_dynar_t transitions;
   xbt_dynar_t states;

-  xbt_state_t current_state;
+  xbt_automaton_state_t current_state;

 } s_xbt_automaton;
 
 typedef struct xbt_automaton* xbt_automaton_t;
 
 } s_xbt_automaton;
 
 typedef struct xbt_automaton* xbt_automaton_t;
 

-typedef struct xbt_exp_label{
+typedef struct xbt_automaton_exp_label{

   enum{or=0, and=1, not=2, predicat=3, one=4} type;
   union{
     struct{
   enum{or=0, and=1, not=2, predicat=3, one=4} type;
   union{
     struct{

-      struct xbt_exp_label* left_exp;
-      struct xbt_exp_label* right_exp;
+      struct xbt_automaton_exp_label* left_exp;
+      struct xbt_automaton_exp_label* right_exp;

     }or_and;
     }or_and;

-    struct xbt_exp_label* exp_not;
+    struct xbt_automaton_exp_label* exp_not;

     char* predicat;
   }u;
     char* predicat;
   }u;

-} s_xbt_exp_label;
+} s_xbt_automaton_exp_label;

 
 

-typedef struct xbt_exp_label* xbt_exp_label_t;
+typedef struct xbt_automaton_exp_label* xbt_automaton_exp_label_t;

 
 
 
 

-typedef struct xbt_transition {
-  xbt_state_t src;
-  xbt_state_t dst;
-  xbt_exp_label_t label;
-} s_xbt_transition;
+typedef struct xbt_automaton_transition {
+  xbt_automaton_state_t src;
+  xbt_automaton_state_t dst;
+  xbt_automaton_exp_label_t label;
+} s_xbt_automaton_transition;

 
 

-typedef struct xbt_transition* xbt_transition_t;
+typedef struct xbt_automaton_transition* xbt_automaton_transition_t;

 
 
 
 

-typedef struct xbt_propositional_symbol{
+typedef struct xbt_automaton_propositional_symbol{

   char* pred;
   void* function;
   char* pred;
   void* function;

-} s_xbt_propositional_symbol;
+} s_xbt_automaton_propositional_symbol;

 
 

-typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t;
+typedef struct xbt_automaton_propositional_symbol* xbt_automaton_propositional_symbol_t;

 
 
 XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);
 
 XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file);
 
 
 
 XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);
 
 XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file);
 

-XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_state_new(xbt_automaton_t a, int type, char* id);

 
 

-XBT_PUBLIC(xbt_transition_t) xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label);
+XBT_PUBLIC(xbt_automaton_transition_t) xbt_automaton_transition_new(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst, xbt_automaton_exp_label_t label);

 
 

-XBT_PUBLIC(xbt_exp_label_t) xbt_automaton_new_label(int type, ...);
+XBT_PUBLIC(xbt_automaton_exp_label_t) xbt_automaton_exp_label_new(int type, ...);

 
 XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_states(xbt_automaton_t a);
 
 XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a);
 
 
 XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_states(xbt_automaton_t a);
 
 XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a);
 

-XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst);
+XBT_PUBLIC(xbt_automaton_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst);

 
 

-XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_transition_get_source(xbt_automaton_transition_t t);

 
 

-XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_transition_get_destination(xbt_automaton_transition_t t);

 
 

-XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src);
+XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_automaton_transition_t t, xbt_automaton_state_t src);

 
 

-XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst);
+XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_automaton_transition_t t, xbt_automaton_state_t dst);

 
 

-XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_state_t s);
+XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_automaton_state_t s);

 
 

-XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_state_t s);
+XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_automaton_state_t s);

 
 

-XBT_PUBLIC(xbt_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id); 
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id); 

 
 XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a);
 
 
 XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a);
 

-XBT_PUBLIC(void) xbt_automaton_display_exp(xbt_exp_label_t l);
+XBT_PUBLIC(void) xbt_automaton_exp_label_display(xbt_automaton_exp_label_t l);

 
 

-XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct);
+XBT_PUBLIC(xbt_automaton_propositional_symbol_t) xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct);

 
 

-XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
+XBT_PUBLIC(xbt_automaton_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);

 
 

-XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2);
+XBT_PUBLIC(int) xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2);

 
 

-XBT_PUBLIC(int) propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2);
+XBT_PUBLIC(int) xbt_automaton_propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2);

 
 

-XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
+XBT_PUBLIC(int) xbt_automaton_transition_compare(const void *t1, const void *t2);

 
 

-XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2);
+XBT_PUBLIC(int) xbt_automaton_exp_label_compare(xbt_automaton_exp_label_t l1, xbt_automaton_exp_label_t l2);

 
 

-XBT_PUBLIC(void) xbt_state_free_voidp(void *s);
+XBT_PUBLIC(void) xbt_automaton_state_free_voidp(void *s);

 
 

-XBT_PUBLIC(void) xbt_state_free(xbt_state_t s);
+XBT_PUBLIC(void) xbt_automaton_state_free(xbt_automaton_state_t s);

 
 

-XBT_PUBLIC(void) xbt_transition_free_voidp(void *t);
+XBT_PUBLIC(void) xbt_automaton_transition_free_voidp(void *t);

 
 

-XBT_PUBLIC(void) xbt_exp_label_free_voidp(void *e);
+XBT_PUBLIC(void) xbt_automaton_exp_label_free_voidp(void *e);

 
 

-XBT_PUBLIC(void) xbt_propositional_symbol_free_voidp(void *ps);
+XBT_PUBLIC(void) xbt_automaton_propositional_symbol_free_voidp(void *ps);

 
 XBT_PUBLIC(void) xbt_automaton_free(xbt_automaton_t a);
 
 
 XBT_PUBLIC(void) xbt_automaton_free(xbt_automaton_t a);
 

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index cc87fe8..9b0650a 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 693bcae..7388684 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2012-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -41,7 +41,7 @@ static size_t heap_ignore_size(void *address){
   return 0;
 }
 
   return 0;
 }
 

-static int compare_global_variables(int region_type, void *d1, void *d2){
+static int compare_global_variables(int region_type, void *d1, void *d2){ /* region_type = 1 -> libsimgrid, region_type = 2 -> binary */

 
   unsigned int cursor = 0;
   size_t offset; 
 
   unsigned int cursor = 0;
   size_t offset; 


@@ -192,7 +192,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       #ifdef MC_VERBOSE
         XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
       #endif
       #ifdef MC_VERBOSE
         XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
       #endif

-     
+

       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);


@@ -261,7 +261,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       #ifdef MC_VERBOSE
         XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
       #endif
       #ifdef MC_VERBOSE
         XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
       #endif

- 
+

       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);


@@ -294,7 +294,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         #ifdef MC_VERBOSE
           XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
         #endif
         #ifdef MC_VERBOSE
           XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
         #endif

-    
+

         xbt_os_timer_free(timer);
         xbt_os_timer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(timer);
         xbt_os_timer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);


@@ -324,7 +324,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         #ifdef MC_VERBOSE
           XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
         #endif
         #ifdef MC_VERBOSE
           XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
         #endif

-    
+

         xbt_os_timer_free(timer);
         xbt_os_timer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
         xbt_os_timer_free(timer);
         xbt_os_timer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);


@@ -357,7 +357,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       #ifdef MC_VERBOSE
         XBT_VERB("Different global variables in binary"); 
       #endif
       #ifdef MC_VERBOSE
         XBT_VERB("Different global variables in binary"); 
       #endif

-    
+

       reset_heap_information();
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       reset_heap_information();
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);


@@ -600,6 +600,7 @@ static int compare_local_variables(char *s1, char *s2){
             #ifdef MC_DEBUG
               XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
             #endif
             #ifdef MC_DEBUG
               XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
             #endif

+

             xbt_dynar_free(&s_tokens1);
             xbt_dynar_free(&s_tokens2);
             xbt_dynar_free(&tokens1);
             xbt_dynar_free(&s_tokens1);
             xbt_dynar_free(&s_tokens2);
             xbt_dynar_free(&tokens1);

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index c52988b..06e03d9 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved.           */
+/* Copyright (c) 2008-2013. Da SimGrid Team. All rights reserved.           */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -11,10 +11,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
 xbt_dynar_t visited_states;
 
 static int is_visited_state(void);
 xbt_dynar_t visited_states;
 
 static int is_visited_state(void);

-static void visited_state_free(mc_safety_visited_state_t state);
+static void visited_state_free(mc_visited_state_t state);

 static void visited_state_free_voidp(void *s);
 
 static void visited_state_free_voidp(void *s);
 

-static void visited_state_free(mc_safety_visited_state_t state){
+static void visited_state_free(mc_visited_state_t state){

   if(state){
     MC_free_snapshot(state->system_state);
     xbt_free(state);
   if(state){
     MC_free_snapshot(state->system_state);
     xbt_free(state);


@@ -22,7 +22,7 @@ static void visited_state_free(mc_safety_visited_state_t state){
 }
 
 static void visited_state_free_voidp(void *s){
 }
 
 static void visited_state_free_voidp(void *s){

-  visited_state_free((mc_safety_visited_state_t) * (void **) s);
+  visited_state_free((mc_visited_state_t) * (void **) s);

 }
 
 static int is_visited_state(){
 }
 
 static int is_visited_state(){


@@ -34,8 +34,8 @@ static int is_visited_state(){
 
   MC_SET_RAW_MEM;
 
 
   MC_SET_RAW_MEM;
 

-  mc_safety_visited_state_t new_state = NULL;
-  new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
+  mc_visited_state_t new_state = NULL;
+  new_state = xbt_new0(s_mc_visited_state_t, 1);

   new_state->system_state = MC_take_snapshot();
   new_state->num = mc_stats->expanded_states;
 
   new_state->system_state = MC_take_snapshot();
   new_state->num = mc_stats->expanded_states;
 


@@ -63,13 +63,13 @@ static int is_visited_state(){
     int start = 0;
     int end = xbt_dynar_length(visited_states) - 1;
 
     int start = 0;
     int end = xbt_dynar_length(visited_states) - 1;
 

-    mc_safety_visited_state_t state_test = NULL;
+    mc_visited_state_t state_test = NULL;

     size_t bytes_used_test;
     int same_bytes_not_found = 1;
 
     while(start <= end && same_bytes_not_found){
       cursor = (start + end) / 2;
     size_t bytes_used_test;
     int same_bytes_not_found = 1;
 
     while(start <= end && same_bytes_not_found){
       cursor = (start + end) / 2;

-      state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
+      state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);

       bytes_used_test = state_test->system_state->heap_bytes_used;
       if(bytes_used_test < current_bytes_used)
         start = cursor + 1;
       bytes_used_test = state_test->system_state->heap_bytes_used;
       if(bytes_used_test < current_bytes_used)
         start = cursor + 1;


@@ -90,7 +90,7 @@ static int is_visited_state(){
           /* Search another state with same number of bytes used */
           previous_cursor = cursor - 1;
           while(previous_cursor >= 0){
           /* Search another state with same number of bytes used */
           previous_cursor = cursor - 1;
           while(previous_cursor >= 0){

-            state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
+            state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t);

             bytes_used_test = state_test->system_state->heap_bytes_used;
             if(bytes_used_test != current_bytes_used)
               break;
             bytes_used_test = state_test->system_state->heap_bytes_used;
             if(bytes_used_test != current_bytes_used)
               break;


@@ -108,7 +108,7 @@ static int is_visited_state(){
           }
           next_cursor = cursor + 1;
           while(next_cursor < xbt_dynar_length(visited_states)){
           }
           next_cursor = cursor + 1;
           while(next_cursor < xbt_dynar_length(visited_states)){

-            state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
+            state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t);

             bytes_used_test = state_test->system_state->heap_bytes_used;
             if(bytes_used_test != current_bytes_used)
               break;
             bytes_used_test = state_test->system_state->heap_bytes_used;
             if(bytes_used_test != current_bytes_used)
               break;


@@ -128,7 +128,7 @@ static int is_visited_state(){
       }
     }
 
       }
     }
 

-    state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
+    state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);

     bytes_used_test = state_test->system_state->heap_bytes_used;
 
     if(bytes_used_test < current_bytes_used)
     bytes_used_test = state_test->system_state->heap_bytes_used;
 
     if(bytes_used_test < current_bytes_used)


@@ -174,7 +174,7 @@ void MC_dpor_init()
   MC_SET_RAW_MEM;
 
   initial_state = MC_state_new();
   MC_SET_RAW_MEM;
 
   initial_state = MC_state_new();

-  visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp);
+  visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);

 
   MC_UNSET_RAW_MEM;
 
 
   MC_UNSET_RAW_MEM;
 


@@ -322,8 +322,6 @@ void MC_dpor(void)
 
       }
 
 
       }
 

-      
-

       xbt_fifo_unshift(mc_stack_safety, next_state);
       MC_UNSET_RAW_MEM;
 
       xbt_fifo_unshift(mc_stack_safety, next_state);
       MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index b04debe..970ef80 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -95,16 +95,15 @@ char mc_replay_mode = FALSE;
 double *mc_time = NULL;
 mc_comparison_times_t mc_comp_times = NULL;
 double mc_snapshot_comparison_time;
 double *mc_time = NULL;
 mc_comparison_times_t mc_comp_times = NULL;
 double mc_snapshot_comparison_time;

+mc_stats_t mc_stats = NULL;

 
 /* Safety */
 
 xbt_fifo_t mc_stack_safety = NULL;
 
 /* Safety */
 
 xbt_fifo_t mc_stack_safety = NULL;

-mc_stats_t mc_stats = NULL;

 mc_global_t initial_state_safety = NULL;
 
 /* Liveness */
 
 mc_global_t initial_state_safety = NULL;
 
 /* Liveness */
 

-mc_stats_pair_t mc_stats_pair = NULL;

 xbt_fifo_t mc_stack_liveness = NULL;
 mc_global_t initial_state_liveness = NULL;
 int compare;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_global_t initial_state_liveness = NULL;
 int compare;


@@ -310,13 +309,15 @@ void MC_modelcheck_liveness(){
   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
  
   MC_SET_RAW_MEM;
   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
  
   MC_SET_RAW_MEM;

-  
+ 

   /* Initialize statistics */
   /* Initialize statistics */

-  mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  mc_stats->state_size = 1;

 
   /* Create exploration stack */
   mc_stack_liveness = xbt_fifo_new();
 
 
   /* Create exploration stack */
   mc_stack_liveness = xbt_fifo_new();
 

+  /* Create the initial state */

   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 
   MC_UNSET_RAW_MEM;
   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 
   MC_UNSET_RAW_MEM;


@@ -324,7 +325,7 @@ void MC_modelcheck_liveness(){
   MC_ddfs_init();
 
   /* We're done */
   MC_ddfs_init();
 
   /* We're done */

-  MC_print_statistics_pairs(mc_stats_pair);
+  MC_print_statistics(mc_stats);

   xbt_free(mc_time);
 
   if(raw_mem_set)
   xbt_free(mc_time);
 
   if(raw_mem_set)


@@ -477,7 +478,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item;
   mc_state_t state;
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item;
   mc_state_t state;

-  mc_pair_stateless_t pair;
+  mc_pair_t pair;

   int depth = 1;
 
   XBT_DEBUG("**** Begin Replay ****");
   int depth = 1;
 
   XBT_DEBUG("**** Begin Replay ****");


@@ -496,7 +497,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
     while(depth <= xbt_fifo_size(stack)){
 
 
     while(depth <= xbt_fifo_size(stack)){
 

-      pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);

       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){
       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){


@@ -526,7 +527,8 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
       depth++;
     
       /* Update statistics */

-      mc_stats_pair->visited_pairs++;
+      mc_stats->visited_states++;
+      mc_stats->executed_transitions++;

 
       item = xbt_fifo_get_prev_item(item);
     }
 
       item = xbt_fifo_get_prev_item(item);
     }


@@ -538,7 +540,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
          item != xbt_fifo_get_first_item(stack);
          item = xbt_fifo_get_prev_item(item)) {
 
          item != xbt_fifo_get_first_item(stack);
          item = xbt_fifo_get_prev_item(item)) {
 

-      pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);

       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){
       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){


@@ -568,7 +570,8 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
       depth++;
     
       /* Update statistics */

-      mc_stats_pair->visited_pairs++;
+      mc_stats->visited_states++;
+      mc_stats->executed_transitions++;

     }
   }  
 
     }
   }  
 


@@ -649,13 +652,13 @@ void MC_show_deadlock(smx_simcall_t req)
 
 void MC_show_stack_liveness(xbt_fifo_t stack){
   int value;
 
 void MC_show_stack_liveness(xbt_fifo_t stack){
   int value;

-  mc_pair_stateless_t pair;
+  mc_pair_t pair;

   xbt_fifo_item_t item;
   smx_simcall_t req;
   char *req_str = NULL;
   
   for (item = xbt_fifo_get_last_item(stack);
   xbt_fifo_item_t item;
   smx_simcall_t req;
   char *req_str = NULL;
   
   for (item = xbt_fifo_get_last_item(stack);

-       (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
+       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))

         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
     req = MC_state_get_executed_request(pair->graph_state, &value);
     if(req){
         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
     req = MC_state_get_executed_request(pair->graph_state, &value);
     if(req){


@@ -674,11 +677,11 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 

-  mc_pair_stateless_t pair;
+  mc_pair_t pair;

 
   MC_SET_RAW_MEM;
 
   MC_SET_RAW_MEM;

-  while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
-    pair_stateless_free(pair);
+  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
+    MC_pair_delete(pair);

   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)


@@ -699,18 +702,6 @@ void MC_print_statistics(mc_stats_t stats)
     (double)stats->expanded_states / stats->state_size); */
 }
 
     (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);
-
-  if(mmalloc_get_current_heap() == raw_heap)
-    MC_UNSET_RAW_MEM;
-}
-

 void MC_assert(int prop)
 {
   if (MC_is_active() && !prop){
 void MC_assert(int prop)
 {
   if (MC_is_active() && !prop){


@@ -732,7 +723,7 @@ static void MC_assert_pair(int prop){
     //XBT_INFO("Counter-example execution trace:");
     MC_show_stack_liveness(mc_stack_liveness);
     //MC_dump_snapshot_stack(mc_snapshot_stack);
     //XBT_INFO("Counter-example execution trace:");
     MC_show_stack_liveness(mc_stack_liveness);
     //MC_dump_snapshot_stack(mc_snapshot_stack);

-    MC_print_statistics_pairs(mc_stats_pair);
+    MC_print_statistics(mc_stats);

     xbt_abort();
   }
 }
     xbt_abort();
   }
 }


@@ -781,7 +772,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
   if (_mc_property_automaton == NULL)
     _mc_property_automaton = xbt_automaton_new();
 
   if (_mc_property_automaton == NULL)
     _mc_property_automaton = xbt_automaton_new();
 

-  xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
+  xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);

 
   MC_UNSET_RAW_MEM;
 
 
   MC_UNSET_RAW_MEM;
 


@@ -865,7 +856,7 @@ void MC_remove_ignore_heap(void *address, size_t size){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;

-  
+

   unsigned int cursor = 0;
   int start = 0;
   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
   unsigned int cursor = 0;
   int start = 0;
   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 06265cb..ac9b74d 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -10,56 +10,24 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 

-xbt_dynar_t reached_pairs;
+/********* Global variables *********/
+
+xbt_dynar_t acceptance_pairs;

 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
 
 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
 

-int create_dump(int pair)
-{
-   // Try to enable core dumps
-  struct rlimit core_limit;
-  core_limit.rlim_cur = RLIM_INFINITY;
-  core_limit.rlim_max = RLIM_INFINITY;
-  
-  if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
-    fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
-  
-  int status;
-  switch(fork()){
-  case 0:
-    // We are the child process -- run the actual program
-    xbt_abort();
-    break;
-    
-  case -1:
-    // An error occurred, shouldn't happen
-    perror("fork");
-    return -1;
-    
-  default:
-    // We are the parent process -- wait for the child process to exit
-    if(wait(&status) < 0)
-      perror("wait");
-    if(WIFSIGNALED(status) && WCOREDUMP(status)){
-      char *core_name = xbt_malloc(20);
-      sprintf(core_name,"core_%d", pair); 
-      rename("core", core_name);
-      free(core_name);
-    }
-  }

 
 

-  return 0;
-}
+/********* Static functions *********/

 
 

-int reached(xbt_state_t st){
+static int is_reached_acceptance_pair(xbt_automaton_state_t st){

 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 

-  mc_pair_reached_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_reached_t, 1);
-  new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
+  mc_acceptance_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+  new_pair->num = xbt_dynar_length(acceptance_pairs) + 1;

   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  
   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  


@@ -68,7 +36,7 @@ int reached(xbt_state_t st){
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;

-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;

   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();


@@ -77,11 +45,11 @@ int reached(xbt_state_t st){
   
   MC_UNSET_RAW_MEM;
   
   
   MC_UNSET_RAW_MEM;
   

-  if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
+  if(xbt_dynar_is_empty(acceptance_pairs)){

 
     MC_SET_RAW_MEM;
 
     MC_SET_RAW_MEM;

-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    /* New acceptance pair */
+    xbt_dynar_push(acceptance_pairs, &new_pair); 

     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)


@@ -94,13 +62,13 @@ int reached(xbt_state_t st){
     MC_SET_RAW_MEM;
     
     cursor = 0;
     MC_SET_RAW_MEM;
     
     cursor = 0;

-    mc_pair_reached_t pair_test = NULL;
+    mc_acceptance_pair_t pair_test = NULL;

      
      

-    xbt_dynar_foreach(reached_pairs, cursor, pair_test){
+    xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){

       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))

-        XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb);
-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+        XBT_DEBUG("****** Pair reached #%d ******", pair_test->num);
+      if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
+        if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){

           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             
             if(raw_mem_set)
           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             
             if(raw_mem_set)


@@ -118,8 +86,8 @@ int reached(xbt_state_t st){
       }
     }
 
       }
     }
 

-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    /* New acceptance pair */
+    xbt_dynar_push(acceptance_pairs, &new_pair); 

     
     MC_UNSET_RAW_MEM;
 
     
     MC_UNSET_RAW_MEM;
 


@@ -134,22 +102,22 @@ int reached(xbt_state_t st){
 }
 
 
 }
 
 

-void set_pair_reached(xbt_state_t st){
+static void set_acceptance_pair_reached(xbt_automaton_state_t st){

 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;
 

-  mc_pair_reached_t pair = NULL;
-  pair = xbt_new0(s_mc_pair_reached_t, 1);
-  pair->nb = xbt_dynar_length(reached_pairs) + 1;
+  mc_acceptance_pair_t pair = NULL;
+  pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+  pair->num = xbt_dynar_length(acceptance_pairs) + 1;

   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   pair->system_state = MC_take_snapshot();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;
   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   pair->system_state = MC_take_snapshot();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;

-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;

   int res;
   int_f_void_t f;
 
   int res;
   int_f_void_t f;
 


@@ -159,7 +127,7 @@ void set_pair_reached(xbt_state_t st){
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
 
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
 

-  xbt_dynar_push(reached_pairs, &pair); 
+  xbt_dynar_push(acceptance_pairs, &pair); 

   
   MC_UNSET_RAW_MEM;
 
   
   MC_UNSET_RAW_MEM;
 


@@ -168,7 +136,7 @@ void set_pair_reached(xbt_state_t st){
     
 }
 
     
 }
 

-int visited(xbt_state_t st){
+static int is_visited_pair(xbt_automaton_state_t st){

 
   if(_sg_mc_visited == 0)
     return 0;
 
   if(_sg_mc_visited == 0)
     return 0;


@@ -177,8 +145,8 @@ int visited(xbt_state_t st){
 
   MC_SET_RAW_MEM;
 
 
   MC_SET_RAW_MEM;
 

-  mc_pair_visited_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_visited_t, 1);
+  mc_visited_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_visited_pair_t, 1);

   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  
   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  


@@ -187,7 +155,7 @@ int visited(xbt_state_t st){
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;

-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;

   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();


@@ -213,13 +181,13 @@ int visited(xbt_state_t st){
     MC_SET_RAW_MEM;
     
     cursor = 0;
     MC_SET_RAW_MEM;
     
     cursor = 0;

-    mc_pair_visited_t pair_test = NULL;
+    mc_visited_pair_t pair_test = NULL;

      
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
      
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);

-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+      if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
+        if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){

           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             if(raw_mem_set)
               MC_SET_RAW_MEM;
           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             if(raw_mem_set)
               MC_SET_RAW_MEM;


@@ -253,15 +221,7 @@ int visited(xbt_state_t st){
   }
 }
 
   }
 }
 

-void MC_pair_delete(mc_pair_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  xbt_free(pair);
-}
-
-
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l){
+static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){

   
   switch(l->type){
   case 0 : {
   
   switch(l->type){
   case 0 : {


@@ -280,7 +240,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
   }
   case 3 : { 
     unsigned int cursor = 0;
   }
   case 3 : { 
     unsigned int cursor = 0;

-    xbt_propositional_symbol_t p = NULL;
+    xbt_automaton_propositional_symbol_t p = NULL;

     int_f_void_t f;
     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
     int_f_void_t f;
     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){


@@ -299,9 +259,9 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 }
 
 
 }
 
 

-/********************* Double-DFS stateless *******************/
+/********* Free functions *********/

 
 

-void pair_visited_free(mc_pair_visited_t pair){
+static void visited_pair_free(mc_visited_pair_t pair){

   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);


@@ -309,32 +269,11 @@ void pair_visited_free(mc_pair_visited_t pair){
   }
 }
 
   }
 }
 

-void pair_visited_free_voidp(void *p){
-  pair_visited_free((mc_pair_visited_t) * (void **) p);
+static void visited_pair_free_voidp(void *p){
+  visited_pair_free((mc_visited_pair_t) * (void **) p);

 }
 
 }
 

-void pair_stateless_free(mc_pair_stateless_t pair){
-  xbt_free(pair->graph_state->system_state);
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  xbt_free(pair);
-}
-
-void pair_stateless_free_voidp(void *p){
-  pair_stateless_free((mc_pair_stateless_t) * (void **) p);
-}
-
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
-  mc_pair_stateless_t p = NULL;
-  p = xbt_new0(s_mc_pair_stateless_t, 1);
-  p->automaton_state = st;
-  p->graph_state = sg;
-  p->requests = r;
-  mc_stats_pair->expanded_pairs++;
-  return p;
-}
-
-void pair_reached_free(mc_pair_reached_t pair){
+static void acceptance_pair_free(mc_acceptance_pair_t pair){

   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);


@@ -342,10 +281,14 @@ void pair_reached_free(mc_pair_reached_t pair){
   }
 }
 
   }
 }
 

-void pair_reached_free_voidp(void *p){
-  pair_reached_free((mc_pair_reached_t) * (void **) p);
+static void acceptance_pair_free_voidp(void *p){
+  acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);

 }
 
 }
 

+
+/********* DDFS Algorithm *********/
+
+

 void MC_ddfs_init(void){
 
   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 void MC_ddfs_init(void){
 
   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);


@@ -354,7 +297,7 @@ void MC_ddfs_init(void){
   XBT_DEBUG("Double-DFS init");
   XBT_DEBUG("**************************************************");
 
   XBT_DEBUG("Double-DFS init");
   XBT_DEBUG("**************************************************");
 

-  mc_pair_stateless_t mc_initial_pair = NULL;
+  mc_pair_t mc_initial_pair = NULL;

   mc_state_t initial_graph_state = NULL;
   smx_process_t process; 
 
   mc_state_t initial_graph_state = NULL;
   smx_process_t process; 
 


@@ -363,16 +306,16 @@ void MC_ddfs_init(void){
 
   MC_SET_RAW_MEM;
 
 
   MC_SET_RAW_MEM;
 

-  initial_graph_state = MC_state_pair_new();
+  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);
     }
   }
 
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
       MC_state_interleave_process(initial_graph_state, process);
     }
   }
 

-  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
-  visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp);
-  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
+  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
+  successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);

 
   /* Save the initial state */
   initial_state_liveness->snapshot = MC_take_snapshot();
 
   /* Save the initial state */
   initial_state_liveness->snapshot = MC_take_snapshot();


@@ -380,13 +323,13 @@ void MC_ddfs_init(void){
   MC_UNSET_RAW_MEM; 
   
   unsigned int cursor = 0;
   MC_UNSET_RAW_MEM; 
   
   unsigned int cursor = 0;

-  xbt_state_t state;
+  xbt_automaton_state_t automaton_state;

 
 

-  xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
-    if(state->type == -1){
+  xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
+    if(automaton_state->type == -1){

       
       MC_SET_RAW_MEM;
       
       MC_SET_RAW_MEM;

-      mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+      mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));

       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
       MC_UNSET_RAW_MEM;
       
       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
       MC_UNSET_RAW_MEM;
       


@@ -398,14 +341,14 @@ void MC_ddfs_init(void){
       MC_ddfs(0);
 
     }else{
       MC_ddfs(0);
 
     }else{

-      if(state->type == 2){
+      if(automaton_state->type == 2){

       
         MC_SET_RAW_MEM;
       
         MC_SET_RAW_MEM;

-        mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+        mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));

         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
         MC_UNSET_RAW_MEM;
 
         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
         MC_UNSET_RAW_MEM;
 

-        set_pair_reached(state);
+        set_acceptance_pair_reached(automaton_state);

 
         if(cursor != 0){
           MC_restore_snapshot(initial_state_liveness->snapshot);
 
         if(cursor != 0){
           MC_restore_snapshot(initial_state_liveness->snapshot);


@@ -429,17 +372,15 @@ void MC_ddfs_init(void){
 
 void MC_ddfs(int search_cycle){
 
 
 void MC_ddfs(int search_cycle){
 

-  //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-

   smx_process_t process;
   smx_process_t process;

-  mc_pair_stateless_t current_pair = NULL;
+  mc_pair_t current_pair = NULL;

 
   if(xbt_fifo_size(mc_stack_liveness) == 0)
     return;
 
 
   /* Get current pair */
 
   if(xbt_fifo_size(mc_stack_liveness) == 0)
     return;
 
 
   /* Get current pair */

-  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
+  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));

 
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;


@@ -447,24 +388,22 @@ void MC_ddfs(int search_cycle){
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  

-  mc_stats_pair->visited_pairs++;
-
-  //sleep(1);
+  mc_stats->visited_states++;

 
   int value;
   mc_state_t next_graph_state = NULL;
   smx_simcall_t req = NULL;
   char *req_str;
 
 
   int value;
   mc_state_t next_graph_state = NULL;
   smx_simcall_t req = NULL;
   char *req_str;
 

-  xbt_transition_t transition_succ;
+  xbt_automaton_transition_t transition_succ;

   unsigned int cursor = 0;
   int res;
 
   unsigned int cursor = 0;
   int res;
 

-  mc_pair_stateless_t next_pair = NULL;
-  mc_pair_stateless_t pair_succ;
+  mc_pair_t next_pair = NULL;
+  mc_pair_t pair_succ;

 
 

-  mc_pair_stateless_t remove_pair;
-  mc_pair_reached_t remove_pair_reached;
+  mc_pair_t pair_to_remove;
+  mc_acceptance_pair_t acceptance_pair_to_remove;

   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 


@@ -491,7 +430,7 @@ void MC_ddfs(int search_cycle){
         MC_SET_RAW_MEM;
 
         /* Create the new expanded graph_state */
         MC_SET_RAW_MEM;
 
         /* Create the new expanded graph_state */

-        next_graph_state = MC_state_pair_new();
+        next_graph_state = MC_state_new();

 
         /* Get enabled process and insert it in the interleave set of the next graph_state */
         xbt_swag_foreach(process, simix_global->process_list){
 
         /* Get enabled process and insert it in the interleave set of the next graph_state */
         xbt_swag_foreach(process, simix_global->process_list){


@@ -518,7 +457,7 @@ void MC_ddfs(int search_cycle){
 
           if(res == 1){ // enabled transition in automaton
             MC_SET_RAW_MEM;
 
           if(res == 1){ // enabled transition in automaton
             MC_SET_RAW_MEM;

-            next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+            next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));

             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }
             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }


@@ -533,7 +472,7 @@ void MC_ddfs(int search_cycle){
   
           if(res == 2){ // true transition in automaton
             MC_SET_RAW_MEM;
   
           if(res == 2){ // true transition in automaton
             MC_SET_RAW_MEM;

-            next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+            next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));

             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }
             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }


@@ -548,7 +487,7 @@ void MC_ddfs(int search_cycle){
 
             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
           
 
             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
           

-              if(reached(pair_succ->automaton_state)){
+              if(is_reached_acceptance_pair(pair_succ->automaton_state)){

         
                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 
         
                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 


@@ -558,12 +497,12 @@ void MC_ddfs(int search_cycle){
                 XBT_INFO("Counter-example that violates formula :");
                 MC_show_stack_liveness(mc_stack_liveness);
                 MC_dump_stack_liveness(mc_stack_liveness);
                 XBT_INFO("Counter-example that violates formula :");
                 MC_show_stack_liveness(mc_stack_liveness);
                 MC_dump_stack_liveness(mc_stack_liveness);

-                MC_print_statistics_pairs(mc_stats_pair);
+                MC_print_statistics(mc_stats);

                 xbt_abort();
 
               }else{
 
                 xbt_abort();
 
               }else{
 

-                if(visited(pair_succ->automaton_state)){
+                if(is_visited_pair(pair_succ->automaton_state)){

 
                   XBT_DEBUG("Next pair already visited !");
                   break;
 
                   XBT_DEBUG("Next pair already visited !");
                   break;


@@ -572,7 +511,7 @@ void MC_ddfs(int search_cycle){
 
                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 
 
                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 

-                  XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                  XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
                   MC_SET_RAW_MEM;
                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 
                   MC_SET_RAW_MEM;
                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);


@@ -586,7 +525,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
 
             }else{
 

-              if(visited(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state)){

 
                 XBT_DEBUG("Next pair already visited !");
                 break;
 
                 XBT_DEBUG("Next pair already visited !");
                 break;


@@ -604,7 +543,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
 
           }else{
 

-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state)){

 
               XBT_DEBUG("Next pair already visited !");
               break;
 
               XBT_DEBUG("Next pair already visited !");
               break;


@@ -615,11 +554,11 @@ void MC_ddfs(int search_cycle){
 
                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
       
 
                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
       

-                set_pair_reached(pair_succ->automaton_state); 
+                set_acceptance_pair_reached(pair_succ->automaton_state); 

 
                 search_cycle = 1;
 
 
                 search_cycle = 1;
 

-                XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
               }
 
 
               }
 


@@ -653,7 +592,7 @@ void MC_ddfs(int search_cycle){
       MC_SET_RAW_MEM;
 
       /* Create the new expanded graph_state */
       MC_SET_RAW_MEM;
 
       /* Create the new expanded graph_state */

-      next_graph_state = MC_state_pair_new();
+      next_graph_state = MC_state_new();

 
       xbt_dynar_reset(successors);
 
 
       xbt_dynar_reset(successors);
 


@@ -667,7 +606,7 @@ void MC_ddfs(int search_cycle){
 
         if(res == 1){ // enabled transition in automaton
           MC_SET_RAW_MEM;
 
         if(res == 1){ // enabled transition in automaton
           MC_SET_RAW_MEM;

-          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+          next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));

           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }
           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }


@@ -682,7 +621,7 @@ void MC_ddfs(int search_cycle){
   
         if(res == 2){ // true transition in automaton
           MC_SET_RAW_MEM;
   
         if(res == 2){ // true transition in automaton
           MC_SET_RAW_MEM;

-          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+          next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));

           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }
           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }


@@ -697,7 +636,7 @@ void MC_ddfs(int search_cycle){
 
           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
 
           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 

-            if(reached(pair_succ->automaton_state)){
+            if(is_reached_acceptance_pair(pair_succ->automaton_state)){

            
               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
         
            
               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
         


@@ -707,12 +646,12 @@ void MC_ddfs(int search_cycle){
               XBT_INFO("Counter-example that violates formula :");
               MC_show_stack_liveness(mc_stack_liveness);
               MC_dump_stack_liveness(mc_stack_liveness);
               XBT_INFO("Counter-example that violates formula :");
               MC_show_stack_liveness(mc_stack_liveness);
               MC_dump_stack_liveness(mc_stack_liveness);

-              MC_print_statistics_pairs(mc_stats_pair);
+              MC_print_statistics(mc_stats);

               xbt_abort();
 
             }else{
 
               xbt_abort();
 
             }else{
 

-              if(visited(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state)){

                 
                 XBT_DEBUG("Next pair already visited !");
                 break;
                 
                 XBT_DEBUG("Next pair already visited !");
                 break;


@@ -721,7 +660,7 @@ void MC_ddfs(int search_cycle){
 
                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
         
 
                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
         

-                XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
                 MC_SET_RAW_MEM;
                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 
                 MC_SET_RAW_MEM;
                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);


@@ -735,7 +674,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
             
 
           }else{
             

-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state)){

               
               XBT_DEBUG("Next pair already visited !");
               break;
               
               XBT_DEBUG("Next pair already visited !");
               break;


@@ -755,7 +694,7 @@ void MC_ddfs(int search_cycle){
 
         }else{
       
 
         }else{
       

-          if(visited(pair_succ->automaton_state)){
+          if(is_visited_pair(pair_succ->automaton_state)){

 
             XBT_DEBUG("Next pair already visited !");
             break;
 
             XBT_DEBUG("Next pair already visited !");
             break;


@@ -764,11 +703,11 @@ void MC_ddfs(int search_cycle){
 
             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
 
             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 

-              set_pair_reached(pair_succ->automaton_state);
+              set_acceptance_pair_reached(pair_succ->automaton_state);

          
               search_cycle = 1;
 
          
               search_cycle = 1;
 

-              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
             }
 
 
             }
 


@@ -793,7 +732,7 @@ void MC_ddfs(int search_cycle){
   }else{
     
     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
   }else{
     
     XBT_WARN("/!\\ Max depth reached ! /!\\ ");

-    if(current_pair->requests > 0){
+    if(MC_state_interleave_size(current_pair->graph_state) > 0){

       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
     }
       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
     }


@@ -808,17 +747,14 @@ void MC_ddfs(int search_cycle){
 
   
   MC_SET_RAW_MEM;
 
   
   MC_SET_RAW_MEM;

-  remove_pair = xbt_fifo_shift(mc_stack_liveness);
-  xbt_fifo_remove(mc_stack_liveness, remove_pair);
-  remove_pair = NULL;
+  pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
+  xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
+  pair_to_remove = NULL;

   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){

-    remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
-    pair_reached_free(remove_pair_reached);
-    remove_pair_reached = NULL;
+    acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t);
+    acceptance_pair_free(acceptance_pair_to_remove);
+    acceptance_pair_to_remove = NULL;

   }
   MC_UNSET_RAW_MEM;
 
   }
   MC_UNSET_RAW_MEM;
 

-  /*if(initial_state_liveness->raw_mem_set)
-    MC_SET_RAW_MEM;*/
-

 }
 }

diff --git a/src/mc/mc_memory.c b/src/mc/mc_memory.c
index f104773..82b4b51 100644 (file)
--- a/src/mc/mc_memory.c
+++ b/src/mc/mc_memory.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */

diff --git a/src/mc/mc_pair.c b/src/mc/mc_pair.c
new file mode 100644 (file)
index 0000000..9e8ff3e
--- /dev/null
+++ b/src/mc/mc_pair.c
@@ -0,0 +1,24 @@
+/* Copyright (c) 2013 Da SimGrid Team. All rights reserved.            */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "mc_private.h"
+
+mc_pair_t MC_pair_new(mc_state_t gs, xbt_automaton_state_t as, int r){
+  mc_pair_t p = NULL;
+  p = xbt_new0(s_mc_pair_t, 1);
+  p->automaton_state = as;
+  p->graph_state = gs;
+  p->system_state = NULL;
+  p->requests = r;
+  return p;
+}
+
+void MC_pair_delete(mc_pair_t p){
+  p->automaton_state = NULL;
+  if(p->system_state)
+    MC_free_snapshot(p->system_state);
+  MC_state_delete(p->graph_state);
+  xbt_free(p);
+}

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index b2f9a1b..6a46fd6 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -1,4 +1,4 @@
-/* Copyright (c) 2007-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2007-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -63,6 +63,7 @@ void snapshot_stack_free_voidp(void *s);
 int is_stack_ignore_variable(char *frame, char *var_name);
 
 /********************************* MC Global **********************************/
 int is_stack_ignore_variable(char *frame, char *var_name);
 
 /********************************* MC Global **********************************/

+

 extern double *mc_time;
 extern FILE *dot_output;
 extern const char* colors[10];
 extern double *mc_time;
 extern FILE *dot_output;
 extern const char* colors[10];


@@ -78,7 +79,9 @@ void MC_init(void);
 void MC_init_dot_output(void);
 int SIMIX_pre_mc_random(smx_simcall_t simcall);
 
 void MC_init_dot_output(void);
 int SIMIX_pre_mc_random(smx_simcall_t simcall);
 

+

 /********************************* Requests ***********************************/
 /********************************* Requests ***********************************/

+

 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
 char* MC_request_to_string(smx_simcall_t req, int value);
 unsigned int MC_request_testany_fail(smx_simcall_t req);
 int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2);
 char* MC_request_to_string(smx_simcall_t req, int value);
 unsigned int MC_request_testany_fail(smx_simcall_t req);


@@ -91,6 +94,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value);
 
 
 /******************************** States **************************************/
 
 
 /******************************** States **************************************/

+

 /* Possible exploration status of a process in a state */
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */
 /* Possible exploration status of a process in a state */
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */


@@ -130,7 +134,9 @@ 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);
 
 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 ************************************/
 /****************************** Statistics ************************************/

+

 typedef struct mc_stats {
   unsigned long state_size;
   unsigned long visited_states;
 typedef struct mc_stats {
   unsigned long state_size;
   unsigned long visited_states;


@@ -138,18 +144,10 @@ typedef struct mc_stats {
   unsigned long executed_transitions;
 } s_mc_stats_t, *mc_stats_t;
 
   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_t mc_stats;

-extern mc_stats_pair_t mc_stats_pair;

 
 void MC_print_statistics(mc_stats_t);
 
 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. */
 
 /********************************** MEMORY ******************************/
 /* The possible memory modes for the modelchecker are standard and raw. */


@@ -175,6 +173,7 @@ extern void *raw_heap;
 #define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
 #define MC_UNSET_RAW_MEM  mmalloc_set_current_heap(std_heap)
 
 #define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
 #define MC_UNSET_RAW_MEM  mmalloc_set_current_heap(std_heap)
 

+

 /******************************* MEMORY MAPPINGS ***************************/
 /* These functions and data structures implements a binary interface for   */
 /* the proc maps ascii interface                                           */
 /******************************* MEMORY MAPPINGS ***************************/
 /* These functions and data structures implements a binary interface for   */
 /* the proc maps ascii interface                                           */


@@ -201,6 +200,8 @@ typedef struct s_memory_map {
 
 } s_memory_map_t, *memory_map_t;
 
 
 } s_memory_map_t, *memory_map_t;
 

+
+void MC_init_memory_map_info(void);

 memory_map_t get_memory_map(void);
 void free_memory_map(memory_map_t map);
 void get_libsimgrid_plt_section(void);
 memory_map_t get_memory_map(void);
 void free_memory_map(memory_map_t map);
 void get_libsimgrid_plt_section(void);


@@ -221,6 +222,7 @@ extern void *end_got_plt_libsimgrid;
 extern void *start_got_plt_binary;
 extern void *end_got_plt_binary;
 
 extern void *start_got_plt_binary;
 extern void *end_got_plt_binary;
 

+

 /********************************** Snapshot comparison **********************************/
 
 typedef struct s_mc_comparison_times{
 /********************************** Snapshot comparison **********************************/
 
 typedef struct s_mc_comparison_times{


@@ -243,9 +245,11 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_s
 void print_comparison_times(void);
 
 //#define MC_DEBUG 1
 void print_comparison_times(void);
 
 //#define MC_DEBUG 1

-//#define MC_VERBOSE 1
+#define MC_VERBOSE 1
+
+
+/********************************** DPOR for safety property **************************************/

 
 

-/********************************** DPOR for safety  **************************************/

 typedef enum {
   e_mc_reduce_unset,
   e_mc_reduce_none,
 typedef enum {
   e_mc_reduce_unset,
   e_mc_reduce_none,


@@ -254,17 +258,18 @@ typedef enum {
 
 extern e_mc_reduce_t mc_reduce_kind;
 extern mc_global_t initial_state_safety;
 
 extern e_mc_reduce_t mc_reduce_kind;
 extern mc_global_t initial_state_safety;

+extern xbt_fifo_t mc_stack_safety;

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

-typedef struct s_mc_safety_visited_state{
+typedef struct s_mc_visited_state{

   mc_snapshot_t system_state;
   int num;
   mc_snapshot_t system_state;
   int num;

-}s_mc_safety_visited_state_t, *mc_safety_visited_state_t;
+}s_mc_visited_state_t, *mc_visited_state_t;

 
 
 
 

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

 
 extern xbt_fifo_t mc_stack_liveness;
 extern mc_global_t initial_state_liveness;
 
 extern xbt_fifo_t mc_stack_liveness;
 extern mc_global_t initial_state_liveness;


@@ -273,66 +278,37 @@ extern int compare;
 extern xbt_dynar_t mc_stack_comparison_ignore;
 extern xbt_dynar_t mc_data_bss_comparison_ignore;
 
 extern xbt_dynar_t mc_stack_comparison_ignore;
 extern xbt_dynar_t mc_data_bss_comparison_ignore;
 

-

 typedef struct s_mc_pair{
   mc_snapshot_t system_state;
   mc_state_t graph_state;
 typedef struct s_mc_pair{
   mc_snapshot_t system_state;
   mc_state_t graph_state;

-  xbt_state_t automaton_state;
+  xbt_automaton_state_t automaton_state;
+  int requests;

 }s_mc_pair_t, *mc_pair_t;
 
 }s_mc_pair_t, *mc_pair_t;
 

-typedef struct s_mc_pair_reached{
-  int nb;
-  xbt_state_t automaton_state;
+typedef struct s_mc_acceptance_pair{
+  int num;
+  xbt_automaton_state_t automaton_state;

   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;
   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;

-}s_mc_pair_reached_t, *mc_pair_reached_t;
+}s_mc_acceptance_pair_t, *mc_acceptance_pair_t;

 
 

-typedef struct s_mc_pair_visited{
-  xbt_state_t automaton_state;
+typedef struct s_mc_visited_pair{
+  xbt_automaton_state_t automaton_state;

   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;
   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;

-}s_mc_pair_visited_t, *mc_pair_visited_t;
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l);
-
-int reached(xbt_state_t st);
-void set_pair_reached(xbt_state_t st);
-int visited(xbt_state_t st);
-
-void MC_pair_delete(mc_pair_t pair);
-mc_state_t MC_state_pair_new(void);
-void pair_reached_free(mc_pair_reached_t pair);
-void pair_reached_free_voidp(void *p);
-void pair_visited_free(mc_pair_visited_t pair);
-void pair_visited_free_voidp(void *p);
-void MC_init_memory_map_info(void);
-
-int get_heap_region_index(mc_snapshot_t s);
-
-/* **** Double-DFS stateless **** */
+  int num;
+}s_mc_visited_pair_t, *mc_visited_pair_t;

 
 

-typedef struct s_mc_pair_stateless{
-  mc_state_t graph_state;
-  xbt_state_t automaton_state;
-  int requests;
-}s_mc_pair_stateless_t, *mc_pair_stateless_t;
+mc_pair_t MC_pair_new(mc_state_t sg, xbt_automaton_state_t st, int r);
+void MC_pair_delete(mc_pair_t);

 
 

-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r);

 void MC_ddfs_init(void);
 void MC_ddfs(int search_cycle);
 void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);
 void MC_ddfs_init(void);
 void MC_ddfs(int search_cycle);
 void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);

-void pair_stateless_free(mc_pair_stateless_t pair);
-void pair_stateless_free_voidp(void *p);

 
 

-/********************************** Configuration of MC **************************************/
-extern xbt_fifo_t mc_stack_safety;
-
-/****** Core dump ******/

 
 

-int create_dump(int pair);
-
-/****** Local variables with DWARF ******/
+/********************************** Local variables with DWARF **********************************/

 
 typedef enum {
   e_dw_loclist,
 
 typedef enum {
   e_dw_loclist,


@@ -431,7 +407,8 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
 void print_local_variables(xbt_dict_t list);
 xbt_dict_t MC_get_location_list(const char *elf_file);
 
 void print_local_variables(xbt_dict_t list);
 xbt_dict_t MC_get_location_list(const char *elf_file);
 

-/**** Global variables ****/
+
+/********************************** Global variables with objdump **********************************/

 
 typedef struct s_global_variable{
   char *name;
 
 typedef struct s_global_variable{
   char *name;

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 2bf890d..c25a0bc 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index a78a72e..59cca4e 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -23,18 +23,6 @@ mc_state_t MC_state_new()
   return state;
 }
 
   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
 /**
  * \brief Deletes a state data structure
  * \param trans The state to be deleted

diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c
index 1606b2d..b431523 100644 (file)
--- a/src/mc/memory_map.c
+++ b/src/mc/memory_map.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */

diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c
index 8824c52..7e0916a 100644 (file)
--- a/src/xbt/automaton/automaton.c
+++ b/src/xbt/automaton/automaton.c
@@ -11,26 +11,26 @@
 xbt_automaton_t xbt_automaton_new(){
   xbt_automaton_t automaton = NULL;
   automaton = xbt_new0(struct xbt_automaton, 1);
 xbt_automaton_t xbt_automaton_new(){
   xbt_automaton_t automaton = NULL;
   automaton = xbt_new0(struct xbt_automaton, 1);

-  automaton->states = xbt_dynar_new(sizeof(xbt_state_t), xbt_state_free_voidp);
-  automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
-  automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), xbt_propositional_symbol_free_voidp);
+  automaton->states = xbt_dynar_new(sizeof(xbt_automaton_state_t), xbt_automaton_state_free_voidp);
+  automaton->transitions = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp);
+  automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_automaton_propositional_symbol_t), xbt_automaton_propositional_symbol_free_voidp);

   return automaton;
 }
 
   return automaton;
 }
 

-xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){
-  xbt_state_t state = NULL;
-  state = xbt_new0(struct xbt_state, 1);
+xbt_automaton_state_t xbt_automaton_state_new(xbt_automaton_t a, int type, char* id){
+  xbt_automaton_state_t state = NULL;
+  state = xbt_new0(struct xbt_automaton_state, 1);

   state->type = type;
   state->id = strdup(id);
   state->type = type;
   state->id = strdup(id);

-  state->in = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
-  state->out = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); 
+  state->in = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp);
+  state->out = xbt_dynar_new(sizeof(xbt_automaton_transition_t), xbt_automaton_transition_free_voidp); 

   xbt_dynar_push(a->states, &state);
   return state;
 }
 
   xbt_dynar_push(a->states, &state);
   return state;
 }
 

-xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label){
-  xbt_transition_t transition = NULL;
-  transition = xbt_new0(struct xbt_transition, 1);
+xbt_automaton_transition_t xbt_automaton_transition_new(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst, xbt_automaton_exp_label_t label){
+  xbt_automaton_transition_t transition = NULL;
+  transition = xbt_new0(struct xbt_automaton_transition, 1);

   if(src != NULL){
     xbt_dynar_push(src->out, &transition);
     transition->src = src;
   if(src != NULL){
     xbt_dynar_push(src->out, &transition);
     transition->src = src;


@@ -44,30 +44,30 @@ xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src
   return transition;
 }
 
   return transition;
 }
 

-xbt_exp_label_t xbt_automaton_new_label(int type, ...){
-  xbt_exp_label_t label = NULL;
-  label = xbt_new0(struct xbt_exp_label, 1);
+xbt_automaton_exp_label_t xbt_automaton_exp_label_new(int type, ...){
+  xbt_automaton_exp_label_t label = NULL;
+  label = xbt_new0(struct xbt_automaton_exp_label, 1);

   label->type = type;
 
   va_list ap;
   va_start(ap, type);
   switch(type){
   case 0 : {
   label->type = type;
 
   va_list ap;
   va_start(ap, type);
   switch(type){
   case 0 : {

-    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
-    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+    xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+    xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);

     label->u.or_and.left_exp = left;
     label->u.or_and.right_exp = right;
     break;
   }
   case 1 : {
     label->u.or_and.left_exp = left;
     label->u.or_and.right_exp = right;
     break;
   }
   case 1 : {

-    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
-    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+    xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+    xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);

     label->u.or_and.left_exp = left;
     label->u.or_and.right_exp = right;
     break;
   }
   case 2 : {
     label->u.or_and.left_exp = left;
     label->u.or_and.right_exp = right;
     break;
   }
   case 2 : {

-    xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
+    xbt_automaton_exp_label_t exp_not = va_arg(ap, xbt_automaton_exp_label_t);

     label->u.exp_not = exp_not;
     break;
   }
     label->u.exp_not = exp_not;
     break;
   }


@@ -90,8 +90,8 @@ xbt_dynar_t xbt_automaton_get_transitions(xbt_automaton_t a){
   return a->transitions;
 }
 
   return a->transitions;
 }
 

-xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst){
-  xbt_transition_t transition;
+xbt_automaton_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_automaton_state_t src, xbt_automaton_state_t dst){
+  xbt_automaton_transition_t transition;

   unsigned int cursor;
   xbt_dynar_foreach(src->out, cursor, transition){
     if((transition->src == src) && (transition->dst == dst))
   unsigned int cursor;
   xbt_dynar_foreach(src->out, cursor, transition){
     if((transition->src == src) && (transition->dst == dst))


@@ -100,34 +100,34 @@ xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src
   return NULL;
 }
 
   return NULL;
 }
 

-xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){
+xbt_automaton_state_t xbt_automaton_transition_get_source(xbt_automaton_transition_t t){

   return t->src;
 }
 
   return t->src;
 }
 

-xbt_state_t xbt_automaton_transition_get_destination(xbt_transition_t t){
+xbt_automaton_state_t xbt_automaton_transition_get_destination(xbt_automaton_transition_t t){

   return t->dst;
 }
 
   return t->dst;
 }
 

-void xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src){
+void xbt_automaton_transition_set_source(xbt_automaton_transition_t t, xbt_automaton_state_t src){

   t->src = src;
   xbt_dynar_push(src->out,&t);
 }
 
   t->src = src;
   xbt_dynar_push(src->out,&t);
 }
 

-void xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst){
+void xbt_automaton_transition_set_destination(xbt_automaton_transition_t t, xbt_automaton_state_t dst){

   t->dst = dst;
   xbt_dynar_push(dst->in,&t);
 }
 
   t->dst = dst;
   xbt_dynar_push(dst->in,&t);
 }
 

-xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_state_t s){
+xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_automaton_state_t s){

   return s->out;
 }
 
   return s->out;
 }
 

-xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_state_t s){
+xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_automaton_state_t s){

   return s->in;
 }
 
   return s->in;
 }
 

-xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
-  xbt_state_t state = NULL;
+xbt_automaton_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
+  xbt_automaton_state_t state = NULL;

   unsigned int cursor = 0;
   xbt_dynar_foreach(a->states, cursor, state){
    if(strcmp(state->id, id)==0)
   unsigned int cursor = 0;
   xbt_dynar_foreach(a->states, cursor, state){
    if(strcmp(state->id, id)==0)


@@ -136,9 +136,9 @@ xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
   return NULL;
 }
 
   return NULL;
 }
 

-void  xbt_automaton_display(xbt_automaton_t a){
+void xbt_automaton_display(xbt_automaton_t a){

   unsigned int cursor = 0;
   unsigned int cursor = 0;

-  xbt_state_t state = NULL;
+  xbt_automaton_state_t state = NULL;

 
   printf("\n\nEtat courant : %s\n", a->current_state->id);
 
 
   printf("\n\nEtat courant : %s\n", a->current_state->id);
 


@@ -150,36 +150,36 @@ void  xbt_automaton_display(xbt_automaton_t a){
   }
 
   cursor=0;
   }
 
   cursor=0;

-  xbt_transition_t transition = NULL;
+  xbt_automaton_transition_t transition = NULL;

   printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions));
   
   xbt_dynar_foreach(a->transitions, cursor, transition){
     printf("label :");
   printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions));
   
   xbt_dynar_foreach(a->transitions, cursor, transition){
     printf("label :");

-    xbt_automaton_display_exp(transition->label);
+    xbt_automaton_exp_label_display(transition->label);

     printf(", %s -> %s\n", transition->src->id, transition->dst->id);
   }
 }
 
     printf(", %s -> %s\n", transition->src->id, transition->dst->id);
   }
 }
 

-void xbt_automaton_display_exp(xbt_exp_label_t label){
+void xbt_automaton_exp_label_display(xbt_automaton_exp_label_t label){

 
   switch(label->type){
   case 0 :
     printf("(");
 
   switch(label->type){
   case 0 :
     printf("(");

-    xbt_automaton_display_exp(label->u.or_and.left_exp);
+    xbt_automaton_exp_label_display(label->u.or_and.left_exp);

     printf(" || ");
     printf(" || ");

-    xbt_automaton_display_exp(label->u.or_and.right_exp);
+    xbt_automaton_exp_label_display(label->u.or_and.right_exp);

     printf(")");
     break;
   case 1 : 
     printf("(");
     printf(")");
     break;
   case 1 : 
     printf("(");

-    xbt_automaton_display_exp(label->u.or_and.left_exp);
+    xbt_automaton_exp_label_display(label->u.or_and.left_exp);

     printf(" && ");
     printf(" && ");

-    xbt_automaton_display_exp(label->u.or_and.right_exp);
+    xbt_automaton_exp_label_display(label->u.or_and.right_exp);

     printf(")");
     break;
   case 2 : 
     printf("(!");
     printf(")");
     break;
   case 2 : 
     printf("(!");

-    xbt_automaton_display_exp(label->u.exp_not);
+    xbt_automaton_exp_label_display(label->u.exp_not);

     printf(")");
     break;
   case 3 :
     printf(")");
     break;
   case 3 :


@@ -192,20 +192,20 @@ void xbt_automaton_display_exp(xbt_exp_label_t label){
 
 }
 
 
 }
 

-xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
+xbt_automaton_state_t xbt_automaton_get_current_state(xbt_automaton_t a){

   return a->current_state;
 }
 
   return a->current_state;
 }
 

-xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){
-  xbt_propositional_symbol_t prop_symb = NULL;
-  prop_symb = xbt_new0(struct xbt_propositional_symbol, 1);
+xbt_automaton_propositional_symbol_t xbt_automaton_propositional_symbol_new(xbt_automaton_t a, const char* id, void* fct){
+  xbt_automaton_propositional_symbol_t prop_symb = NULL;
+  prop_symb = xbt_new0(struct xbt_automaton_propositional_symbol, 1);

   prop_symb->pred = strdup(id);
   prop_symb->function = fct;
   xbt_dynar_push(a->propositional_symbols, &prop_symb);
   return prop_symb;
 }
 
   prop_symb->pred = strdup(id);
   prop_symb->function = fct;
   xbt_dynar_push(a->propositional_symbols, &prop_symb);
   return prop_symb;
 }
 

-int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
+int xbt_automaton_state_compare(xbt_automaton_state_t s1, xbt_automaton_state_t s2){

 
   /* single id for each state, id and type sufficient for comparison*/
 
 
   /* single id for each state, id and type sufficient for comparison*/
 


@@ -219,22 +219,22 @@ int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
 
 }
 
 
 }
 

-int automaton_transition_compare(const void *t1, const void *t2){
+int xbt_automaton_transition_compare(const void *t1, const void *t2){

 
 

-  if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src))
+  if(xbt_automaton_state_compare(((xbt_automaton_transition_t)t1)->src, ((xbt_automaton_transition_t)t2)->src))

     return 1;
   
     return 1;
   

-  if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst))
+  if(xbt_automaton_state_compare(((xbt_automaton_transition_t)t1)->dst, ((xbt_automaton_transition_t)t2)->dst))

     return 1;
 
     return 1;
 

-  if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label))
+  if(xbt_automaton_exp_label_compare(((xbt_automaton_transition_t)t1)->label,((xbt_automaton_transition_t)t2)->label))

     return 1;
 
   return 0;
   
 }
 
     return 1;
 
   return 0;
   
 }
 

-int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
+int xbt_automaton_exp_label_compare(xbt_automaton_exp_label_t l1, xbt_automaton_exp_label_t l2){

 
   if(l1->type != l2->type)
     return 1;
 
   if(l1->type != l2->type)
     return 1;


@@ -243,14 +243,14 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 
   case 0 : // OR 
   case 1 : // AND
 
   case 0 : // OR 
   case 1 : // AND

-    if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
+    if(xbt_automaton_exp_label_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))

       return 1;
     else
       return 1;
     else

-      return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
+      return xbt_automaton_exp_label_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);

     break;
 
   case 2 : // NOT
     break;
 
   case 2 : // NOT

-    return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not);
+    return xbt_automaton_exp_label_compare(l1->u.exp_not, l2->u.exp_not);

     break;
 
   case 3 : // predicat
     break;
 
   case 3 : // predicat


@@ -270,7 +270,7 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 }
 
 
 }
 
 

-int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
+int xbt_automaton_propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){

 
   int *iptr1, *iptr2;
   unsigned int cursor;
 
   int *iptr1, *iptr2;
   unsigned int cursor;


@@ -288,11 +288,11 @@ int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
 
 /************ Free functions ****************/
 
 
 /************ Free functions ****************/
 

-static void xbt_transition_free(xbt_transition_t t);
-static void xbt_exp_label_free(xbt_exp_label_t e);
-static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps);
+static void xbt_automaton_transition_free(xbt_automaton_transition_t t);
+static void xbt_automaton_exp_label_free(xbt_automaton_exp_label_t e);
+static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_symbol_t ps);

 
 

-void xbt_state_free(xbt_state_t s){
+void xbt_automaton_state_free(xbt_automaton_state_t s){

   if(s){
     xbt_free(s->id);
     xbt_dynar_free(&(s->in));
   if(s){
     xbt_free(s->id);
     xbt_dynar_free(&(s->in));


@@ -302,32 +302,32 @@ void xbt_state_free(xbt_state_t s){
   }
 }
 
   }
 }
 

-void xbt_state_free_voidp(void *s){
-  xbt_state_free((xbt_state_t) * (void **) s);
+void xbt_automaton_state_free_voidp(void *s){
+  xbt_automaton_state_free((xbt_automaton_state_t) * (void **) s);

 }
 
 }
 

-static void xbt_transition_free(xbt_transition_t t){
+static void xbt_automaton_transition_free(xbt_automaton_transition_t t){

   if(t){
   if(t){

-    xbt_exp_label_free(t->label);
+    xbt_automaton_exp_label_free(t->label);

     xbt_free(t);
     t = NULL;
   }
 }
 
     xbt_free(t);
     t = NULL;
   }
 }
 

-void xbt_transition_free_voidp(void *t){
-  xbt_transition_free((xbt_transition_t) * (void **) t);
+void xbt_automaton_transition_free_voidp(void *t){
+  xbt_automaton_transition_free((xbt_automaton_transition_t) * (void **) t);

 }
 
 }
 

-static void xbt_exp_label_free(xbt_exp_label_t e){
+static void xbt_automaton_exp_label_free(xbt_automaton_exp_label_t e){

   if(e){
     switch(e->type){
     case 0:
     case 1:
   if(e){
     switch(e->type){
     case 0:
     case 1:

-      xbt_exp_label_free(e->u.or_and.left_exp);
-      xbt_exp_label_free(e->u.or_and.right_exp);
+      xbt_automaton_exp_label_free(e->u.or_and.left_exp);
+      xbt_automaton_exp_label_free(e->u.or_and.right_exp);

       break;
     case 2:
       break;
     case 2:

-      xbt_exp_label_free(e->u.exp_not);
+      xbt_automaton_exp_label_free(e->u.exp_not);

       break;
     case 3:
       xbt_free(e->u.predicat);
       break;
     case 3:
       xbt_free(e->u.predicat);


@@ -340,11 +340,11 @@ static void xbt_exp_label_free(xbt_exp_label_t e){
   }
 }
 
   }
 }
 

-void xbt_exp_label_free_voidp(void *e){
-  xbt_exp_label_free((xbt_exp_label_t) * (void **) e);
+void xbt_automaton_exp_label_free_voidp(void *e){
+  xbt_automaton_exp_label_free((xbt_automaton_exp_label_t) * (void **) e);

 }
 
 }
 

-static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){
+static void xbt_automaton_propositional_symbol_free(xbt_automaton_propositional_symbol_t ps){

   if(ps){
     xbt_free(ps->pred);
     xbt_free(ps);
   if(ps){
     xbt_free(ps->pred);
     xbt_free(ps);


@@ -352,8 +352,8 @@ static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){
   }
 }
 
   }
 }
 

-void xbt_propositional_symbol_free_voidp(void *ps){
-  xbt_propositional_symbol_free((xbt_propositional_symbol_t) * (void **) ps);
+void xbt_automaton_propositional_symbol_free_voidp(void *ps){
+  xbt_automaton_propositional_symbol_free((xbt_automaton_propositional_symbol_t) * (void **) ps);

 }
 
 void xbt_automaton_free(xbt_automaton_t a){
 }
 
 void xbt_automaton_free(xbt_automaton_t a){


@@ -361,7 +361,7 @@ void xbt_automaton_free(xbt_automaton_t a){
     xbt_dynar_free(&(a->propositional_symbols));
     xbt_dynar_free(&(a->transitions));
     xbt_dynar_free(&(a->states));
     xbt_dynar_free(&(a->propositional_symbols));
     xbt_dynar_free(&(a->transitions));
     xbt_dynar_free(&(a->states));

-    xbt_state_free(a->current_state);
+    xbt_automaton_state_free(a->current_state);

     xbt_free(a);
     a = NULL;
   }
     xbt_free(a);
     a = NULL;
   }

diff --git a/src/xbt/automaton/automatonparse_promela.c b/src/xbt/automaton/automatonparse_promela.c
index 9736dd1..34dcbc5 100644 (file)
--- a/src/xbt/automaton/automatonparse_promela.c
+++ b/src/xbt/automaton/automatonparse_promela.c
@@ -25,10 +25,10 @@ static void new_state(char* id, int src){
     }
   }
 
     }
   }
 

-  xbt_state_t state = NULL;
+  xbt_automaton_state_t state = NULL;

   state = xbt_automaton_state_exists(parsed_automaton, id_state);
   if(state == NULL){
   state = xbt_automaton_state_exists(parsed_automaton, id_state);
   if(state == NULL){

-    state = xbt_automaton_new_state(parsed_automaton, type, id_state);
+    state = xbt_automaton_state_new(parsed_automaton, type, id_state);

   }
 
   if(type==-1)
   }
 
   if(type==-1)


@@ -39,48 +39,48 @@ static void new_state(char* id, int src){
     
 }
 
     
 }
 

-static void new_transition(char* id, xbt_exp_label_t label){
+static void new_transition(char* id, xbt_automaton_exp_label_t label){

 
   char* id_state = strdup(id);
 
   char* id_state = strdup(id);

-  xbt_state_t state_dst = NULL;
+  xbt_automaton_state_t state_dst = NULL;

   new_state(id, 0);
   state_dst = xbt_automaton_state_exists(parsed_automaton, id_state);
   new_state(id, 0);
   state_dst = xbt_automaton_state_exists(parsed_automaton, id_state);

-  xbt_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);
+  xbt_automaton_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);

   
   //xbt_transition_t trans = NULL;
   
   //xbt_transition_t trans = NULL;

-  xbt_automaton_new_transition(parsed_automaton, state_src, state_dst, label);
+  xbt_automaton_transition_new(parsed_automaton, state_src, state_dst, label);

 
 }
 
 
 }
 

-static xbt_exp_label_t new_label(int type, ...){
-  xbt_exp_label_t label = NULL;
+static xbt_automaton_exp_label_t new_label(int type, ...){
+  xbt_automaton_exp_label_t label = NULL;

   va_list ap;
   va_start(ap,type);
   switch(type){
   case 0 : {
   va_list ap;
   va_start(ap,type);
   switch(type){
   case 0 : {

-    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
-    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
-    label = xbt_automaton_new_label(type, left, right);
+    xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+    xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);
+    label = xbt_automaton_exp_label_new(type, left, right);

     break;
   }
   case 1 : {
     break;
   }
   case 1 : {

-    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
-    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
-    label = xbt_automaton_new_label(type, left, right);
+    xbt_automaton_exp_label_t left = va_arg(ap, xbt_automaton_exp_label_t);
+    xbt_automaton_exp_label_t right = va_arg(ap, xbt_automaton_exp_label_t);
+    label = xbt_automaton_exp_label_new(type, left, right);

     break;
   }
   case 2 : {
     break;
   }
   case 2 : {

-    xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
-    label = xbt_automaton_new_label(type, exp_not);
+    xbt_automaton_exp_label_t exp_not = va_arg(ap, xbt_automaton_exp_label_t);
+    label = xbt_automaton_exp_label_new(type, exp_not);

     break;
   }
   case 3 : {
     char* p = va_arg(ap, char*);
     break;
   }
   case 3 : {
     char* p = va_arg(ap, char*);

-    label = xbt_automaton_new_label(type, p);
+    label = xbt_automaton_exp_label_new(type, p);

     break;
   }
   case 4 : {
     break;
   }
   case 4 : {

-    label = xbt_automaton_new_label(type);
+    label = xbt_automaton_exp_label_new(type);

     break;
   }
   }
     break;
   }
   }

diff --git a/src/xbt/automaton/parserPromela.tab.hacc b/src/xbt/automaton/parserPromela.tab.hacc
index 51a4ae6..676dd59 100644 (file)
--- a/src/xbt/automaton/parserPromela.tab.hacc
+++ b/src/xbt/automaton/parserPromela.tab.hacc
@@ -72,7 +72,7 @@ typedef union YYSTYPE
   double real;
   int integer;
   char* string;
   double real;
   int integer;
   char* string;

-  xbt_exp_label_t label;
+  xbt_automaton_exp_label_t label;

 
 
 
 
 
 

diff --git a/src/xbt/automaton/parserPromela.yacc b/src/xbt/automaton/parserPromela.yacc
index f88ac53..c74d2ce 100644 (file)
--- a/src/xbt/automaton/parserPromela.yacc
+++ b/src/xbt/automaton/parserPromela.yacc
@@ -11,7 +11,7 @@ void yyerror(const char *s);
   double real;
   int integer;
   char* string;
   double real;
   int integer;
   char* string;

-  xbt_exp_label_t label;
+  xbt_automaton_exp_label_t label;

 }
 
 %token NEVER
 }
 
 %token NEVER