1 /* Copyright (c) 2016. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
7 #ifndef SIMGRID_MC_SESSION_HPP
8 #define SIMGRID_MC_SESSION_HPP
11 #include <sys/prctl.h>
14 #include "xbt/sysdep.h"
15 #include "xbt/system_error.hpp"
16 #include <sys/socket.h>
17 #include <sys/types.h>
23 #include "src/mc/mc_forward.hpp"
24 #include "src/mc/ModelChecker.hpp"
29 /** A model-checking session
31 * This is expected to become the interface used by model-checking
32 * algorithms to control the execution of the model-checked process
33 * and the exploration of the execution graph. Model-checking
34 * algorithms should be able to be written in high-level languages
35 * (e.g. Python) using bindings on this interface.
39 std::unique_ptr<ModelChecker> modelChecker_;
40 std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;
43 Session(pid_t pid, int socket);
46 Session(Session const&) = delete;
47 Session& operator=(Session const&) = delete;
55 void execute(Transition const& transition);
58 void restoreInitialState();
60 public: // static constructors
62 /** Create a new session by forking
64 * This sets up the environment for the model-checked process
65 * (environoment variables, sockets, etc.).
67 * The code is expected to `exec` the model-checker program.
69 static Session* fork(std::function<void()> code);
71 /** Spawn a model-checked process
73 * @param path full path of the executable
74 * @param argv arguments for the model-checked process (NULL-terminated)
76 static Session* spawnv(const char *path, char *const argv[]);
78 /** Spawn a model-checked process (using PATH)
80 * @param file file name of the executable (found using `PATH`)
81 * @param argv arguments for the model-checked process (NULL-terminated)
83 static Session* spawnvp(const char *file, char *const argv[]);
87 extern simgrid::mc::Session* session;