X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d656f9465e7b1c36319f86eeafdcec58fe9551a4..b63024606c00dc186c5ed6335449bb92342c8f9c:/src/mc/checker/LivenessChecker.hpp diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp index 1f9be7f6d5..678e0eef4d 100644 --- a/src/mc/checker/LivenessChecker.hpp +++ b/src/mc/checker/LivenessChecker.hpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2007-2017. The SimGrid Team. +/* Copyright (c) 2007-2020. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it @@ -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,31 @@ 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(const 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_; }; }