- while((current_pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
- req = MC_state_get_internal_request(current_pair->graph_state);
- xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pairs_t) {
- if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
- if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
- XBT_DEBUG("Dependent Transitions:");
- prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
- req_str = MC_request_to_string(prev_req, value);
- XBT_DEBUG("%s (state=%p)", req_str, prev_pair->graph_state);
- xbt_free(req_str);
- prev_req = MC_state_get_executed_request(current_pair->graph_state, &value);
- req_str = MC_request_to_string(prev_req, value);
- XBT_DEBUG("%s (state=%p)", req_str, current_pair->graph_state);
- xbt_free(req_str);
- }
-
- if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
- MC_state_interleave_process(prev_pair->graph_state, req->issuer);
-
- } else {
- XBT_DEBUG("Process %p is in done set", req->issuer);
- }
-
- break;
- }
- }
-
- if(MC_state_interleave_size(current_pair->graph_state)){
- MC_restore_snapshot(current_pair->system_state);
- xbt_fifo_unshift(mc_snapshot_stack, current_pair);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
+ MC_ddfs_stateless(a, search_cycle, 0);
+
+
+ if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+
+ XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+ int res = set_pair_reached(a);
+
+ MC_SET_RAW_MEM;
+ xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+ MC_UNSET_RAW_MEM;
+
+ MC_ddfs_stateless(a, 1, 1);
+
+ if(res){
+ MC_SET_RAW_MEM;
+ xbt_dynar_pop(reached_pairs, NULL);