X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/068223d8b457b296adeee39403cda89ffc5baf76..30bf612c3a18711cccade2f179c4a9fc1589ab2e:/src/mc/LivenessChecker.hpp diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 263bde47e8..d5cd324f06 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -7,11 +7,13 @@ #ifndef SIMGRID_MC_LIVENESS_CHECKER_HPP #define SIMGRID_MC_LIVENESS_CHECKER_HPP -#include +#include + +#include +#include #include #include -#include #include #include #include @@ -30,7 +32,7 @@ extern XBT_PRIVATE xbt_automaton_t property_automaton; struct XBT_PRIVATE Pair { int num = 0; int search_cycle = 0; - mc_state_t graph_state = nullptr; /* System state included */ + simgrid::mc::State* graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; simgrid::xbt::unique_ptr atomic_propositions; int requests = 0; @@ -49,15 +51,15 @@ struct XBT_PRIVATE VisitedPair { int num = 0; int other_num = 0; /* Dot output for */ int acceptance_pair = 0; - mc_state_t graph_state = nullptr; /* System state included */ + simgrid::mc::State* graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; simgrid::xbt::unique_ptr atomic_propositions; - size_t heap_bytes_used = 0; + std::size_t heap_bytes_used = 0; int nb_processes = 0; int acceptance_removed = 0; int visited_removed = 0; - VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state); + VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state); ~VisitedPair(); }; @@ -76,8 +78,11 @@ private: simgrid::mc::VisitedPair* insertAcceptancePair(simgrid::mc::Pair* pair); int insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair); void showAcceptanceCycle(std::size_t depth); - void replay(xbt_fifo_t stack); + void replay(); void removeAcceptancePair(int pair_num); +public: // (non-static wannabe) fields + static std::list acceptance_pairs; + static std::list liveness_stack; }; }