+ if ((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth)
+ || user_max_depth_reached || visited_state != -1) {
+
+ if (user_max_depth_reached && visited_state == -1)
+ XBT_DEBUG("User max depth reached !");
+ else if (visited_state == -1)
+ XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+
+ if (mc_reduce_kind == e_mc_reduce_dpor) {
+ /* Interleave enabled processes in the state in which they have been enabled for the first time */
+ xbt_swag_foreach(process, simix_global->process_list) {
+ if (MC_process_is_enabled(process)) {
+ char *key = bprintf("%lu", process->pid);
+ enabled =
+ (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
+ 0, 10);
+ xbt_free(key);
+ int cursor = xbt_fifo_size(mc_stack_safety);
+ xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t) {
+ if (cursor-- == enabled) {
+ if (!MC_state_process_is_done(state_test, process)
+ && state_test->num != state->num) {
+ XBT_DEBUG("Interleave process %lu in state %d",
+ process->pid, state_test->num);
+ MC_state_interleave_process(state_test, process);
+ break;
+ }
+ }
+ }
+ }
+ }
+ }
+
+ } else {
+
+ XBT_DEBUG("There are no more processes to interleave. (depth %d)",
+ xbt_fifo_size(mc_stack_safety) + 1);
+
+ }
+
+ MC_SET_MC_HEAP;
+
+ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
+ if (initial_state_safety->initial_communications_pattern_done) {
+ if (visited_state == -1) {
+ deterministic_pattern(initial_communications_pattern,
+ communications_pattern);
+ if (initial_state_safety->comm_deterministic == 0
+ && _sg_mc_comms_determinism) {
+ XBT_INFO("****************************************************");
+ XBT_INFO("***** Non-deterministic communications pattern *****");
+ XBT_INFO("****************************************************");
+ XBT_INFO("Initial communications pattern:");
+ print_communications_pattern(initial_communications_pattern);
+ XBT_INFO("Communications pattern counter-example:");
+ print_communications_pattern(communications_pattern);
+ MC_print_statistics(mc_stats);
+ return;
+ } else if (initial_state_safety->send_deterministic == 0
+ && _sg_mc_send_determinism) {
+ XBT_INFO
+ ("*********************************************************");
+ XBT_INFO
+ ("***** Non-send-deterministic communications pattern *****");
+ XBT_INFO
+ ("*********************************************************");
+ XBT_INFO("Initial communications pattern:");
+ print_communications_pattern(initial_communications_pattern);
+ XBT_INFO("Communications pattern counter-example:");
+ print_communications_pattern(communications_pattern);
+ MC_print_statistics(mc_stats);
+ return;
+ }
+ } else {
+
+ }
+ } else {
+ initial_state_safety->initial_communications_pattern_done = 1;
+ }
+ }