- xbt_dynar_t incomplete_comm_pattern;
- xbt_dynar_t index_comm; // comm determinism verification
-} s_mc_state_t, *mc_state_t;
-
-XBT_INTERNAL mc_state_t MC_state_new(void);
-XBT_INTERNAL void MC_state_delete(mc_state_t state, int free_snapshot);
-XBT_INTERNAL void MC_state_interleave_process(mc_state_t state, smx_process_t process);
-XBT_INTERNAL unsigned int MC_state_interleave_size(mc_state_t state);
-XBT_INTERNAL int MC_state_process_is_done(mc_state_t state, smx_process_t process);
-XBT_INTERNAL void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
-XBT_INTERNAL smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
-XBT_INTERNAL smx_simcall_t MC_state_get_internal_request(mc_state_t state);
-XBT_INTERNAL smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
-XBT_INTERNAL void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
-
-SG_END_DECL()
+ xbt_dynar_t incomplete_comm_pattern = nullptr;
+
+ // For communication determinism verification:
+ std::vector<unsigned> communicationIndices;
+
+ State();
+ ~State();
+
+ std::size_t interleaveSize() const;
+};
+
+XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
+
+}
+}
+
+XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
+XBT_PRIVATE void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process);
+XBT_PRIVATE void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int value);
+XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value);
+XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state);
+XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
+XBT_PRIVATE void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process);