X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d882f311a5e8d59afe8c26d2b5025fa45ab713ae..937854de9dc8e2771ef0891ddc0f39929be1a3d9:/src/mc/ModelChecker.hpp diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index a1138ce0ea..bb733e3e61 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -15,15 +15,14 @@ #include -#include -#include +#include "xbt/base.h" #include -#include "src/mc/mc_forward.hpp" -#include "src/mc/Process.hpp" #include "src/mc/PageStore.hpp" -#include "src/mc/mc_protocol.h" #include "src/mc/Transition.hpp" +#include "src/mc/mc_forward.hpp" +#include "src/mc/remote/RemoteClient.hpp" +#include "src/mc/remote/mc_protocol.h" namespace simgrid { namespace mc { @@ -32,13 +31,14 @@ namespace mc { */ class ModelChecker { struct event_base *base_; - struct event *socket_event_, *signal_event_; + struct event* socket_event_; + struct event* signal_event_; /** String pool for host names */ // TODO, use std::set with heterogeneous comparison lookup (C++14)? std::set hostnames_; // This is the parent snapshot of the current state: PageStore page_store_; - std::unique_ptr process_; + std::unique_ptr process_; Checker* checker_ = nullptr; public: std::shared_ptr parent_snapshot_; @@ -46,13 +46,10 @@ public: public: ModelChecker(ModelChecker const&) = delete; ModelChecker& operator=(ModelChecker const&) = delete; - ModelChecker(std::unique_ptr process); + explicit ModelChecker(std::unique_ptr process); ~ModelChecker(); - Process& process() - { - return *process_; - } + RemoteClient& process() { return *process_; } PageStore& page_store() { return page_store_; @@ -69,15 +66,11 @@ public: void start(); void shutdown(); - void resume(simgrid::mc::Process& process); + void resume(simgrid::mc::RemoteClient& process); void loop(); void handle_events(int fd, short events); - void wait_client(simgrid::mc::Process& process); + void wait_for_requests(); void handle_simcall(Transition const& transition); - void wait_for_requests() - { - mc_model_checker->wait_client(mc_model_checker->process()); - } void exit(int status); bool checkDeadlock();