- }
-
-
- if(MC_state_interleave_size(current_pair->graph_state) > 0){
- MC_restore_snapshot(current_snapshot);
- MC_UNSET_RAW_MEM;
- }
- }
-
-
- MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_stack_liveness_stateful);
- XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
- MC_UNSET_RAW_MEM;
-
-}
-
-
-
-/********************* Double-DFS stateless *******************/
-
-void MC_pair_stateless_delete(mc_pair_stateless_t pair){
- xbt_free(pair->graph_state->proc_status);
- xbt_free(pair->graph_state);
- //xbt_free(pair->automaton_state); -> FIXME : à implémenter
- xbt_free(pair);
-}
-
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
- mc_pair_stateless_t p = NULL;
- p = xbt_new0(s_mc_pair_stateless_t, 1);
- p->automaton_state = st;
- p->graph_state = sg;
- mc_stats_pair->expanded_pairs++;
- return p;
-}
-
-
-int reached_stateless(mc_reached_pair_stateless_t pair){
-
- char* hash_reached = malloc(sizeof(char)*160);
- unsigned int c= 0;
-
- MC_SET_RAW_MEM;
- char *hash = malloc(sizeof(char)*160);
- xbt_sha((char *)&pair, hash);
- xbt_dynar_foreach(reached_pairs, c, hash_reached){
- if(strcmp(hash, hash_reached) == 0){
- MC_UNSET_RAW_MEM;
- return 1;
- }
- }
-
- MC_UNSET_RAW_MEM;
- return 0;
-}
-
-void set_pair_stateless_reached(mc_pair_stateless_t pair){
-
- mc_reached_pair_stateless_t p = NULL;
- p = xbt_new0(s_mc_reached_pair_stateless_t, 1);
- p->pair = pair;
- p->snapshot_system = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(p->snapshot_system);
-
- if(reached_stateless(p) == 0){
- MC_SET_RAW_MEM;
- char *hash = malloc(sizeof(char)*160) ;
- xbt_sha((char *)&p, hash);
- xbt_dynar_push(reached_pairs, &hash);
- MC_UNSET_RAW_MEM;
- }
-
-}
-