X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ba9a4cfeba4eb00e84cd17603fc9654e81445655..11ce6b59ec29ed55d422a0c97a7d734ac1eb7a39:/src/mc/mc_safety.h diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h index 46c5ec95dc..b1cd987846 100644 --- a/src/mc/mc_safety.h +++ b/src/mc/mc_safety.h @@ -9,6 +9,9 @@ #include +#include +#include + #include #include @@ -17,31 +20,18 @@ #include "src/mc/mc_forward.hpp" #include "src/mc/mc_state.h" -SG_BEGIN_DECL() - -typedef enum { - e_mc_reduce_unset, - e_mc_reduce_none, - e_mc_reduce_dpor -} e_mc_reduce_t; - -extern XBT_PRIVATE e_mc_reduce_t mc_reduce_kind; - -int MC_modelcheck_safety(void); +namespace simgrid { +namespace mc { -typedef struct XBT_PRIVATE s_mc_visited_state{ - mc_snapshot_t system_state; - size_t heap_bytes_used; - int nb_processes; - int num; - int other_num; // dot_output for -}s_mc_visited_state_t, *mc_visited_state_t; +enum class ReductionMode { + unset, + none, + dpor, +}; -extern XBT_PRIVATE xbt_dynar_t visited_states; -XBT_PRIVATE mc_visited_state_t is_visited_state(mc_state_t graph_state); -XBT_PRIVATE void visited_state_free(mc_visited_state_t state); -XBT_PRIVATE void visited_state_free_voidp(void *s); +extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode; -SG_END_DECL() +} +} #endif