+void MC_pre_modelcheck_comm_determinism(void)
+{
+
+ int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
+
+ mc_state_t initial_state = NULL;
+ smx_process_t process;
+ int i;
+
+ if (!mc_mem_set)
+ MC_SET_MC_HEAP;
+
+ if (_sg_mc_visited > 0)
+ visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
+
+ initial_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+ for (i=0; i<simix_process_maxpid; i++){
+ xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+ xbt_dynar_insert_at(initial_communications_pattern, i, &process_pattern);
+ }
+ communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+ for (i=0; i<simix_process_maxpid; i++){
+ xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
+ xbt_dynar_insert_at(communications_pattern, i, &process_pattern);
+ }
+ incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
+ for (i=0; i<simix_process_maxpid; i++){
+ xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(int), NULL);
+ xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
+ }
+
+ nb_comm_pattern = 0;
+
+ initial_state = MC_state_new();
+
+ MC_SET_STD_HEAP;
+
+ XBT_DEBUG("********* Start communication determinism verification *********");
+
+ /* Wait for requests (schedules processes) */
+ MC_wait_for_requests();
+
+ MC_SET_MC_HEAP;
+
+ /* Get an enabled process and insert it in the interleave set of the initial state */
+ xbt_swag_foreach(process, simix_global->process_list) {
+ if (MC_process_is_enabled(process)) {
+ MC_state_interleave_process(initial_state, process);
+ }
+ }
+
+ xbt_fifo_unshift(mc_stack, initial_state);
+
+ MC_SET_STD_HEAP;
+
+}
+
+void MC_modelcheck_comm_determinism(void)