+ std::unique_ptr<simgrid::mc::State> initial_state =
+ std::unique_ptr<simgrid::mc::State>(MC_state_new());
+
+ XBT_DEBUG("**************************************************");
+ XBT_DEBUG("Initial state");
+
+ /* Wait for requests (schedules processes) */
+ mc_model_checker->wait_for_requests();
+
+ /* Get an enabled process and insert it in the interleave set of the initial state */
+ for (auto& p : mc_model_checker->process().simix_processes())
+ if (simgrid::mc::process_is_enabled(&p.copy)) {
+ MC_state_interleave_process(initial_state.get(), &p.copy);
+ if (reductionMode_ != simgrid::mc::ReductionMode::none)
+ break;
+ }