X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ce2e676ad127f782b9c959499ab1c042195e411a..9692d43fa911bdc2d6d0263a3cb3e22d5e3167fe:/src/mc/ModelChecker.hpp diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index 274ace7d3d..0e7ed9d9f3 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -10,10 +10,12 @@ #include #include + #include +#include +#include #include -#include #include #include @@ -21,6 +23,7 @@ #include "src/mc/Process.hpp" #include "src/mc/PageStore.hpp" #include "src/mc/mc_protocol.h" +#include "src/mc/Transition.hpp" namespace simgrid { namespace mc { @@ -31,7 +34,7 @@ class ModelChecker { struct pollfd fds_[2]; /** String pool for host names */ // TODO, use std::set with heterogeneous comparison lookup (C++14)? - xbt_dict_t /* */ hostnames_; + std::set hostnames_; // This is the parent snapshot of the current state: PageStore page_store_; std::unique_ptr process_; @@ -53,11 +56,14 @@ public: { return page_store_; } - const char* get_host_name(const char* name); - bool is_important_snapshot(Snapshot const& snapshot) const + std::string const& get_host_name(const char* hostname) + { + return *this->hostnames_.insert(hostname).first; + } + std::string const& get_host_name(std::string const& hostname) { - return &snapshot == this->parent_snapshot_.get(); + return *this->hostnames_.insert(hostname).first; } void start(); @@ -66,7 +72,7 @@ public: void loop(); bool handle_events(); void wait_client(simgrid::mc::Process& process); - void simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value); + void handle_simcall(Transition const& transition); void wait_for_requests() { mc_model_checker->wait_client(mc_model_checker->process()); @@ -85,6 +91,9 @@ private: void handle_waitpid(); void on_signal(const struct signalfd_siginfo* info); +public: + unsigned long visited_states = 0; + unsigned long executed_transitions = 0; }; }