- //printf("++ current state : %s\n", current_state->id);
-
- xbt_dynar_foreach(current_state->out, cursor, transition_succ){
- successor = transition_succ->dst;
- res = MC_automaton_evaluate_label(a, transition_succ->label);
- //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
- if(res == 1){
- if(search_cycle == 1 && reached_dfs != NULL){
- if(strcmp(reached_dfs->id, successor->id) == 0){
- xbt_dynar_push(state_automaton_visited_dfs, &successor);
- printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
- printf("Visited states : \n");
- unsigned int cursor2 = 0;
- xbt_state_t visited_state = NULL;
- xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
- printf("State : %s\n", visited_state->id);
- }
- exit(1);
- }
- }
- if(successor->visited == 0){
- successor->visited = 1;
- xbt_fifo_unshift(stack_automaton_dfs, successor);
- xbt_dynar_push(state_automaton_visited_dfs, &successor);
- MC_dfs(a, search_cycle);
- if(search_cycle == 0 && successor->type == 1){
- reached_dfs = successor;
- MC_dfs(a, 1);
- }
- }
- }else{
- if(res == 2){
- xbt_dynar_push(elses,&transition_succ);
- }
- }
- }
-
- cursor = 0;
- xbt_dynar_foreach(elses, cursor, transition_succ){
- successor = transition_succ->dst;
- if(search_cycle == 1 && reached_dfs != NULL){
- if(strcmp(reached_dfs->id, successor->id) == 0){
- xbt_dynar_push(state_automaton_visited_dfs, &successor);
- printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
- printf("Visited states : \n");
- unsigned int cursor2 = 0;
- xbt_state_t visited_state = NULL;
- xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
- printf("State : %s\n", visited_state->id);
- }
- exit(1);
- }
- }
- if(successor->visited == 0){
- successor->visited = 1;
- xbt_fifo_unshift(stack_automaton_dfs, successor);
- xbt_dynar_push(state_automaton_visited_dfs, &successor);
- MC_dfs(a, search_cycle);
- if(search_cycle == 0 && successor->type == 1){
- reached_dfs = successor;
- MC_dfs(a, 1);
- }
- }
- }