X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/bd11e68e17f60d1516d80ce8f8c7319542a15ae6..1f7ae620b5e74e6d7b364807ef04b6c869f7d744:/src/mc/ModelChecker.hpp diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 8ef6f807b4..41aa6cbad2 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -1,56 +1,33 @@ -/* Copyright (c) 2007-2015. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2007-2023. 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. */ - + #ifndef SIMGRID_MC_MODEL_CHECKER_HPP #define SIMGRID_MC_MODEL_CHECKER_HPP -#include - -#include -#include +#include "src/mc/remote/CheckerSide.hpp" +#include "src/mc/remote/RemotePtr.hpp" +#include "src/mc/sosp/PageStore.hpp" +#include "xbt/base.h" -#include "mc_forward.h" -#include "mc_process.h" -#include "PageStore.hpp" -#include "mc_protocol.h" +#include -namespace simgrid { -namespace mc { +namespace simgrid::mc { /** State of the model-checker (global variables for the model checker) - * - * Each part of the state of the model chercker represented as a global - * variable prevents some sharing between snapshots and must be ignored. - * By moving as much state as possible in this structure allocated - * on the model-checker heap, we avoid those issues. */ class ModelChecker { - /** String pool for host names */ - // TODO, use std::unordered_set with heterogeneous comparison lookup (C++14) - xbt_dict_t /* */ hostnames_; - // This is the parent snapshot of the current state: - PageStore page_store_; - Process process_; + std::unique_ptr remote_process_memory_; + public: ModelChecker(ModelChecker const&) = delete; ModelChecker& operator=(ModelChecker const&) = delete; - ModelChecker(pid_t pid, int socket); - ~ModelChecker(); - Process& process() - { - return process_; - } - PageStore& page_store() - { - return page_store_; - } - const char* get_host_name(const char* name); + explicit ModelChecker(std::unique_ptr remote_simulation); + + RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; } }; -} -} +} // namespace simgrid::mc #endif