X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/96cedde3cdbc0b8ffc3f096a1b65d021b0226f99..90136cb8268510961005b533a970c61282a1f37c:/src/mc/checker/LivenessChecker.hpp diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp index 25517a02ed..e90523ca9d 100644 --- a/src/mc/checker/LivenessChecker.hpp +++ b/src/mc/checker/LivenessChecker.hpp @@ -7,19 +7,14 @@ #ifndef SIMGRID_MC_LIVENESS_CHECKER_HPP #define SIMGRID_MC_LIVENESS_CHECKER_HPP -#include +#include "src/mc/checker/Checker.hpp" +#include "src/mc/mc_state.hpp" +#include "xbt/automaton.hpp" -#include #include #include #include -#include "src/mc/checker/Checker.hpp" -#include "src/mc/mc_state.hpp" -#include -#include -#include - namespace simgrid { namespace mc { @@ -63,30 +58,32 @@ public: explicit LivenessChecker(Session& session); ~LivenessChecker() = default; void run() override; - RecordTrace getRecordTrace() override; - std::vector getTextualTrace() override; - void logState() override; + RecordTrace get_record_trace() override; + std::vector get_textual_trace() override; + void log_state() override; + private: int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2); - 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); + std::shared_ptr> get_proposition_values(); + std::shared_ptr insert_acceptance_pair(simgrid::mc::Pair* pair); + int insert_visited_pair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair); + void show_acceptance_cycle(std::size_t depth); void replay(); - void removeAcceptancePair(int pair_num); - void purgeVisitedPairs(); + void remove_acceptance_pair(int pair_num); + void purge_visited_pairs(); void backtrack(); - std::shared_ptr newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr> propositions); + std::shared_ptr create_pair(Pair* pair, xbt_automaton_state_t state, + std::shared_ptr> propositions); // A stack of (application_state, automaton_state) pairs for DFS exploration: - std::list> explorationStack_; - std::list> acceptancePairs_; - std::list> visitedPairs_; - unsigned long visitedPairsCount_ = 0; - unsigned long expandedPairsCount_ = 0; - unsigned long expandedStatesCount_ = 0; - int previousPair_ = 0; - std::string previousRequest_; + std::list> exploration_stack_; + std::list> acceptance_pairs_; + std::list> visited_pairs_; + unsigned long visited_pairs_count_ = 0; + unsigned long expanded_pairs_count_ = 0; + unsigned long expanded_states_count_ = 0; + int previous_pair_ = 0; + std::string previous_request_; }; }