- MC_UNSET_RAW_MEM;
- //XBT_DEBUG("End test visited pair");
- return 0;
-
-}
-
-void MC_dfs_init(xbt_automaton_t a){
-
- XBT_DEBUG("**************************************************");
- XBT_DEBUG("DFS init");
- XBT_DEBUG("**************************************************");
-
- mc_pairs_t mc_initial_pair;
- mc_state_t initial_graph_state;
- smx_process_t process;
- mc_snapshot_t init_snapshot;
-
- MC_wait_for_requests();
-
- MC_SET_RAW_MEM;
-
- init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-
- initial_graph_state = MC_state_pair_new();
- xbt_swag_foreach(process, simix_global->process_list){
- if(MC_process_is_enabled(process)){
- MC_state_interleave_process(initial_graph_state, process);
- }
- }
-
- visited_pairs = xbt_dynar_new(sizeof(char *), NULL);
- reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
-
- MC_take_snapshot(init_snapshot);
-
- MC_UNSET_RAW_MEM;
-
- /* unsigned int cursor = 0; */
- /* xbt_state_t state = NULL; */
- /* int nb_init_state = 0; */
-
- /* xbt_dynar_foreach(a->states, cursor, state){ */
- /* if(state->type == -1){ */
-
- /* MC_SET_RAW_MEM; */
- /* mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); */
-
- /* xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); */
-
- /* XBT_DEBUG("**************************************************"); */
- /* XBT_DEBUG("Initial state=%p ", mc_initial_pair); */
-
- /* MC_UNSET_RAW_MEM; */
-
- /* set_pair_visited(mc_initial_pair->graph_state, mc_initial_pair->automaton_state, 0); */
-
- /* if(nb_init_state == 0) */
- /* MC_dfs(a, 0, 0); */
- /* else */
- /* MC_dfs(a, 0, 1); */
-
- /* nb_init_state++; */
- /* } */
- /* } */
-
- /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
- -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
-
- unsigned int cursor = 0;
- unsigned int cursor2 = 0;
- xbt_state_t state = NULL;