X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0e9f97aeb3a3b0843cf7429cb586e4149636918e..3a70f3d43980112b067cf0f51a8327bdccaf5ef9:/src/mc/LivenessChecker.hpp diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index f12c0b3be1..18c32a0372 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -34,7 +34,7 @@ struct XBT_PRIVATE Pair { bool search_cycle = false; std::shared_ptr graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; - std::vector atomic_propositions; + std::shared_ptr> atomic_propositions; int requests = 0; int depth = 0; bool exploration_started = false; @@ -51,13 +51,13 @@ struct XBT_PRIVATE VisitedPair { int other_num = 0; /* Dot output for */ std::shared_ptr graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; - std::vector atomic_propositions; + std::shared_ptr> atomic_propositions; std::size_t heap_bytes_used = 0; int nb_processes = 0; VisitedPair( int pair_num, xbt_automaton_state_t automaton_state, - std::vector const& atomic_propositions, + std::shared_ptr> atomic_propositions, std::shared_ptr graph_state); ~VisitedPair(); }; @@ -73,7 +73,7 @@ private: int main(); void prepare(); int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2); - std::vector getPropositionValues(); + std::shared_ptr> getPropositionValues(); std::shared_ptr insertAcceptancePair(simgrid::mc::Pair* pair); int insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair); void showAcceptanceCycle(std::size_t depth); @@ -81,7 +81,7 @@ private: void removeAcceptancePair(int pair_num); void purgeVisitedPairs(); void backtrack(); - std::shared_ptr newPair(Pair* pair, xbt_automaton_state_t state); + std::shared_ptr newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr> propositions); public: // A stack of (application_state, automaton_state) pairs for DFS exploration: std::list> explorationStack_;