-
-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;
-
- 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(mc_comm_pattern_t), comm_pattern_free_voidp);
- communications_pattern =
- xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
- incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
- 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();
-
- if (_sg_mc_visited > 0) {
- MC_ignore_heap(simix_global->process_to_run->data, 0);
- MC_ignore_heap(simix_global->process_that_ran->data, 0);
- }
-
- 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;
-
- MC_modelcheck_comm_determinism();
-
-}