X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2b1c48aa8ff28c0d706779f2a69aadc5333e48ab..ae7de36436dc212a9537e15b06cf433f50594f63:/src/mc/mc_private.h diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 9b36857fca..30d01cb060 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" @@ -202,6 +203,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 +216,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 **** */