X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/8b0d5ae29ebd13e69a23991b8adfb67c5c5d79d3..1692f2d57cbdd2bfffcba9481b96fb58fec34016:/src/mc/Session.hpp diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index 6806c0c6cb..ab21a05b71 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -21,51 +21,33 @@ namespace mc { * algorithms should be able to be written in high-level languages * (e.g. Python) using bindings on this interface. */ -class Session { +class XBT_PUBLIC Session { private: - std::unique_ptr modelChecker_; - std::shared_ptr initialSnapshot_; - - Session(pid_t pid, int socket); + std::unique_ptr model_checker_; + std::shared_ptr initial_snapshot_; // No copy: Session(Session const&) = delete; Session& operator=(Session const&) = delete; public: - ~Session(); - void close(); - - void initialize(); - void execute(Transition const& transition); - void logState(); - - void restoreInitialState(); - - // static constructors - - /** Create a new session by forking + /** Create a new session by executing the provided code in a fork() * * This sets up the environment for the model-checked process * (environment variables, sockets, etc.). * - * The code is expected to `exec` the model-checker program. + * The code is expected to `exec` the model-checked application. */ - static Session* fork(const std::function& code); + explicit Session(const std::function& code); - /** Spawn a model-checked process - * - * @param path full path of the executable - * @param argv arguments for the model-checked process (NULL-terminated) - */ - static Session* spawnv(const char *path, char *const argv[]); + ~Session(); + void close(); - /** Spawn a model-checked process (using PATH) - * - * @param file file name of the executable (found using `PATH`) - * @param argv arguments for the model-checked process (NULL-terminated) - */ - static Session* spawnvp(const char *file, char *const argv[]); + void initialize(); + void execute(Transition const& transition); + void log_state(); + + void restore_initial_state(); }; // Temporary :)