X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ae3dade03692d488ab83a1504a4ff7c1643bce4e..554255fe3f311a54df171d31a4a27f4004840f59:/src/mc/ModelChecker.hpp diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 0647ada5fa..6dead6e0da 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -25,20 +25,20 @@ class ModelChecker { std::set> hostnames_; // This is the parent snapshot of the current state: PageStore page_store_{500}; - std::unique_ptr remote_simulation_; + std::unique_ptr remote_process_; Checker* checker_ = nullptr; + // Expect MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL + std::string simcall_to_string(MessageType type, int aid, int times_considered); + public: ModelChecker(ModelChecker const&) = delete; ModelChecker& operator=(ModelChecker const&) = delete; - explicit ModelChecker(std::unique_ptr remote_simulation, int sockfd); + explicit ModelChecker(std::unique_ptr remote_simulation, int sockfd); - RemoteSimulation& get_remote_simulation() { return *remote_simulation_; } + RemoteProcess& get_remote_process() { return *remote_process_; } Channel& channel() { return checker_side_.get_channel(); } - PageStore& page_store() - { - return page_store_; - } + PageStore& page_store() { return page_store_; } xbt::string const& get_host_name(const char* hostname) { @@ -47,7 +47,7 @@ public: void start(); void shutdown(); - void resume(simgrid::mc::RemoteSimulation& get_remote_simulation); + void resume(); void wait_for_requests(); void handle_simcall(Transition const& transition); @@ -59,6 +59,7 @@ public: XBT_ATTRIB_NORETURN void exit(int status); bool checkDeadlock(); + void finalize_app(); Checker* getChecker() const { return checker_; } void setChecker(Checker* checker) { checker_ = checker; }