From 96d605fde63f72480bf570f7bc7609e2954cb2d7 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 2 Aug 2022 11:15:01 +0200 Subject: [PATCH] Rename mc::Session into mc::api::RemoteApp --- MANIFEST.in | 4 +-- src/mc/ModelChecker.cpp | 4 +-- src/mc/api.cpp | 14 +++++----- src/mc/api.hpp | 6 ++--- src/mc/{Session.cpp => api/RemoteApp.cpp} | 26 +++++++++---------- src/mc/{Session.hpp => api/RemoteApp.hpp} | 16 ++++++------ src/mc/api/State.cpp | 4 +-- src/mc/api/State.hpp | 3 ++- .../explo/CommunicationDeterminismChecker.cpp | 8 +++--- src/mc/explo/DFSExplorer.cpp | 16 ++++++------ src/mc/explo/DFSExplorer.hpp | 2 +- src/mc/explo/Exploration.hpp | 22 +++++++--------- src/mc/explo/LivenessChecker.cpp | 14 +++++----- src/mc/explo/LivenessChecker.hpp | 2 +- src/mc/explo/UdporChecker.cpp | 6 ++--- src/mc/explo/UdporChecker.hpp | 2 +- src/mc/mc_base.cpp | 2 +- src/mc/mc_global.cpp | 2 +- src/mc/transition/TransitionAny.cpp | 2 +- src/mc/transition/TransitionComm.cpp | 2 +- tools/cmake/DefinePackages.cmake | 6 ++--- 21 files changed, 81 insertions(+), 82 deletions(-) rename src/mc/{Session.cpp => api/RemoteApp.cpp} (91%) rename src/mc/{Session.hpp => api/RemoteApp.hpp} (81%) diff --git a/MANIFEST.in b/MANIFEST.in index a1b8d5ad8d..e6cd446730 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2278,13 +2278,13 @@ include src/kernel/timer/Timer.cpp include src/mc/AddressSpace.hpp include src/mc/ModelChecker.cpp include src/mc/ModelChecker.hpp -include src/mc/Session.cpp -include src/mc/Session.hpp include src/mc/VisitedState.cpp include src/mc/VisitedState.hpp include src/mc/api.cpp include src/mc/api.hpp include src/mc/api/ActorState.hpp +include src/mc/api/RemoteApp.cpp +include src/mc/api/RemoteApp.hpp include src/mc/api/State.cpp include src/mc/api/State.hpp include src/mc/compare.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index fe5d743d15..9a22666117 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -141,7 +141,7 @@ static void MC_report_crash(int status) 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->get_exploration()->get_record_trace().to_string().c_str()); - Api::get().get_session().log_state(); + Api::get().get_remote_app().log_state(); if (xbt_log_no_loc) { XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); } else { @@ -233,7 +233,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) for (auto const& s : get_exploration()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str()); - Api::get().get_session().log_state(); + Api::get().get_remote_app().log_state(); this->exit(SIMGRID_MC_EXIT_SAFETY); diff --git a/src/mc/api.cpp b/src/mc/api.cpp index f854af4da5..c57dd6921a 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -8,7 +8,7 @@ #include "src/kernel/activity/MailboxImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/actor/SimcallObserver.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_base.hpp" #include "src/mc/mc_exit.hpp" @@ -32,7 +32,7 @@ namespace simgrid::mc { simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map& env, simgrid::mc::ExplorationAlgorithm algo) { - session_ = std::make_unique([argv, &env] { + remote_app_ = std::make_unique([argv, &env] { int i = 1; while (argv[i] != nullptr && argv[i][0] == '-') i++; @@ -50,19 +50,19 @@ simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map< simgrid::mc::Exploration* explo; switch (algo) { case ExplorationAlgorithm::CommDeterminism: - explo = simgrid::mc::create_communication_determinism_checker(session_.get()); + explo = simgrid::mc::create_communication_determinism_checker(remote_app_.get()); break; case ExplorationAlgorithm::UDPOR: - explo = simgrid::mc::create_udpor_checker(session_.get()); + explo = simgrid::mc::create_udpor_checker(remote_app_.get()); break; case ExplorationAlgorithm::Safety: - explo = simgrid::mc::create_dfs_exploration(session_.get()); + explo = simgrid::mc::create_dfs_exploration(remote_app_.get()); break; case ExplorationAlgorithm::Liveness: - explo = simgrid::mc::create_liveness_checker(session_.get()); + explo = simgrid::mc::create_liveness_checker(remote_app_.get()); break; default: @@ -118,7 +118,7 @@ simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const void Api::s_close() { - session_.reset(); + remote_app_.reset(); if (simgrid::mc::property_automaton != nullptr) { xbt_automaton_free(simgrid::mc::property_automaton); simgrid::mc::property_automaton = nullptr; diff --git a/src/mc/api.hpp b/src/mc/api.hpp index 2a9d2500ce..98baee7252 100644 --- a/src/mc/api.hpp +++ b/src/mc/api.hpp @@ -10,7 +10,7 @@ #include #include "simgrid/forward.h" -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/api/State.hpp" #include "src/mc/mc_forward.hpp" #include "src/mc/mc_record.hpp" @@ -40,7 +40,7 @@ private: } }; - std::unique_ptr session_; + std::unique_ptr remote_app_; public: // No copy: @@ -75,7 +75,7 @@ public: simgrid::mc::Snapshot* take_snapshot(long num_state) const; // SESSION APIs - simgrid::mc::Session const& get_session() const { return *session_; } + simgrid::mc::RemoteApp const& get_remote_app() const { return *remote_app_; } void s_close(); // AUTOMATION APIs diff --git a/src/mc/Session.cpp b/src/mc/api/RemoteApp.cpp similarity index 91% rename from src/mc/Session.cpp rename to src/mc/api/RemoteApp.cpp index 3f19003dca..6037b6a1ec 100644 --- a/src/mc/Session.cpp +++ b/src/mc/api/RemoteApp.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/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/internal_config.h" // HAVE_SMPI #include "src/mc/explo/Exploration.hpp" #include "src/mc/mc_config.hpp" @@ -41,7 +41,7 @@ template void run_child_process(int socket, Code code) #ifdef __linux__ // Make sure we do not outlive our parent sigset_t mask; - sigemptyset (&mask); + sigemptyset(&mask); xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals"); xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG"); #endif @@ -56,10 +56,10 @@ template void run_child_process(int socket, Code code) code(); } -Session::Session(const std::function& code) +RemoteApp::RemoteApp(const std::function& code) { #if HAVE_SMPI - smpi_init_options();//only performed once + smpi_init_options(); // only performed once xbt_assert(smpi_cfg_privatization() != SmpiPrivStrategies::MMAP, "Please use the dlopen privatization schema when model-checking SMPI code"); #endif @@ -91,25 +91,25 @@ Session::Session(const std::function& code) model_checker_->start(); } -Session::~Session() +RemoteApp::~RemoteApp() { this->close(); } /** The application must be stopped. */ -void Session::take_initial_snapshot() +void RemoteApp::take_initial_snapshot() { xbt_assert(initial_snapshot_ == nullptr); model_checker_->wait_for_requests(); initial_snapshot_ = std::make_shared(0); } -void Session::restore_initial_state() const +void RemoteApp::restore_initial_state() const { this->initial_snapshot_->restore(&model_checker_->get_remote_process()); } -void Session::log_state() const +void RemoteApp::log_state() const { model_checker_->get_exploration()->log_state(); @@ -117,14 +117,14 @@ void Session::log_state() const fprintf(dot_output, "}\n"); fclose(dot_output); } - if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){ - int ret=system("free"); + if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) { + int ret = system("free"); if (ret != 0) XBT_WARN("Call to system(free) did not return 0, but %d", ret); } } -void Session::close() +void RemoteApp::close() { initial_snapshot_ = nullptr; if (model_checker_) { @@ -134,7 +134,7 @@ void Session::close() } } -void Session::get_actors_status(std::map& whereto) +void RemoteApp::get_actors_status(std::map& whereto) { s_mc_message_t msg; memset(&msg, 0, sizeof msg); @@ -159,7 +159,7 @@ void Session::get_actors_status(std::map& whereto) whereto.insert(std::make_pair(actor.aid, ActorState(actor.aid, actor.enabled, actor.max_considered))); } -void Session::check_deadlock() const +void RemoteApp::check_deadlock() const { xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state"); s_mc_message_int_t message; diff --git a/src/mc/Session.hpp b/src/mc/api/RemoteApp.hpp similarity index 81% rename from src/mc/Session.hpp rename to src/mc/api/RemoteApp.hpp index 16294c87c4..a9a9ea37f3 100644 --- a/src/mc/Session.hpp +++ b/src/mc/api/RemoteApp.hpp @@ -3,8 +3,8 @@ /* 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. */ -#ifndef SIMGRID_MC_SESSION_HPP -#define SIMGRID_MC_SESSION_HPP +#ifndef SIMGRID_MC_REMOTE_APP_HPP +#define SIMGRID_MC_REMOTE_APP_HPP #include "simgrid/forward.h" #include "src/mc/ModelChecker.hpp" @@ -15,7 +15,7 @@ namespace simgrid::mc { -/** A model-checking session +/** High-level view of the verified application, from the model-checker POV * * This is expected to become the interface used by model-checking * algorithms to control the execution of the model-checked process @@ -23,14 +23,14 @@ namespace simgrid::mc { * algorithms should be able to be written in high-level languages * (e.g. Python) using bindings on this interface. */ -class XBT_PUBLIC Session { +class XBT_PUBLIC RemoteApp { private: std::unique_ptr model_checker_; std::shared_ptr initial_snapshot_; // No copy: - Session(Session const&) = delete; - Session& operator=(Session const&) = delete; + RemoteApp(RemoteApp const&) = delete; + RemoteApp& operator=(RemoteApp const&) = delete; public: /** Create a new session by executing the provided code in a fork() @@ -40,9 +40,9 @@ public: * * The code is expected to `exec` the model-checked application. */ - explicit Session(const std::function& code); + explicit RemoteApp(const std::function& code); - ~Session(); + ~RemoteApp(); void close(); void take_initial_snapshot(); diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 1ba81a2754..7467b6aa5a 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -15,9 +15,9 @@ namespace simgrid::mc { long State::expended_states_ = 0; -State::State(Session& session) : num_(++expended_states_) +State::State(RemoteApp& remote_app) : num_(++expended_states_) { - session.get_actors_status(actors_to_run_); + remote_app.get_actors_status(actors_to_run_); transition_.reset(new Transition()); /* Stateful model checking */ diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index ddca326a70..01d013550e 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -7,6 +7,7 @@ #define SIMGRID_MC_STATE_HPP #include "src/mc/api/ActorState.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/sosp/Snapshot.hpp" #include "src/mc/transition/Transition.hpp" @@ -29,7 +30,7 @@ class XBT_PRIVATE State : public xbt::Extendable { std::shared_ptr system_state_; public: - explicit State(Session& session); + explicit State(RemoteApp& remote_app); /* Returns a positive number if there is another transition to pick, or -1 if not */ aid_t next_transition() const; diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 4464631415..3212daacbc 100644 --- a/src/mc/explo/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -202,7 +202,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC XBT_INFO("***** Non-send-deterministic communications pattern *****"); XBT_INFO("*********************************************************"); XBT_INFO("%s", send_diff.c_str()); - Api::get().get_session().log_state(); + Api::get().get_remote_app().log_state(); Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) { XBT_INFO("****************************************************"); @@ -212,7 +212,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC XBT_INFO("%s", send_diff.c_str()); if (not recv_diff.empty()) XBT_INFO("%s", recv_diff.c_str()); - Api::get().get_session().log_state(); + Api::get().get_remote_app().log_state(); Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } @@ -314,7 +314,7 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) } */ -Exploration* create_communication_determinism_checker(Session* session) +Exploration* create_communication_determinism_checker(RemoteApp* remote_app) { CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create(); StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create(); @@ -366,7 +366,7 @@ Exploration* create_communication_determinism_checker(Session* session) delete extension; }); - return new DFSExplorer(session); + return new DFSExplorer(remote_app); } } // namespace simgrid::mc diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index d7e0f1e7a9..1d429a2f24 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -148,7 +148,7 @@ void DFSExplorer::run() state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo()); /* Create the new expanded state (copy the state of MCed into our MCer data) */ - auto next_state = std::make_unique(get_session()); + auto next_state = std::make_unique(get_remote_app()); on_state_creation_signal(next_state.get()); if (_sg_mc_termination) @@ -191,7 +191,7 @@ void DFSExplorer::backtrack() on_backtracking_signal(); stack_.pop_back(); - get_session().check_deadlock(); + get_remote_app().check_deadlock(); /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that * have it empty in the way. For each deleted state, check if the request that has generated it (from its @@ -252,7 +252,7 @@ void DFSExplorer::restore_state() } /* if no snapshot, we need to restore the initial state and replay the transitions */ - get_session().restore_initial_state(); + get_remote_app().restore_initial_state(); on_restore_initial_state_signal(); /* Traverse the stack from the state at position start and re-execute the transitions */ @@ -266,7 +266,7 @@ void DFSExplorer::restore_state() } } -DFSExplorer::DFSExplorer(Session* session) : Exploration(session) +DFSExplorer::DFSExplorer(RemoteApp* remote_app) : Exploration(remote_app) { reductionMode_ = reduction_mode; if (_sg_mc_termination) @@ -281,11 +281,11 @@ DFSExplorer::DFSExplorer(Session* session) : Exploration(session) (reductionMode_ == ReductionMode::none ? "none" : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown"))); - get_session().take_initial_snapshot(); + get_remote_app().take_initial_snapshot(); XBT_DEBUG("Starting the DFS exploration"); - auto initial_state = std::make_unique(get_session()); + auto initial_state = std::make_unique(get_remote_app()); XBT_DEBUG("**************************************************"); @@ -305,9 +305,9 @@ DFSExplorer::DFSExplorer(Session* session) : Exploration(session) stack_.push_back(std::move(initial_state)); } -Exploration* create_dfs_exploration(Session* session) +Exploration* create_dfs_exploration(RemoteApp* remote_app) { - return new DFSExplorer(session); + return new DFSExplorer(remote_app); } } // namespace simgrid::mc diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 8c59356b9b..ce5fa545e1 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -34,7 +34,7 @@ class XBT_PRIVATE DFSExplorer : public Exploration { static xbt::signal on_log_state_signal; public: - explicit DFSExplorer(Session* session); + explicit DFSExplorer(RemoteApp* remote_app); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index 5b995f7ded..5b27bffbe5 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -1,5 +1,4 @@ -/* Copyright (c) 2016-2022. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2016-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. */ @@ -20,15 +19,14 @@ namespace simgrid::mc { * you might be able to write your model-checking algorithm as plain * imperative code instead. * - * It is expected to interact with the model-checking core through the - * `Session` interface (but currently the `Session` interface does not - * have all the necessary features). */ + * It is expected to interact with the model-checked application through the + * `RemoteApp` interface (that is currently not perfectly sufficient to that extend). */ // abstract class Exploration : public xbt::Extendable { - Session* session_; + RemoteApp* remote_app_; public: - explicit Exploration(Session* session) : session_(session) {} + explicit Exploration(RemoteApp* remote_app) : remote_app_(remote_app) {} // No copy: Exploration(Exploration const&) = delete; @@ -54,14 +52,14 @@ public: /** Log additional information about the state of the model-checker */ virtual void log_state() = 0; - Session& get_session() { return *session_; } + RemoteApp& get_remote_app() { return *remote_app_; } }; // External constructors so that the types (and the types of their content) remain hidden -XBT_PUBLIC Exploration* create_liveness_checker(Session* session); -XBT_PUBLIC Exploration* create_dfs_exploration(Session* session); -XBT_PUBLIC Exploration* create_communication_determinism_checker(Session* session); -XBT_PUBLIC Exploration* create_udpor_checker(Session* session); +XBT_PUBLIC Exploration* create_liveness_checker(RemoteApp* remote_app); +XBT_PUBLIC Exploration* create_dfs_exploration(RemoteApp* remote_app); +XBT_PUBLIC Exploration* create_communication_determinism_checker(RemoteApp* remote_app); +XBT_PUBLIC Exploration* create_udpor_checker(RemoteApp* remote_app); } // namespace simgrid::mc diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index bcaabb3ada..3acd33a319 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -4,7 +4,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "src/mc/explo/LivenessChecker.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" @@ -106,7 +106,7 @@ void LivenessChecker::replay() } } - get_session().restore_initial_state(); + get_remote_app().restore_initial_state(); /* Traverse the stack from the initial state and re-execute the transitions */ int depth = 1; @@ -178,7 +178,7 @@ void LivenessChecker::purge_visited_pairs() } } -LivenessChecker::LivenessChecker(Session* session) : Exploration(session) {} +LivenessChecker::LivenessChecker(RemoteApp* remote_app) : Exploration(remote_app) {} RecordTrace LivenessChecker::get_record_trace() // override { @@ -223,7 +223,7 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt ++expanded_pairs_count_; auto next_pair = std::make_shared(expanded_pairs_count_); next_pair->prop_state_ = state; - next_pair->app_state_ = std::make_shared(get_session()); + next_pair->app_state_ = std::make_shared(get_remote_app()); next_pair->atomic_propositions = std::move(propositions); if (current_pair) next_pair->depth = current_pair->depth + 1; @@ -271,7 +271,7 @@ void LivenessChecker::run() Api::get().automaton_load(_sg_mc_property_file.get().c_str()); XBT_DEBUG("Starting the liveness algorithm"); - get_session().take_initial_snapshot(); + get_remote_app().take_initial_snapshot(); /* Initialize */ this->previous_pair_ = 0; @@ -367,9 +367,9 @@ void LivenessChecker::run() log_state(); } -Exploration* create_liveness_checker(Session* session) +Exploration* create_liveness_checker(RemoteApp* remote_app) { - return new LivenessChecker(session); + return new LivenessChecker(remote_app); } } // namespace simgrid::mc diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp index 09e8a6041e..f47c4ec44c 100644 --- a/src/mc/explo/LivenessChecker.hpp +++ b/src/mc/explo/LivenessChecker.hpp @@ -50,7 +50,7 @@ public: class XBT_PRIVATE LivenessChecker : public Exploration { public: - explicit LivenessChecker(Session* session); + explicit LivenessChecker(RemoteApp* remote_app); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 7f43c4e678..b935dcccaa 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -10,7 +10,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety ver namespace simgrid::mc { -UdporChecker::UdporChecker(Session* session) : Exploration(session) {} +UdporChecker::UdporChecker(RemoteApp* remote_app) : Exploration(remote_app) {} void UdporChecker::run() {} @@ -28,9 +28,9 @@ std::vector UdporChecker::get_textual_trace() void UdporChecker::log_state() {} -Exploration* create_udpor_checker(Session* session) +Exploration* create_udpor_checker(RemoteApp* remote_app) { - return new UdporChecker(session); + return new UdporChecker(remote_app); } } // namespace simgrid::mc diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 168a14a58c..e5e1097c25 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -14,7 +14,7 @@ namespace simgrid::mc { class XBT_PRIVATE UdporChecker : public Exploration { public: - explicit UdporChecker(Session* session); + explicit UdporChecker(RemoteApp* remote_app); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index a35833c032..91012ba602 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -16,7 +16,7 @@ #if SIMGRID_HAVE_MC #include "src/mc/ModelChecker.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/remote/RemoteProcess.hpp" #endif diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index ef212045bf..dacf7e423a 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -7,7 +7,7 @@ #include "src/kernel/actor/ActorImpl.hpp" #if SIMGRID_HAVE_MC -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/explo/Exploration.hpp" #include "src/mc/inspect/mc_unw.hpp" #include "src/mc/mc_config.hpp" diff --git a/src/mc/transition/TransitionAny.cpp b/src/mc/transition/TransitionAny.cpp index d590c5f5a1..9de469b684 100644 --- a/src/mc/transition/TransitionAny.cpp +++ b/src/mc/transition/TransitionAny.cpp @@ -8,7 +8,7 @@ #include #if SIMGRID_HAVE_MC #include "src/mc/ModelChecker.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/api/State.hpp" #endif diff --git a/src/mc/transition/TransitionComm.cpp b/src/mc/transition/TransitionComm.cpp index 916dd8ba85..0d48bcf7db 100644 --- a/src/mc/transition/TransitionComm.cpp +++ b/src/mc/transition/TransitionComm.cpp @@ -8,7 +8,7 @@ #include #if SIMGRID_HAVE_MC #include "src/mc/ModelChecker.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/api/RemoteApp.hpp" #include "src/mc/api/State.hpp" #endif diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 5be7c8a2a7..9596c7e492 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -634,15 +634,15 @@ set(MC_SRC src/mc/AddressSpace.hpp src/mc/ModelChecker.cpp src/mc/ModelChecker.hpp - src/mc/Session.cpp - src/mc/Session.hpp src/mc/VisitedState.cpp src/mc/VisitedState.hpp src/mc/api.cpp src/mc/api.hpp + src/mc/api/ActorState.hpp src/mc/api/State.cpp src/mc/api/State.hpp - src/mc/api/ActorState.hpp + src/mc/api/RemoteApp.cpp + src/mc/api/RemoteApp.hpp src/mc/compare.cpp src/mc/mc_client_api.cpp src/mc/mc_exit.hpp -- 2.20.1