+
+
+/* void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ */
+
+
+/* if(xbt_fifo_size(mc_snapshot_stack) == 0) */
+/* return; */
+
+/* if(restore == 1){ */
+/* MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state); */
+/* MC_UNSET_RAW_MEM; */
+/* } */
+
+
+/* //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); */
+
+/* /\* Get current state *\/ */
+/* mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
+
+/* XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); */
+/* XBT_DEBUG("State : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); */
+
+/* //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); */
+
+/* //sleep(1); */
+
+/* smx_process_t process = NULL; */
+/* int value; */
+/* mc_state_t next_graph_state = NULL; */
+/* smx_req_t req = NULL; */
+/* char *req_str; */
+
+/* mc_pairs_t pair_succ; */
+/* xbt_transition_t transition_succ; */
+/* unsigned int cursor; */
+/* int res; */
+/* //int enabled_transition = 0; */
+
+/* xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); */
+/* xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL); */
+/* xbt_dynar_reset(all_successors); */
+
+/* mc_pairs_t next_pair; */
+/* mc_snapshot_t next_snapshot; */
+/* mc_snapshot_t current_snapshot; */
+
+/* while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ */
+
+/* //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); */
+/* //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); */
+
+/* MC_SET_RAW_MEM; */
+/* current_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
+/* MC_take_snapshot(current_snapshot); */
+/* MC_UNSET_RAW_MEM; */
+
+
+/* /\* Debug information *\/ */
+/* if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){ */
+/* req_str = MC_request_to_string(req, value); */
+/* XBT_DEBUG("Execute: %s", req_str); */
+/* xbt_free(req_str); */
+/* } */
+
+/* MC_state_set_executed_request(current_pair->graph_state, req, value); */
+/* //mc_stats->executed_transitions++; */
+
+/* /\* Answer the request *\/ */
+/* SIMIX_request_pre(req, value); */
+
+/* /\* Wait for requests (schedules processes) *\/ */
+/* MC_wait_for_requests(); */
+
+
+/* /\* Create the new expanded graph_state *\/ */
+/* MC_SET_RAW_MEM; */
+
+/* next_graph_state = MC_state_new(); */
+
+/* /\* Get enabled process and insert it in the interleave set of the next graph_state *\/ */
+/* xbt_swag_foreach(process, simix_global->process_list){ */
+/* if(MC_process_is_enabled(process)){ */
+/* MC_state_interleave_process(next_graph_state, process); */
+/* } */
+/* } */
+
+/* next_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
+/* MC_take_snapshot(next_snapshot); */
+
+/* MC_UNSET_RAW_MEM; */
+
+/* xbt_dynar_reset(elses); */
+/* xbt_dynar_reset(successors); */
+
+/* cursor = 0; */
+/* xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ */
+
+/* res = MC_automaton_evaluate_label(a, transition_succ->label); */
+
+/* MC_SET_RAW_MEM; */
+/* next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); */
+
+/* //XBT_DEBUG("Next pair : %p", next_pair); */
+
+/* if(res == 1){ // enabled transition in automaton */
+/* xbt_dynar_push(successors, &next_pair); */
+/* //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); */
+/* }else{ */
+/* if(res == 2){ */
+/* xbt_dynar_push(elses, &next_pair); */
+/* //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); */
+/* } */
+/* } */
+
+/* MC_UNSET_RAW_MEM; */
+/* } */
+
+
+/* if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ */
+
+/* MC_SET_RAW_MEM; */
+/* next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); */
+/* xbt_dynar_push(successors, &next_pair); */
+/* MC_UNSET_RAW_MEM; */
+
+/* } */
+
+/* //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); */
+/* //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); */
+
+/* if(xbt_dynar_length(successors) > 0){ */
+
+/* cursor = 0; */
+/* xbt_dynar_foreach(successors, cursor, pair_succ){ */
+/* MC_SET_RAW_MEM; */
+/* xbt_dynar_push(all_successors, &pair_succ); */
+/* MC_UNSET_RAW_MEM; */
+/* } */
+
+/* }else{ */
+
+/* cursor = 0; */
+/* xbt_dynar_foreach(elses, cursor, pair_succ){ */
+/* MC_SET_RAW_MEM; */
+/* xbt_dynar_push(all_successors, &pair_succ); */
+/* MC_UNSET_RAW_MEM; */
+/* } */
+
+/* } */
+
+/* MC_restore_snapshot(current_snapshot); */
+/* MC_UNSET_RAW_MEM; */
+
+/* } */
+
+/* //XBT_DEBUG("All successors : %lu", xbt_dynar_length(all_successors)); */
+
+/* cursor = 0; */
+
+/* xbt_dynar_foreach(all_successors, cursor, pair_succ){ */
+
+/* if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ */
+/* XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
+/* XBT_INFO("| ACCEPTANCE CYCLE |"); */
+/* XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
+/* XBT_INFO("Counter-example that violates formula :"); */
+/* MC_show_snapshot_stack(mc_snapshot_stack); */
+/* MC_dump_snapshot_stack(mc_snapshot_stack); */
+/* exit(0); */
+/* } */
+
+/* if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ */
+
+/* //XBT_DEBUG("New pair in stack"); */
+
+/* MC_SET_RAW_MEM; */
+/* xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
+/* MC_UNSET_RAW_MEM; */
+
+/* set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); */
+/* MC_dfs(a, search_cycle, 1); */
+
+/* if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ */
+
+/* set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); */
+/* XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); */
+/* MC_dfs(a, 1, 1); */
+
+/* } */
+/* } */
+
+/* } */
+
+/* MC_SET_RAW_MEM; */
+/* //remove_pair_reached(current_pair->graph_state); */
+/* xbt_fifo_shift(mc_snapshot_stack); */
+/* XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); */
+/* MC_UNSET_RAW_MEM; */
+
+/* } */