X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b61e4656c43c76b402a84cc138032a9f0126d951..ac679d5e69b1eb25e3f82be198607593407e7fc5:/src/mc/ModelChecker.hpp diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 4e3a56505b..f8b0982139 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -3,18 +3,19 @@ /* 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 MC_MODEL_CHECKER_H -#define MC_MODEL_CHECKER_H + +#ifndef SIMGRID_MC_MODEL_CHECKER_HPP +#define SIMGRID_MC_MODEL_CHECKER_HPP #include #include -#include +#include +#include -#include "mc_forward.h" -#include "mc_process.h" -#include "PageStore.hpp" +#include "mc_forward.hpp" +#include "mc/Process.hpp" +#include "mc/PageStore.hpp" #include "mc_protocol.h" namespace simgrid { @@ -28,18 +29,21 @@ namespace mc { * on the model-checker heap, we avoid those issues. */ class ModelChecker { - // This is the parent snapshot of the current state: - s_mc_pages_store_t page_store_; - s_mc_process_t process_; /** 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_; +public: + mc_snapshot_t parent_snapshot_; + public: ModelChecker(ModelChecker const&) = delete; ModelChecker& operator=(ModelChecker const&) = delete; ModelChecker(pid_t pid, int socket); ~ModelChecker(); - s_mc_process_t& process() + Process& process() { return process_; } @@ -48,6 +52,11 @@ public: return page_store_; } const char* get_host_name(const char* name); + + bool is_important_snapshot(Snapshot const& snapshot) const + { + return &snapshot == mc_model_checker->parent_snapshot_; + } }; }