+ 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;
+ }
+ }
+