void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
XBT_DEBUG("**************************************************");
void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
XBT_DEBUG("**************************************************");
xbt_fifo_shift(mc_stack_liveness_stateless);
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
xbt_fifo_shift(reached_pairs);
xbt_fifo_shift(mc_stack_liveness_stateless);
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
xbt_fifo_shift(reached_pairs);