- // Create a AF_LOCAL socketpair used for exchanging messages
- // bewteen the model-checker process (ourselves) and the model-checked
- // process:
- int res;
- int sockets[2];
- res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
- if (res == -1)
- throw simgrid::xbt::errno_error(errno, "Could not create socketpair");
-
- pid_t pid = do_fork([&] {
- ::close(sockets[1]);
- setup_child_environment(sockets[0]);
- code();
- xbt_die("The model-checked process failed to exec()");
- });
-
- // Parent (model-checker):
- ::close(sockets[0]);
+ xbt_assert(initial_snapshot_ == nullptr);
+ mc_model_checker->wait_for_requests();
+ initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
+}