From: Martin Quinson Date: Mon, 21 Feb 2022 21:25:55 +0000 (+0100) Subject: Rename mc::Checker to mc::Exploration as it defines an exploration algo X-Git-Tag: v3.31~349 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ebadbf7894190d4c66238842db5f8931adb7df5b Rename mc::Checker to mc::Exploration as it defines an exploration algo --- diff --git a/MANIFEST.in b/MANIFEST.in index f5cec521c6..ea185af5bf 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2343,16 +2343,16 @@ include src/mc/api.cpp include src/mc/api.hpp include src/mc/api/State.cpp include src/mc/api/State.hpp -include src/mc/checker/Checker.hpp -include src/mc/checker/CommunicationDeterminismChecker.cpp -include src/mc/checker/LivenessChecker.cpp -include src/mc/checker/LivenessChecker.hpp -include src/mc/checker/SafetyChecker.cpp -include src/mc/checker/SafetyChecker.hpp -include src/mc/checker/UdporChecker.cpp -include src/mc/checker/UdporChecker.hpp -include src/mc/checker/simgrid_mc.cpp include src/mc/compare.cpp +include src/mc/explo/CommunicationDeterminismChecker.cpp +include src/mc/explo/Exploration.hpp +include src/mc/explo/LivenessChecker.cpp +include src/mc/explo/LivenessChecker.hpp +include src/mc/explo/SafetyChecker.cpp +include src/mc/explo/SafetyChecker.hpp +include src/mc/explo/UdporChecker.cpp +include src/mc/explo/UdporChecker.hpp +include src/mc/explo/simgrid_mc.cpp include src/mc/inspect/DwarfExpression.cpp include src/mc/inspect/DwarfExpression.hpp include src/mc/inspect/Frame.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index e3893940ee..2b0d821dae 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -5,7 +5,7 @@ #include "src/mc/ModelChecker.hpp" #include "src/mc/Session.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" @@ -136,9 +136,9 @@ static void MC_report_crash(int status) if (not xbt_log_no_loc) XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No"); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) + for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); - XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str()); + XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str()); session_singleton->log_state(); if (xbt_log_no_loc) { XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); @@ -227,9 +227,9 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : getChecker()->get_textual_trace()) + for (auto const& s : get_exploration()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); - XBT_INFO("Path = %s", getChecker()->get_record_trace().to_string().c_str()); + XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str()); session_singleton->log_state(); this->exit(SIMGRID_MC_EXIT_SAFETY); diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index fd305fb404..8bf67d31d1 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -27,7 +27,7 @@ class ModelChecker { // This is the parent snapshot of the current state: PageStore page_store_{500}; std::unique_ptr remote_process_; - Checker* checker_ = nullptr; + Exploration* exploration_ = nullptr; // Expect MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL std::string simcall_to_string(MessageType type, aid_t aid, int times_considered); @@ -59,8 +59,8 @@ public: void finalize_app(bool terminate_asap = false); - Checker* getChecker() const { return checker_; } - void setChecker(Checker* checker) { checker_ = checker; } + Exploration* get_exploration() const { return exploration_; } + void set_exploration(Exploration* exploration) { exploration_ = exploration; } private: void setup_ignore(); diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index 0fbe964e6d..dffeed7e56 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -4,9 +4,9 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/Session.hpp" -#include "src/mc/checker/Checker.hpp" -#include "src/mc/mc_config.hpp" #include "src/internal_config.h" // HAVE_SMPI +#include "src/mc/explo/Exploration.hpp" +#include "src/mc/mc_config.hpp" #if HAVE_SMPI #include "smpi/smpi.h" #include "src/smpi/include/private.hpp" @@ -116,7 +116,7 @@ void Session::restore_initial_state() const void Session::log_state() const { - model_checker_->getChecker()->log_state(); + model_checker_->get_exploration()->log_state(); if (not _sg_mc_dot_output_file.get().empty()) { fprintf(dot_output, "}\n"); @@ -169,9 +169,9 @@ void Session::check_deadlock() const XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***"); XBT_CINFO(mc_global, "**************************"); XBT_CINFO(mc_global, "Counter-example execution trace:"); - for (auto const& frame : model_checker_->getChecker()->get_textual_trace()) + for (auto const& frame : model_checker_->get_exploration()->get_textual_trace()) XBT_CINFO(mc_global, " %s", frame.c_str()); - XBT_CINFO(mc_global, "Path = %s", model_checker_->getChecker()->get_record_trace().to_string().c_str()); + XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str()); log_state(); throw DeadlockError(); } diff --git a/src/mc/api.cpp b/src/mc/api.cpp index 6590c22751..8ac88e50cf 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -9,7 +9,7 @@ #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/actor/SimcallObserver.hpp" #include "src/mc/Session.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_base.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_pattern.hpp" @@ -85,7 +85,7 @@ xbt::string const& Api::get_actor_name(smx_actor_t actor) const return info->name; } -simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const +simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const { auto session = new simgrid::mc::Session([argv] { int i = 1; @@ -97,22 +97,22 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm xbt_die("The model-checked process failed to exec(%s): %s", argv[i], strerror(errno)); }); - simgrid::mc::Checker* checker; + simgrid::mc::Exploration* explo; switch (algo) { case CheckerAlgorithm::CommDeterminism: - checker = simgrid::mc::create_communication_determinism_checker(session); + explo = simgrid::mc::create_communication_determinism_checker(session); break; case CheckerAlgorithm::UDPOR: - checker = simgrid::mc::create_udpor_checker(session); + explo = simgrid::mc::create_udpor_checker(session); break; case CheckerAlgorithm::Safety: - checker = simgrid::mc::create_safety_checker(session); + explo = simgrid::mc::create_safety_checker(session); break; case CheckerAlgorithm::Liveness: - checker = simgrid::mc::create_liveness_checker(session); + explo = simgrid::mc::create_liveness_checker(session); break; default: @@ -121,8 +121,8 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm // FIXME: session and checker are never deleted simgrid::mc::session_singleton = session; - mc_model_checker->setChecker(checker); - return checker; + mc_model_checker->set_exploration(explo); + return explo; } std::vector& Api::get_actors() const diff --git a/src/mc/api.hpp b/src/mc/api.hpp index 1134b94a32..3889583faf 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -63,7 +63,7 @@ public: return api; } - simgrid::mc::Checker* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const; + simgrid::mc::Exploration* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const; // ACTOR APIs std::vector& get_actors() const; diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp similarity index 95% rename from src/mc/checker/CommunicationDeterminismChecker.cpp rename to src/mc/explo/CommunicationDeterminismChecker.cpp index 4a13814d9d..e2b5d5595b 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -5,7 +5,7 @@ #include "src/kernel/activity/MailboxImpl.hpp" #include "src/mc/Session.hpp" -#include "src/mc/checker/SafetyChecker.hpp" +#include "src/mc/explo/SafetyChecker.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_forward.hpp" @@ -32,15 +32,15 @@ enum class PatternCommunicationType { class PatternCommunication { public: - int num = 0; + int num = 0; uintptr_t comm_addr = 0; PatternCommunicationType type = PatternCommunicationType::send; unsigned long src_proc = 0; unsigned long dst_proc = 0; unsigned mbox = 0; unsigned size = 0; - int tag = 0; - int index = 0; + int tag = 0; + int index = 0; PatternCommunication dup() const { @@ -49,10 +49,10 @@ public: res.comm_addr = this->comm_addr; res.type = this->type; res.src_proc = this->src_proc; - res.dst_proc = this->dst_proc; - res.mbox = this->mbox; + res.dst_proc = this->dst_proc; + res.mbox = this->mbox; res.tag = this->tag; - res.index = this->index; + res.index = this->index; return res; } }; @@ -65,7 +65,7 @@ struct PatternCommunicationList { /********** Checker extension **********/ struct CommDetExtension { - static simgrid::xbt::Extension EXTENSION_ID; + static simgrid::xbt::Extension EXTENSION_ID; std::vector initial_communications_pattern; std::vector> incomplete_communications_pattern; @@ -89,7 +89,7 @@ struct CommDetExtension { void complete_comm_pattern(const CommWaitTransition* transition); void handle_comm_pattern(const Transition* transition); }; -simgrid::xbt::Extension CommDetExtension::EXTENSION_ID; +simgrid::xbt::Extension CommDetExtension::EXTENSION_ID; /********** State Extension ***********/ class StateCommDet { @@ -246,7 +246,7 @@ void CommDetExtension::get_comm_pattern(const Transition* transition) } else if (transition->type_ == Transition::Type::COMM_RECV) { auto* recv = static_cast(transition); - pattern->type = PatternCommunicationType::receive; + pattern->type = PatternCommunicationType::receive; pattern->comm_addr = recv->get_comm(); pattern->tag = recv->get_tag(); } @@ -285,7 +285,6 @@ void CommDetExtension::complete_comm_pattern(const CommWaitTransition* transitio } } - void CommDetExtension::handle_comm_pattern(const Transition* transition) { if (not _sg_mc_comms_determinism && not _sg_mc_send_determinism) @@ -323,9 +322,9 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) } */ -Checker* create_communication_determinism_checker(Session* session) +Exploration* create_communication_determinism_checker(Session* session) { - CommDetExtension::EXTENSION_ID = simgrid::mc::Checker::extension_create(); + CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create(); StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create(); XBT_DEBUG("********* Start communication determinism verification *********"); diff --git a/src/mc/checker/Checker.hpp b/src/mc/explo/Exploration.hpp similarity index 75% rename from src/mc/checker/Checker.hpp rename to src/mc/explo/Exploration.hpp index 542ba9688d..f0f7a3a9d2 100644 --- a/src/mc/checker/Checker.hpp +++ b/src/mc/explo/Exploration.hpp @@ -12,7 +12,7 @@ namespace simgrid { namespace mc { -/** A model-checking algorithm +/** A model-checking exploration algorithm * * This is an abstract base class used to group the data, state, configuration * of a model-checking algorithm. @@ -25,17 +25,17 @@ namespace mc { * `Session` interface (but currently the `Session` interface does not * have all the necessary features). */ // abstract -class Checker : public xbt::Extendable { +class Exploration : public xbt::Extendable { Session* session_; public: - explicit Checker(Session* session) : session_(session) {} + explicit Exploration(Session* session) : session_(session) {} // No copy: - Checker(Checker const&) = delete; - Checker& operator=(Checker const&) = delete; + Exploration(Exploration const&) = delete; + Exploration& operator=(Exploration const&) = delete; - virtual ~Checker() = default; + virtual ~Exploration() = default; /** Main function of this algorithm */ virtual void run() = 0; @@ -59,10 +59,10 @@ public: }; // External constructors so that the types (and the types of their content) remain hidden -XBT_PUBLIC Checker* create_liveness_checker(Session* session); -XBT_PUBLIC Checker* create_safety_checker(Session* session); -XBT_PUBLIC Checker* create_communication_determinism_checker(Session* session); -XBT_PUBLIC Checker* create_udpor_checker(Session* session); +XBT_PUBLIC Exploration* create_liveness_checker(Session* session); +XBT_PUBLIC Exploration* create_safety_checker(Session* session); +XBT_PUBLIC Exploration* create_communication_determinism_checker(Session* session); +XBT_PUBLIC Exploration* create_udpor_checker(Session* session); } // namespace mc } // namespace simgrid diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp similarity index 84% rename from src/mc/checker/LivenessChecker.cpp rename to src/mc/explo/LivenessChecker.cpp index 1a512aaff1..a0073d285b 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -3,7 +3,7 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include "src/mc/checker/LivenessChecker.hpp" +#include "src/mc/explo/LivenessChecker.hpp" #include "src/mc/Session.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" @@ -29,34 +29,31 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, this->graph_state = std::move(graph_state); if (this->graph_state->system_state_ == nullptr) this->graph_state->system_state_ = std::make_shared(pair_num); - this->heap_bytes_used = api::get().get_remote_heap_bytes(); + this->heap_bytes_used = api::get().get_remote_heap_bytes(); this->actors_count = api::get().get_actors().size(); - this->other_num = -1; + this->other_num = -1; this->atomic_propositions = std::move(atomic_propositions); } static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector const& values) { switch (l->type) { - case xbt_automaton_exp_label::AUT_OR: - return evaluate_label(l->u.or_and.left_exp, values) - || evaluate_label(l->u.or_and.right_exp, values); - case xbt_automaton_exp_label::AUT_AND: - return evaluate_label(l->u.or_and.left_exp, values) - && evaluate_label(l->u.or_and.right_exp, values); - case xbt_automaton_exp_label::AUT_NOT: - return not evaluate_label(l->u.exp_not, values); - case xbt_automaton_exp_label::AUT_PREDICAT: - return values.at(api::get().compare_automaton_exp_label(l)) != 0; - case xbt_automaton_exp_label::AUT_ONE: - return true; - default: - xbt_die("Unexpected value for automaton"); + case xbt_automaton_exp_label::AUT_OR: + return evaluate_label(l->u.or_and.left_exp, values) || evaluate_label(l->u.or_and.right_exp, values); + case xbt_automaton_exp_label::AUT_AND: + return evaluate_label(l->u.or_and.left_exp, values) && evaluate_label(l->u.or_and.right_exp, values); + case xbt_automaton_exp_label::AUT_NOT: + return not evaluate_label(l->u.exp_not, values); + case xbt_automaton_exp_label::AUT_PREDICAT: + return values.at(api::get().compare_automaton_exp_label(l)) != 0; + case xbt_automaton_exp_label::AUT_ONE: + return true; + default: + xbt_die("Unexpected value for automaton"); } } -Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) -{} +Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs) {} std::shared_ptr> LivenessChecker::get_proposition_values() const { @@ -71,19 +68,21 @@ std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc auto res = boost::range::equal_range(acceptance_pairs_, new_pair.get(), api::get().compare_pair()); - if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) { - std::shared_ptr const& pair_test = *i; - if (api::get().automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 || - *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || - not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(), new_pair->graph_state->system_state_.get())) - continue; - XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); - exploration_stack_.pop_back(); - if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, - this->previous_request_.c_str()); - return nullptr; - } + if (pair->search_cycle) + for (auto i = res.first; i != res.second; ++i) { + std::shared_ptr const& pair_test = *i; + if (api::get().automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 || + *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || + not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(), + new_pair->graph_state->system_state_.get())) + continue; + XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); + exploration_stack_.pop_back(); + if (dot_output != nullptr) + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, + this->previous_request_.c_str()); + return nullptr; + } acceptance_pairs_.insert(res.first, new_pair); return new_pair; @@ -103,7 +102,7 @@ void LivenessChecker::replay() XBT_DEBUG("**** Begin Replay ****"); /* Intermediate backtracking */ - if(_sg_mc_checkpoint > 0) { + if (_sg_mc_checkpoint > 0) { const Pair* pair = exploration_stack_.back().get(); if (pair->graph_state->system_state_) { api::get().restore_state(pair->graph_state->system_state_); @@ -151,7 +150,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa const VisitedPair* pair_test = i->get(); if (api::get().automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) || - not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(), visited_pair->graph_state->system_state_.get())) + not api::get().snapshot_equal(pair_test->graph_state->system_state_.get(), + visited_pair->graph_state->system_state_.get())) continue; if (pair_test->other_num == -1) visited_pair->other_num = pair_test->num; @@ -160,8 +160,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa if (dot_output == nullptr) XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", visited_pair->num, pair_test->num); else - XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", - visited_pair->num, pair_test->num, visited_pair->other_num); + XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", visited_pair->num, + pair_test->num, visited_pair->other_num); (*i) = std::move(visited_pair); return (*i)->other_num; } @@ -181,7 +181,7 @@ void LivenessChecker::purge_visited_pairs() } } -LivenessChecker::LivenessChecker(Session* session) : Checker(session) {} +LivenessChecker::LivenessChecker(Session* session) : Exploration(session) {} RecordTrace LivenessChecker::get_record_trace() // override { @@ -224,10 +224,10 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt std::shared_ptr> propositions) { ++expanded_pairs_count_; - auto next_pair = std::make_shared(expanded_pairs_count_); - next_pair->automaton_state = state; - next_pair->graph_state = std::make_shared(); - next_pair->atomic_propositions = std::move(propositions); + auto next_pair = std::make_shared(expanded_pairs_count_); + next_pair->automaton_state = state; + next_pair->graph_state = std::make_shared(); + next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; else @@ -372,7 +372,7 @@ void LivenessChecker::run() log_state(); } -Checker* create_liveness_checker(Session* session) +Exploration* create_liveness_checker(Session* session) { return new LivenessChecker(session); } diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp similarity index 84% rename from src/mc/checker/LivenessChecker.hpp rename to src/mc/explo/LivenessChecker.hpp index d2d34dfaa9..ea7c0e6fe4 100644 --- a/src/mc/checker/LivenessChecker.hpp +++ b/src/mc/explo/LivenessChecker.hpp @@ -8,7 +8,7 @@ #define SIMGRID_MC_LIVENESS_CHECKER_HPP #include "src/mc/api/State.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "xbt/automaton.hpp" #include @@ -20,13 +20,13 @@ namespace mc { class XBT_PRIVATE Pair { public: - int num = 0; - bool search_cycle = false; + int num = 0; + bool search_cycle = false; std::shared_ptr graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state = nullptr; std::shared_ptr> atomic_propositions; - int requests = 0; - int depth = 0; + int requests = 0; + int depth = 0; bool exploration_started = false; explicit Pair(unsigned long expanded_pairs); @@ -38,7 +38,7 @@ public: class XBT_PRIVATE VisitedPair { public: int num; - int other_num = 0; /* Dot output for */ + int other_num = 0; /* Dot output for */ std::shared_ptr graph_state = nullptr; /* System state included */ xbt_automaton_state_t automaton_state; std::shared_ptr> atomic_propositions; @@ -49,7 +49,7 @@ public: std::shared_ptr> atomic_propositions, std::shared_ptr graph_state); }; -class XBT_PRIVATE LivenessChecker : public Checker { +class XBT_PRIVATE LivenessChecker : public Exploration { public: explicit LivenessChecker(Session* session); void run() override; @@ -73,9 +73,9 @@ private: std::list> exploration_stack_; std::list> acceptance_pairs_; std::list> visited_pairs_; - unsigned long visited_pairs_count_ = 0; - unsigned long expanded_pairs_count_ = 0; - int previous_pair_ = 0; + unsigned long visited_pairs_count_ = 0; + unsigned long expanded_pairs_count_ = 0; + int previous_pair_ = 0; std::string previous_request_; }; diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/explo/SafetyChecker.cpp similarity index 98% rename from src/mc/checker/SafetyChecker.cpp rename to src/mc/explo/SafetyChecker.cpp index 284acd44b6..07e176da34 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/explo/SafetyChecker.cpp @@ -3,7 +3,7 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include "src/mc/checker/SafetyChecker.hpp" +#include "src/mc/explo/SafetyChecker.hpp" #include "src/mc/Session.hpp" #include "src/mc/VisitedState.hpp" #include "src/mc/mc_config.hpp" @@ -268,7 +268,7 @@ void SafetyChecker::restore_state() } } -SafetyChecker::SafetyChecker(Session* session) : Checker(session) +SafetyChecker::SafetyChecker(Session* session) : Exploration(session) { reductionMode_ = reduction_mode; if (_sg_mc_termination) @@ -309,7 +309,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session) stack_.push_back(std::move(initial_state)); } -Checker* create_safety_checker(Session* session) +Exploration* create_safety_checker(Session* session) { return new SafetyChecker(session); } diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/explo/SafetyChecker.hpp similarity index 97% rename from src/mc/checker/SafetyChecker.hpp rename to src/mc/explo/SafetyChecker.hpp index 3851d39a7f..3cd00c7b89 100644 --- a/src/mc/checker/SafetyChecker.hpp +++ b/src/mc/explo/SafetyChecker.hpp @@ -8,7 +8,7 @@ #define SIMGRID_MC_SAFETY_CHECKER_HPP #include "src/mc/VisitedState.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_safety.hpp" #include @@ -19,7 +19,7 @@ namespace simgrid { namespace mc { -class XBT_PRIVATE SafetyChecker : public Checker { +class XBT_PRIVATE SafetyChecker : public Exploration { ReductionMode reductionMode_ = ReductionMode::unset; long backtrack_count_ = 0; diff --git a/src/mc/checker/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp similarity index 79% rename from src/mc/checker/UdporChecker.cpp rename to src/mc/explo/UdporChecker.cpp index 904e066547..fd932b62a3 100644 --- a/src/mc/checker/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -3,7 +3,7 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include "src/mc/checker/UdporChecker.hpp" +#include "src/mc/explo/UdporChecker.hpp" #include XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification "); @@ -11,7 +11,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety ver namespace simgrid { namespace mc { -UdporChecker::UdporChecker(Session* session) : Checker(session) {} +UdporChecker::UdporChecker(Session* session) : Exploration(session) {} void UdporChecker::run() {} @@ -29,7 +29,7 @@ std::vector UdporChecker::get_textual_trace() void UdporChecker::log_state() {} -Checker* create_udpor_checker(Session* session) +Exploration* create_udpor_checker(Session* session) { return new UdporChecker(session); } diff --git a/src/mc/checker/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp similarity index 87% rename from src/mc/checker/UdporChecker.hpp rename to src/mc/explo/UdporChecker.hpp index 514c7f476a..069c515165 100644 --- a/src/mc/checker/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -7,13 +7,13 @@ #ifndef SIMGRID_MC_UDPOR_CHECKER_HPP #define SIMGRID_MC_UDPOR_CHECKER_HPP -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_record.hpp" namespace simgrid { namespace mc { -class XBT_PRIVATE UdporChecker : public Checker { +class XBT_PRIVATE UdporChecker : public Exploration { public: explicit UdporChecker(Session* session); void run() override; diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp similarity index 90% rename from src/mc/checker/simgrid_mc.cpp rename to src/mc/explo/simgrid_mc.cpp index 5ad9992e89..8da00022da 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/explo/simgrid_mc.cpp @@ -1,14 +1,13 @@ -/* Copyright (c) 2015-2022. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ #include "simgrid/sg_config.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/internal_config.h" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" -#include "src/internal_config.h" #if HAVE_SMPI #include "smpi/smpi.h" @@ -20,8 +19,7 @@ using api = simgrid::mc::Api; -static inline -char** argvdup(int argc, char** argv) +static inline char** argvdup(int argc, char** argv) { auto* argv_copy = new char*[argc + 1]; std::memcpy(argv_copy, argv, sizeof(char*) * argc); diff --git a/src/mc/mc_forward.hpp b/src/mc/mc_forward.hpp index dc0e571daa..5972ec1ca9 100644 --- a/src/mc/mc_forward.hpp +++ b/src/mc/mc_forward.hpp @@ -29,8 +29,7 @@ class Frame; class ActorInformation; class Session; -class Checker; - +class Exploration; } } diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 51c4074fed..5a75da01a3 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -8,7 +8,7 @@ #if SIMGRID_HAVE_MC #include "src/mc/Session.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/inspect/mc_unw.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_private.hpp" diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index ff313033b2..dbc8e7cbba 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -12,7 +12,7 @@ #if SIMGRID_HAVE_MC #include "src/mc/api/State.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_private.hpp" #endif diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 68a60f0f27..9750bf5607 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -558,14 +558,14 @@ set(MC_SRC_BASE ) set(MC_SRC - src/mc/checker/Checker.hpp - src/mc/checker/CommunicationDeterminismChecker.cpp - src/mc/checker/SafetyChecker.cpp - src/mc/checker/SafetyChecker.hpp - src/mc/checker/LivenessChecker.cpp - src/mc/checker/LivenessChecker.hpp - src/mc/checker/UdporChecker.cpp - src/mc/checker/UdporChecker.hpp + src/mc/explo/Exploration.hpp + src/mc/explo/CommunicationDeterminismChecker.cpp + src/mc/explo/SafetyChecker.cpp + src/mc/explo/SafetyChecker.hpp + src/mc/explo/LivenessChecker.cpp + src/mc/explo/LivenessChecker.hpp + src/mc/explo/UdporChecker.cpp + src/mc/explo/UdporChecker.hpp src/mc/inspect/DwarfExpression.hpp src/mc/inspect/DwarfExpression.cpp @@ -640,7 +640,7 @@ set(MC_SRC src/mc/udpor_global.hpp ) -set(MC_SIMGRID_MC_SRC src/mc/checker/simgrid_mc.cpp) +set(MC_SIMGRID_MC_SRC src/mc/explo/simgrid_mc.cpp) set(headers_to_install include/simgrid/actor.h