X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2b1c48aa8ff28c0d706779f2a69aadc5333e48ab..fc90483d87af7c41aa3dabc00a43585c6ea928e0:/src/mc/mc_private.h diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 9b36857fca..86431c79a4 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -6,6 +6,7 @@ #ifndef MC_PRIVATE_H #define MC_PRIVATE_H +#include "simgrid_config.h" #include #include #include "mc/mc.h" @@ -182,6 +183,8 @@ typedef struct s_memory_map { } s_memory_map_t, *memory_map_t; memory_map_t get_memory_map(void); +void free_memory_map(memory_map_t map); +void get_plt_section(void); /********************************** DPOR for safety **************************************/ @@ -202,6 +205,7 @@ void MC_init_safety(void); extern mc_snapshot_t initial_snapshot_liveness; extern xbt_automaton_t _mc_property_automaton; +extern int compare; typedef struct s_mc_pair{ mc_snapshot_t system_state; @@ -214,48 +218,17 @@ typedef struct s_mc_pair_reached{ xbt_state_t automaton_state; xbt_dynar_t prop_ato; mc_snapshot_t system_state; - //xbt_dict_t rdv_points; }s_mc_pair_reached_t, *mc_pair_reached_t; -typedef struct s_mc_pair_visited{ - xbt_state_t automaton_state; - xbt_dynar_t prop_ato; - mc_snapshot_t system_state; - int search_cycle; -}s_mc_pair_visited_t, *mc_pair_visited_t; - -typedef struct s_mc_pair_visited_hash{ - xbt_state_t automaton_state; - xbt_dynar_t prop_ato; - unsigned int *hash_regions; - int search_cycle; -}s_mc_pair_visited_hash_t, *mc_pair_visited_hash_t; - -typedef struct s_mc_pair_reached_hash{ - xbt_state_t automaton_state; - xbt_dynar_t prop_ato; - unsigned int *hash_regions; -}s_mc_pair_reached_hash_t, *mc_pair_reached_hash_t; - - - int MC_automaton_evaluate_label(xbt_exp_label_t l); mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); int reached(xbt_state_t st); void set_pair_reached(xbt_state_t st); -int reached_hash(xbt_state_t st); -void set_pair_reached_hash(xbt_state_t st); int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); -int visited(xbt_state_t st, int search_cycle); -void set_pair_visited(xbt_state_t st, int search_cycle); -int visited_hash(xbt_state_t st, int search_cycle); -void set_pair_visited_hash(xbt_state_t st, int search_cycle); -unsigned int hash_region(char *str, int str_len); -int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2); /* **** Double-DFS stateless **** */