From: Martin Quinson Date: Tue, 28 May 2019 09:23:03 +0000 (+0200) Subject: mc: snake_case the checkers X-Git-Tag: v3.22.4~53 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/90136cb8268510961005b533a970c61282a1f37c mc: snake_case the checkers --- diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 874875a031..7bc9774812 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -150,7 +150,7 @@ static void MC_report_crash(int status) else XBT_INFO("No core dump was generated by the system."); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) + for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); simgrid::mc::session->log_state(); @@ -164,7 +164,7 @@ static void MC_report_assertion_error() XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) + for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); simgrid::mc::session->log_state(); diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index 96f377a8ca..1089f65a1a 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -117,7 +117,7 @@ void Session::restore_initial_state() void Session::log_state() { - mc_model_checker->getChecker()->logState(); + mc_model_checker->getChecker()->log_state(); if (not _sg_mc_dot_output_file.get().empty()) { fprintf(dot_output, "}\n"); diff --git a/src/mc/checker/Checker.hpp b/src/mc/checker/Checker.hpp index 96a1f205f5..c71f17e1d1 100644 --- a/src/mc/checker/Checker.hpp +++ b/src/mc/checker/Checker.hpp @@ -48,18 +48,19 @@ public: /** Show the current trace/stack * * Could this be handled in the Session/ModelChecker instead? */ - virtual RecordTrace getRecordTrace() = 0; + virtual RecordTrace get_record_trace() = 0; /** Generate a textual execution trace of the simulated application */ - virtual std::vector getTextualTrace() = 0; + virtual std::vector get_textual_trace() = 0; /** Log additional information about the state of the model-checker */ - virtual void logState() = 0; + virtual void log_state() = 0; protected: - Session& getSession() { return *session_; } + Session& get_session() { return *session_; } }; +// External constructors so that the types (and the types of their content) remain hidden XBT_PUBLIC Checker* createLivenessChecker(Session& session); XBT_PUBLIC Checker* createSafetyChecker(Session& session); XBT_PUBLIC Checker* createCommunicationDeterminismChecker(Session& session); diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 24bdad1ba4..31d3df5dc2 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -282,7 +282,7 @@ CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& s) : C CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default; -RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override +RecordTrace CommunicationDeterminismChecker::get_record_trace() // override { RecordTrace res; for (auto const& state : stack_) @@ -290,7 +290,7 @@ RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override return res; } -std::vector CommunicationDeterminismChecker::getTextualTrace() // override +std::vector CommunicationDeterminismChecker::get_textual_trace() // override { std::vector trace; for (auto const& state : stack_) { @@ -302,7 +302,7 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o return trace; } -void CommunicationDeterminismChecker::logState() // override +void CommunicationDeterminismChecker::log_state() // override { if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) { XBT_INFO("******************************************************"); @@ -315,7 +315,7 @@ void CommunicationDeterminismChecker::logState() // override XBT_INFO("******************************************************"); XBT_INFO("%s", this->send_diff); } - XBT_INFO("Expanded states = %lu", expandedStatesCount_); + XBT_INFO("Expanded states = %lu", expanded_states_count_); XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); XBT_INFO("Send-deterministic : %s", not this->send_deterministic ? "No" : "Yes"); @@ -331,7 +331,7 @@ void CommunicationDeterminismChecker::prepare() incomplete_communications_pattern.resize(maxpid); std::unique_ptr initial_state = - std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); + std::unique_ptr(new simgrid::mc::State(++expanded_states_count_)); XBT_DEBUG("********* Start communication determinism verification *********"); @@ -451,7 +451,7 @@ void CommunicationDeterminismChecker::real_run() /* Create the new expanded state */ std::unique_ptr next_state = - std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); + std::unique_ptr(new simgrid::mc::State(++expanded_states_count_)); /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at * least, data are transferred). These communications are incomplete and they cannot be analyzed and compared @@ -459,7 +459,7 @@ void CommunicationDeterminismChecker::real_run() bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done; if (_sg_mc_max_visited_states != 0) - visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots); + visited_state = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), compare_snapshots); else visited_state = nullptr; diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp index 66181d8970..c10d60f0ec 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.hpp +++ b/src/mc/checker/CommunicationDeterminismChecker.hpp @@ -21,12 +21,13 @@ public: explicit CommunicationDeterminismChecker(Session& session); ~CommunicationDeterminismChecker(); void run() override; - RecordTrace getRecordTrace() override; - std::vector getTextualTrace() override; + RecordTrace get_record_trace() override; + std::vector get_textual_trace() override; + private: void prepare(); void real_run(); - void logState() override; + void log_state() override; void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking); void restoreState(); public: @@ -38,8 +39,8 @@ public: private: /** Stack representing the position in the exploration graph */ std::list> stack_; - simgrid::mc::VisitedStates visitedStates_; - unsigned long expandedStatesCount_ = 0; + simgrid::mc::VisitedStates visited_states_; + unsigned long expanded_states_count_ = 0; bool initial_communications_pattern_done = false; bool recv_deterministic = true; diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 2f7a6a9379..89f2581962 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -70,7 +70,7 @@ static bool evaluate_label(xbt_automaton_exp_label_t l, std::vector const& Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} -std::shared_ptr> LivenessChecker::getPropositionValues() +std::shared_ptr> LivenessChecker::get_proposition_values() { std::vector values; unsigned int cursor = 0; @@ -87,13 +87,13 @@ int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::Visi return simgrid::mc::snapshot_compare(s1, s2); } -std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc::Pair* pair) +std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair) { std::shared_ptr new_pair = std::make_shared( pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); - auto res = boost::range::equal_range(acceptancePairs_, new_pair.get(), + auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap()); if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) { @@ -104,22 +104,22 @@ std::shared_ptr LivenessChecker::insertAcceptancePair(simgrid::mc:: || this->compare(pair_test.get(), new_pair.get()) != 0) continue; XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); - explorationStack_.pop_back(); + exploration_stack_.pop_back(); if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, pair_test->num, - this->previousRequest_.c_str()); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, + this->previous_request_.c_str()); return nullptr; } - acceptancePairs_.insert(res.first, new_pair); + acceptance_pairs_.insert(res.first, new_pair); return new_pair; } -void LivenessChecker::removeAcceptancePair(int pair_num) +void LivenessChecker::remove_acceptance_pair(int pair_num) { - for (auto i = acceptancePairs_.begin(); i != acceptancePairs_.end(); ++i) + for (auto i = acceptance_pairs_.begin(); i != acceptance_pairs_.end(); ++i) if ((*i)->num == pair_num) { - acceptancePairs_.erase(i); + acceptance_pairs_.erase(i); break; } } @@ -130,7 +130,7 @@ void LivenessChecker::replay() /* Intermediate backtracking */ if(_sg_mc_checkpoint > 0) { - simgrid::mc::Pair* pair = explorationStack_.back().get(); + simgrid::mc::Pair* pair = exploration_stack_.back().get(); if(pair->graph_state->system_state){ pair->graph_state->system_state->restore(&mc_model_checker->process()); return; @@ -142,8 +142,8 @@ void LivenessChecker::replay() /* Traverse the stack from the initial state and re-execute the transitions */ int depth = 1; - for (std::shared_ptr const& pair : explorationStack_) { - if (pair == explorationStack_.back()) + for (std::shared_ptr const& pair : exploration_stack_) { + if (pair == exploration_stack_.back()) break; std::shared_ptr state = pair->graph_state; @@ -169,11 +169,11 @@ void LivenessChecker::replay() state.get()); } - this->getSession().execute(state->transition); + this->get_session().execute(state->transition); } /* Update statistics */ - visitedPairsCount_++; + visited_pairs_count_++; mc_model_checker->executed_transitions++; depth++; @@ -186,7 +186,7 @@ void LivenessChecker::replay() /** * @brief Checks whether a given pair has already been visited by the algorithm. */ -int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair) +int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair) { if (_sg_mc_max_visited_states == 0) return -1; @@ -195,7 +195,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair visited_pair = std::make_shared(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); - auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(), + auto range = boost::range::equal_range(visited_pairs_, visited_pair.get(), simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap()); for (auto i = range.first; i != range.second; ++i) { @@ -218,18 +218,18 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr visited_pair return (*i)->other_num; } - visitedPairs_.insert(range.first, std::move(visited_pair)); - this->purgeVisitedPairs(); + visited_pairs_.insert(range.first, std::move(visited_pair)); + this->purge_visited_pairs(); return -1; } -void LivenessChecker::purgeVisitedPairs() +void LivenessChecker::purge_visited_pairs() { - if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) { + if (_sg_mc_max_visited_states != 0 && visited_pairs_.size() > (std::size_t)_sg_mc_max_visited_states) { // Remove the oldest entry with a linear search: - visitedPairs_.erase(boost::min_element(visitedPairs_, - [](std::shared_ptr const a, std::shared_ptr const& b) { - return a->num < b->num; } )); + visited_pairs_.erase( + boost::min_element(visited_pairs_, [](std::shared_ptr const a, + std::shared_ptr const& b) { return a->num < b->num; })); } } @@ -237,38 +237,38 @@ LivenessChecker::LivenessChecker(Session& s) : Checker(s) { } -RecordTrace LivenessChecker::getRecordTrace() // override +RecordTrace LivenessChecker::get_record_trace() // override { RecordTrace res; - for (std::shared_ptr const& pair : explorationStack_) + for (std::shared_ptr const& pair : exploration_stack_) res.push_back(pair->graph_state->getTransition()); return res; } -void LivenessChecker::logState() // override +void LivenessChecker::log_state() // override { - XBT_INFO("Expanded pairs = %lu", expandedPairsCount_); - XBT_INFO("Visited pairs = %lu", visitedPairsCount_); + XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_); + XBT_INFO("Visited pairs = %lu", visited_pairs_count_); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); } -void LivenessChecker::showAcceptanceCycle(std::size_t depth) +void LivenessChecker::show_acceptance_cycle(std::size_t depth) { XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("Counter-example that violates formula:"); - for (auto const& s : this->getTextualTrace()) + for (auto const& s : this->get_textual_trace()) XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); simgrid::mc::session->log_state(); XBT_INFO("Counter-example depth: %zu", depth); } -std::vector LivenessChecker::getTextualTrace() // override +std::vector LivenessChecker::get_textual_trace() // override { std::vector trace; - for (std::shared_ptr const& pair : explorationStack_) { + for (std::shared_ptr const& pair : exploration_stack_) { int req_num = pair->graph_state->transition.argument; smx_simcall_t req = &pair->graph_state->executed_req; if (req && req->call != SIMCALL_NONE) @@ -278,13 +278,13 @@ std::vector LivenessChecker::getTextualTrace() // override return trace; } -std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, - std::shared_ptr> propositions) +std::shared_ptr LivenessChecker::create_pair(Pair* current_pair, xbt_automaton_state_t state, + std::shared_ptr> propositions) { - expandedPairsCount_++; - std::shared_ptr next_pair = std::make_shared(expandedPairsCount_); + expanded_pairs_count_++; + std::shared_ptr next_pair = std::make_shared(expanded_pairs_count_); next_pair->automaton_state = state; - next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expandedStatesCount_)); + next_pair->graph_state = std::shared_ptr(new simgrid::mc::State(++expanded_states_count_)); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; @@ -307,20 +307,20 @@ void LivenessChecker::backtrack() { /* Traverse the stack backwards until a pair with a non empty interleave set is found, deleting all the pairs that have it empty in the way. */ - while (not explorationStack_.empty()) { - std::shared_ptr current_pair = explorationStack_.back(); - explorationStack_.pop_back(); + while (not exploration_stack_.empty()) { + std::shared_ptr current_pair = exploration_stack_.back(); + exploration_stack_.pop_back(); if (current_pair->requests > 0) { /* We found a backtracking point */ XBT_DEBUG("Backtracking to depth %d", current_pair->depth); - explorationStack_.push_back(std::move(current_pair)); + exploration_stack_.push_back(std::move(current_pair)); this->replay(); XBT_DEBUG("Backtracking done"); break; } else { XBT_DEBUG("Delete pair %d at depth %d", current_pair->num, current_pair->depth); if (current_pair->automaton_state->type == 1) - this->removeAcceptancePair(current_pair->num); + this->remove_acceptance_pair(current_pair->num); } } } @@ -334,9 +334,9 @@ void LivenessChecker::run() simgrid::mc::session->initialize(); /* Initialize */ - this->previousPair_ = 0; + this->previous_pair_ = 0; - std::shared_ptr> propos = this->getPropositionValues(); + std::shared_ptr> propos = this->get_proposition_values(); // For each initial state of the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: @@ -344,11 +344,11 @@ void LivenessChecker::run() xbt_automaton_state_t automaton_state; xbt_dynar_foreach (simgrid::mc::property_automaton->states, cursor, automaton_state) if (automaton_state->type == -1) - explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos)); + exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos)); /* Actually run the double DFS search for counter-examples */ - while (not explorationStack_.empty()) { - std::shared_ptr current_pair = explorationStack_.back(); + while (not exploration_stack_.empty()) { + std::shared_ptr current_pair = exploration_stack_.back(); /* Update current state in buchi automaton */ simgrid::mc::property_automaton->current_state = current_pair->automaton_state; @@ -365,20 +365,20 @@ void LivenessChecker::run() std::shared_ptr reached_pair; if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) { - reached_pair = this->insertAcceptancePair(current_pair.get()); + reached_pair = this->insert_acceptance_pair(current_pair.get()); if (reached_pair == nullptr) { - this->showAcceptanceCycle(current_pair->depth); + this->show_acceptance_cycle(current_pair->depth); throw simgrid::mc::LivenessError(); } } /* Pair already visited ? stop the exploration on the current path */ if (not current_pair->exploration_started) { - int visited_num = this->insertVisitedPair(reached_pair, current_pair.get()); + int visited_num = this->insert_visited_pair(reached_pair, current_pair.get()); if (visited_num != -1) { if (dot_output != nullptr) { - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, visited_num, - this->previousRequest_.c_str()); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num, + this->previous_request_.c_str()); fflush(dot_output); } XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num); @@ -392,14 +392,13 @@ void LivenessChecker::run() int req_num = current_pair->graph_state->transition.argument; if (dot_output != nullptr) { - if (this->previousPair_ != 0 && this->previousPair_ != current_pair->num) { - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - this->previousPair_, current_pair->num, - this->previousRequest_.c_str()); - this->previousRequest_.clear(); + if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num, + this->previous_request_.c_str()); + this->previous_request_.clear(); } - this->previousPair_ = current_pair->num; - this->previousRequest_ = simgrid::mc::request_get_dot_output(req, req_num); + this->previous_pair_ = current_pair->num; + this->previous_request_ = simgrid::mc::request_get_dot_output(req, req_num); if (current_pair->search_cycle) fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); fflush(dot_output); @@ -412,7 +411,7 @@ void LivenessChecker::run() /* Update stats */ mc_model_checker->executed_transitions++; if (not current_pair->exploration_started) - visitedPairsCount_++; + visited_pairs_count_++; /* Answer the request */ mc_model_checker->handle_simcall(current_pair->graph_state->transition); @@ -424,7 +423,7 @@ void LivenessChecker::run() current_pair->exploration_started = true; /* Get values of atomic propositions (variables used in the property formula) */ - std::shared_ptr> prop_values = this->getPropositionValues(); + std::shared_ptr> prop_values = this->get_proposition_values(); // For each enabled transition in the property automaton, push a // (application_state, automaton_state) pair to the exploration stack: @@ -432,8 +431,7 @@ void LivenessChecker::run() xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as( current_pair->automaton_state->out, i, xbt_automaton_transition_t); if (evaluate_label(transition_succ->label, *prop_values)) - explorationStack_.push_back(this->newPair( - current_pair.get(), transition_succ->dst, prop_values)); + exploration_stack_.push_back(this->create_pair(current_pair.get(), transition_succ->dst, prop_values)); } } diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp index b37b475d63..e90523ca9d 100644 --- a/src/mc/checker/LivenessChecker.hpp +++ b/src/mc/checker/LivenessChecker.hpp @@ -58,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_; }; } diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 6b1c4da47c..796bed5382 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -38,7 +38,7 @@ static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat return snapshot_compare(s1, s2); } -void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state) +void SafetyChecker::check_non_termination(simgrid::mc::State* current_state) { for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) if (snapshot_compare(state->get(), current_state) == 0) { @@ -47,7 +47,7 @@ void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state) XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); XBT_INFO("******************************************"); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) + for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); simgrid::mc::session->log_state(); @@ -56,7 +56,7 @@ void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state) } } -RecordTrace SafetyChecker::getRecordTrace() // override +RecordTrace SafetyChecker::get_record_trace() // override { RecordTrace res; for (auto const& state : stack_) @@ -64,7 +64,7 @@ RecordTrace SafetyChecker::getRecordTrace() // override return res; } -std::vector SafetyChecker::getTextualTrace() // override +std::vector SafetyChecker::get_textual_trace() // override { std::vector trace; for (auto const& state : stack_) { @@ -77,9 +77,9 @@ std::vector SafetyChecker::getTextualTrace() // override return trace; } -void SafetyChecker::logState() // override +void SafetyChecker::log_state() // override { - XBT_INFO("Expanded states = %lu", expandedStatesCount_); + XBT_INFO("Expanded states = %lu", expanded_states_count_); XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); } @@ -109,11 +109,11 @@ void SafetyChecker::run() } // Backtrack if we are revisiting a state we saw previously - if (visitedState_ != nullptr) { + if (visited_state_ != nullptr) { XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", - visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num); + visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num); - visitedState_ = nullptr; + visited_state_ = nullptr; this->backtrack(); continue; } @@ -143,21 +143,21 @@ void SafetyChecker::run() mc_model_checker->executed_transitions++; /* Actually answer the request: let execute the selected request (MCed does one step) */ - this->getSession().execute(state->transition); + this->get_session().execute(state->transition); /* Create the new expanded state (copy the state of MCed into our MCer data) */ std::unique_ptr next_state = - std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); + std::unique_ptr(new simgrid::mc::State(++expanded_states_count_)); if (_sg_mc_termination) - this->checkNonTermination(next_state.get()); + this->check_non_termination(next_state.get()); /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */ if (_sg_mc_max_visited_states > 0) - visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true); + visited_state_ = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), true); /* If this is a new state (or if we don't care about state-equality reduction) */ - if (visitedState_ == nullptr) { + if (visited_state_ == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto& remoteActor : mc_model_checker->process().actors()) { @@ -175,7 +175,7 @@ void SafetyChecker::run() } else if (dot_output != nullptr) std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, - visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num, + visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num, req_str.c_str()); stack_.push_back(std::move(next_state)); @@ -257,7 +257,7 @@ void SafetyChecker::backtrack() /* We found a back-tracking point, let's loop */ XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); - this->restoreState(); + this->restore_state(); XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size()); break; } else { @@ -266,7 +266,7 @@ void SafetyChecker::backtrack() } } -void SafetyChecker::restoreState() +void SafetyChecker::restore_state() { /* Intermediate backtracking */ simgrid::mc::State* last_state = stack_.back().get(); @@ -308,7 +308,7 @@ SafetyChecker::SafetyChecker(Session& s) : Checker(s) XBT_DEBUG("Starting the safety algorithm"); std::unique_ptr initial_state = - std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); + std::unique_ptr(new simgrid::mc::State(++expanded_states_count_)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/checker/SafetyChecker.hpp index f615e6f9c7..1377934919 100644 --- a/src/mc/checker/SafetyChecker.hpp +++ b/src/mc/checker/SafetyChecker.hpp @@ -25,19 +25,20 @@ public: explicit SafetyChecker(Session& session); ~SafetyChecker() = 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: - void checkNonTermination(simgrid::mc::State* current_state); + void check_non_termination(simgrid::mc::State* current_state); void backtrack(); - void restoreState(); + void restore_state(); /** Stack representing the position in the exploration graph */ std::list> stack_; - simgrid::mc::VisitedStates visitedStates_; - std::unique_ptr visitedState_; - unsigned long expandedStatesCount_ = 0; + simgrid::mc::VisitedStates visited_states_; + std::unique_ptr visited_state_; + unsigned long expanded_states_count_ = 0; }; } diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 5e8fff4752..3621458769 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -89,7 +89,7 @@ void MC_show_deadlock() XBT_INFO("*** DEAD-LOCK DETECTED ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) + for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); simgrid::mc::dumpRecordPath(); simgrid::mc::session->log_state(); diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index 115695c3dd..50d659ca40 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -98,7 +98,7 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace) void dumpRecordPath() { - RecordTrace trace = mc_model_checker->getChecker()->getRecordTrace(); + RecordTrace trace = mc_model_checker->getChecker()->get_record_trace(); XBT_INFO("Path = %s", traceToString(trace).c_str()); }