X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7da2926d0733ff0683f31aeea176ce71e127264f..633e10e9d14bde1225977c96e1da28d942a21074:/src/mc/mc_safety.h diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h index 14bcd4fe5c..8e7503f4da 100644 --- a/src/mc/mc_safety.h +++ b/src/mc/mc_safety.h @@ -9,37 +9,43 @@ #include +#include +#include + #include + #include -#include -#include "mc_forward.hpp" -#include "mc_state.h" +#include + +#include "src/mc/mc_forward.hpp" +#include "src/mc/mc_state.h" -SG_BEGIN_DECL() +namespace simgrid { +namespace mc { -typedef enum { - e_mc_reduce_unset, - e_mc_reduce_none, - e_mc_reduce_dpor -} e_mc_reduce_t; +enum class ReductionMode { + unset, + none, + dpor, +}; -extern XBT_PRIVATE e_mc_reduce_t mc_reduce_kind; +extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode; -void MC_modelcheck_safety(void); +struct XBT_PRIVATE VisitedState { + simgrid::mc::Snapshot* system_state = nullptr; + size_t heap_bytes_used = 0; + int nb_processes = 0; + int num = 0; + int other_num = 0; // dot_output for -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; + VisitedState(); + ~VisitedState(); +}; -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 std::vector> visited_states; +XBT_PRIVATE std::unique_ptr is_visited_state(mc_state_t graph_state); -SG_END_DECL() +} +} #endif