void MC_show_deadlock(smx_simcall_t req);
void MC_show_stack_safety(xbt_fifo_t stack);
void MC_dump_stack_safety(xbt_fifo_t stack);
void MC_show_deadlock(smx_simcall_t req);
void MC_show_stack_safety(xbt_fifo_t stack);
void MC_dump_stack_safety(xbt_fifo_t stack);
/* Possible exploration status of a process in a state */
typedef enum {
MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */
/* Possible exploration status of a process in a state */
typedef enum {
MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */
int other_num; // dot_output for
}s_mc_visited_state_t, *mc_visited_state_t;
int other_num; // dot_output for
}s_mc_visited_state_t, *mc_visited_state_t;
mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
void MC_visited_pair_delete(mc_visited_pair_t p);
mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
void MC_visited_pair_delete(mc_visited_pair_t p);
void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
void MC_post_process_types(mc_object_info_t info);
void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
void MC_post_process_types(mc_object_info_t info);
}s_mc_comm_pattern_t, *mc_comm_pattern_t;
extern xbt_dynar_t communications_pattern;
extern xbt_dynar_t incomplete_communications_pattern;
void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
}s_mc_comm_pattern_t, *mc_comm_pattern_t;
extern xbt_dynar_t communications_pattern;
extern xbt_dynar_t incomplete_communications_pattern;
void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);