1 /* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "mc_private.h"
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
11 "Logging specific to algorithms for liveness properties verification");
13 /********* Global variables *********/
15 xbt_dynar_t acceptance_pairs;
16 xbt_dynar_t visited_pairs;
17 xbt_dynar_t successors;
20 /********* Static functions *********/
22 static mc_acceptance_pair_t acceptance_pair_new(int num, xbt_automaton_state_t as){
24 mc_acceptance_pair_t new_pair = NULL;
25 new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
27 new_pair->automaton_state = as;
28 new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
29 new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
30 new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
31 new_pair->system_state = MC_take_snapshot();
33 /* Get values of propositional symbols */
36 unsigned int cursor = 0;
37 xbt_automaton_propositional_symbol_t ps = NULL;
38 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
39 f = (int_f_void_t)ps->function;
41 xbt_dynar_push_as(new_pair->prop_ato, int, res);
48 static int is_reached_acceptance_pair(int num, xbt_automaton_state_t as){
50 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
53 mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);
56 if(xbt_dynar_is_empty(acceptance_pairs)){
59 xbt_dynar_push(acceptance_pairs, &new_pair);
71 size_t current_bytes_used = new_pair->heap_bytes_used;
72 int current_nb_processes = new_pair->nb_processes;
74 unsigned int cursor = 0;
75 int previous_cursor = 0, next_cursor = 0;
77 int end = xbt_dynar_length(acceptance_pairs) - 1;
79 mc_acceptance_pair_t pair_test = NULL;
80 size_t bytes_used_test;
81 int nb_processes_test;
82 int same_processes_and_bytes_not_found = 1;
84 while(start <= end && same_processes_and_bytes_not_found){
85 cursor = (start + end) / 2;
86 pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
87 bytes_used_test = pair_test->heap_bytes_used;
88 nb_processes_test = pair_test->nb_processes;
89 if(nb_processes_test < current_nb_processes)
91 if(nb_processes_test > current_nb_processes)
93 if(nb_processes_test == current_nb_processes){
94 if(bytes_used_test < current_bytes_used)
96 if(bytes_used_test > current_bytes_used)
98 if(bytes_used_test == current_bytes_used){
99 same_processes_and_bytes_not_found = 0;
100 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
101 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
102 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
107 return pair_test->num;
111 /* Search another pair with same number of bytes used in std_heap */
112 previous_cursor = cursor - 1;
113 while(previous_cursor >= 0){
114 pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_acceptance_pair_t);
115 bytes_used_test = pair_test->system_state->heap_bytes_used;
116 if(bytes_used_test != current_bytes_used)
118 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
119 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
120 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
125 return pair_test->num;
131 next_cursor = cursor + 1;
132 while(next_cursor < xbt_dynar_length(acceptance_pairs)){
133 pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_acceptance_pair_t);
134 bytes_used_test = pair_test->system_state->heap_bytes_used;
135 if(bytes_used_test != current_bytes_used)
137 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
138 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
139 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
144 return pair_test->num;
154 pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
155 bytes_used_test = pair_test->heap_bytes_used;
157 if(bytes_used_test < current_bytes_used)
158 xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair);
160 xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair);
174 static void set_acceptance_pair_reached(int num, xbt_automaton_state_t as){
176 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
179 mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);
182 if(xbt_dynar_is_empty(acceptance_pairs)){
185 xbt_dynar_push(acceptance_pairs, &new_pair);
192 size_t current_bytes_used = new_pair->heap_bytes_used;
193 int current_nb_processes = new_pair->nb_processes;
195 unsigned int cursor = 0;
197 int end = xbt_dynar_length(acceptance_pairs) - 1;
199 mc_acceptance_pair_t pair_test = NULL;
200 size_t bytes_used_test = 0;
201 int nb_processes_test;
204 cursor = (start + end) / 2;
205 pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
206 bytes_used_test = pair_test->heap_bytes_used;
207 nb_processes_test = pair_test->nb_processes;
208 if(nb_processes_test < current_nb_processes)
210 if(nb_processes_test > current_nb_processes)
212 if(nb_processes_test == current_nb_processes){
213 if(bytes_used_test < current_bytes_used)
215 if(bytes_used_test > current_bytes_used)
217 if(bytes_used_test == current_bytes_used)
222 if(bytes_used_test < current_bytes_used)
223 xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair);
225 xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair);
236 static void remove_acceptance_pair(int num_pair){
238 unsigned int cursor = 0;
239 mc_acceptance_pair_t current_pair;
241 xbt_dynar_foreach(acceptance_pairs, cursor, current_pair){
242 if(current_pair->num == num_pair)
246 xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
250 static mc_visited_pair_t visited_pair_new(int num, xbt_automaton_state_t as){
252 mc_visited_pair_t new_pair = NULL;
253 new_pair = xbt_new0(s_mc_visited_pair_t, 1);
254 new_pair->automaton_state = as;
256 new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
257 new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
258 new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
259 new_pair->system_state = MC_take_snapshot();
261 /* Get values of propositional symbols */
264 unsigned int cursor = 0;
265 xbt_automaton_propositional_symbol_t ps = NULL;
266 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
267 f = (int_f_void_t)ps->function;
269 xbt_dynar_push_as(new_pair->prop_ato, int, res);
276 static int is_visited_pair(int num, xbt_automaton_state_t as){
278 if(_sg_mc_visited == 0)
281 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
284 mc_visited_pair_t new_pair = visited_pair_new(num, as);
287 if(xbt_dynar_is_empty(visited_pairs)){
290 xbt_dynar_push(visited_pairs, &new_pair);
302 size_t current_bytes_used = new_pair->heap_bytes_used;
303 int current_nb_processes = new_pair->nb_processes;
305 unsigned int cursor = 0;
306 int previous_cursor = 0, next_cursor = 0;
308 int end = xbt_dynar_length(visited_pairs) - 1;
310 mc_visited_pair_t pair_test = NULL;
311 size_t bytes_used_test;
312 int nb_processes_test;
313 int same_processes_and_bytes_not_found = 1;
315 while(start <= end && same_processes_and_bytes_not_found){
316 cursor = (start + end) / 2;
317 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
318 bytes_used_test = pair_test->heap_bytes_used;
319 nb_processes_test = pair_test->nb_processes;
320 if(nb_processes_test < current_nb_processes)
322 if(nb_processes_test > current_nb_processes)
324 if(nb_processes_test == current_nb_processes){
325 if(bytes_used_test < current_bytes_used)
327 if(bytes_used_test > current_bytes_used)
329 if(bytes_used_test == current_bytes_used){
330 same_processes_and_bytes_not_found = 0;
331 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
332 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
333 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
334 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
335 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
336 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
341 return pair_test->num;
345 /* Search another pair with same number of bytes used in std_heap */
346 previous_cursor = cursor - 1;
347 while(previous_cursor >= 0){
348 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_visited_pair_t);
349 bytes_used_test = pair_test->system_state->heap_bytes_used;
350 if(bytes_used_test != current_bytes_used)
352 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
353 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
354 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
355 xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
356 xbt_dynar_insert_at(visited_pairs, previous_cursor, &new_pair);
357 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
362 return pair_test->num;
368 next_cursor = cursor + 1;
369 while(next_cursor < xbt_dynar_length(visited_pairs)){
370 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_visited_pair_t);
371 bytes_used_test = pair_test->system_state->heap_bytes_used;
372 if(bytes_used_test != current_bytes_used)
374 if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
375 if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
376 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
377 xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
378 xbt_dynar_insert_at(visited_pairs, next_cursor, &new_pair);
379 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
384 return pair_test->num;
394 pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
395 bytes_used_test = pair_test->heap_bytes_used;
397 if(bytes_used_test < current_bytes_used)
398 xbt_dynar_insert_at(visited_pairs, cursor + 1, &new_pair);
400 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
402 if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
403 int min = mc_stats->expanded_states;
404 unsigned int cursor2 = 0;
405 unsigned int index = 0;
406 xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
407 if(pair_test->num < min){
409 min = pair_test->num;
412 xbt_dynar_remove_at(visited_pairs, index, NULL);
416 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
417 fprintf(stderr, "Visited pair %d, nb_processes %d and heap_bytes_used %zu\n", pair_test->num, pair_test->nb_processes, pair_test->heap_bytes_used);
431 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
435 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
436 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
437 return (left_res || right_res);
440 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
441 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
442 return (left_res && right_res);
445 int res = MC_automaton_evaluate_label(l->u.exp_not);
449 unsigned int cursor = 0;
450 xbt_automaton_propositional_symbol_t p = NULL;
452 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
453 if(strcmp(p->pred, l->u.predicat) == 0){
454 f = (int_f_void_t)p->function;
469 /********* Free functions *********/
471 static void visited_pair_free(mc_visited_pair_t pair){
473 xbt_dynar_free(&(pair->prop_ato));
474 MC_free_snapshot(pair->system_state);
479 static void visited_pair_free_voidp(void *p){
480 visited_pair_free((mc_visited_pair_t) * (void **) p);
483 static void acceptance_pair_free(mc_acceptance_pair_t pair){
485 xbt_dynar_free(&(pair->prop_ato));
486 MC_free_snapshot(pair->system_state);
491 static void acceptance_pair_free_voidp(void *p){
492 acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
496 /********* DDFS Algorithm *********/
499 void MC_ddfs_init(void){
501 initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
503 XBT_DEBUG("**************************************************");
504 XBT_DEBUG("Double-DFS init");
505 XBT_DEBUG("**************************************************");
507 mc_pair_t mc_initial_pair = NULL;
508 mc_state_t initial_graph_state = NULL;
509 smx_process_t process;
512 MC_wait_for_requests();
516 initial_graph_state = MC_state_new();
517 xbt_swag_foreach(process, simix_global->process_list){
518 if(MC_process_is_enabled(process)){
519 MC_state_interleave_process(initial_graph_state, process);
523 acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
524 visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
525 successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
527 /* Save the initial state */
528 initial_state_liveness->snapshot = MC_take_snapshot();
532 unsigned int cursor = 0;
533 xbt_automaton_state_t automaton_state;
535 xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
536 if(automaton_state->type == -1){
539 mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
540 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
544 MC_restore_snapshot(initial_state_liveness->snapshot);
551 if(automaton_state->type == 2){
554 mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
555 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
558 set_acceptance_pair_reached(mc_initial_pair->num, automaton_state);
561 MC_restore_snapshot(initial_state_liveness->snapshot);
571 if(initial_state_liveness->raw_mem_set)
580 void MC_ddfs(int search_cycle){
582 smx_process_t process;
583 mc_pair_t current_pair = NULL;
585 if(xbt_fifo_size(mc_stack_liveness) == 0)
589 /* Get current pair */
590 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
592 /* Update current state in buchi automaton */
593 _mc_property_automaton->current_state = current_pair->automaton_state;
596 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
598 mc_stats->visited_pairs++;
601 mc_state_t next_graph_state = NULL;
602 smx_simcall_t req = NULL;
605 xbt_automaton_transition_t transition_succ;
606 unsigned int cursor = 0;
609 mc_pair_t next_pair = NULL;
612 mc_pair_t pair_to_remove;
614 if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
616 if(current_pair->requests > 0){
618 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
620 /* Debug information */
622 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
623 req_str = MC_request_to_string(req, value);
624 XBT_DEBUG("Execute: %s", req_str);
628 MC_state_set_executed_request(current_pair->graph_state, req, value);
629 mc_stats->executed_transitions++;
631 /* Answer the request */
632 SIMIX_simcall_pre(req, value);
634 /* Wait for requests (schedules processes) */
635 MC_wait_for_requests();
639 /* Create the new expanded graph_state */
640 next_graph_state = MC_state_new();
642 /* Get enabled process and insert it in the interleave set of the next graph_state */
643 xbt_swag_foreach(process, simix_global->process_list){
644 if(MC_process_is_enabled(process)){
645 XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
649 xbt_swag_foreach(process, simix_global->process_list){
650 if(MC_process_is_enabled(process)){
651 MC_state_interleave_process(next_graph_state, process);
655 xbt_dynar_reset(successors);
661 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
663 res = MC_automaton_evaluate_label(transition_succ->label);
665 if(res == 1){ // enabled transition in automaton
667 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
668 xbt_dynar_push(successors, &next_pair);
676 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
678 res = MC_automaton_evaluate_label(transition_succ->label);
680 if(res == 2){ // true transition in automaton
682 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
683 xbt_dynar_push(successors, &next_pair);
691 xbt_dynar_foreach(successors, cursor, pair_succ){
693 if(search_cycle == 1){
695 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
697 if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
699 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
701 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
702 XBT_INFO("| ACCEPTANCE CYCLE |");
703 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
704 XBT_INFO("Counter-example that violates formula :");
705 MC_show_stack_liveness(mc_stack_liveness);
706 MC_dump_stack_liveness(mc_stack_liveness);
707 MC_print_statistics(mc_stats);
712 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
714 XBT_DEBUG("Next pair already visited !");
719 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
721 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
724 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
727 MC_ddfs(search_cycle);
735 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
737 XBT_DEBUG("Next pair already visited !");
743 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
746 MC_ddfs(search_cycle);
753 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
755 XBT_DEBUG("Next pair already visited !");
760 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
762 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
764 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
768 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
773 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
776 MC_ddfs(search_cycle);
782 /* Restore system before checking others successors */
783 if(cursor != (xbt_dynar_length(successors) - 1))
784 MC_replay_liveness(mc_stack_liveness, 1);
788 if(MC_state_interleave_size(current_pair->graph_state) > 0){
789 XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
790 MC_replay_liveness(mc_stack_liveness, 0);
797 mc_stats->executed_transitions++;
799 XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
803 /* Create the new expanded graph_state */
804 next_graph_state = MC_state_new();
806 xbt_dynar_reset(successors);
812 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
814 res = MC_automaton_evaluate_label(transition_succ->label);
816 if(res == 1){ // enabled transition in automaton
818 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
819 xbt_dynar_push(successors, &next_pair);
827 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
829 res = MC_automaton_evaluate_label(transition_succ->label);
831 if(res == 2){ // true transition in automaton
833 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
834 xbt_dynar_push(successors, &next_pair);
842 xbt_dynar_foreach(successors, cursor, pair_succ){
844 if(search_cycle == 1){
846 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
848 if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
850 XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
852 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
853 XBT_INFO("| ACCEPTANCE CYCLE |");
854 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
855 XBT_INFO("Counter-example that violates formula :");
856 MC_show_stack_liveness(mc_stack_liveness);
857 MC_dump_stack_liveness(mc_stack_liveness);
858 MC_print_statistics(mc_stats);
863 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
865 XBT_DEBUG("Next pair already visited !");
870 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
872 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
875 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
878 MC_ddfs(search_cycle);
886 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
888 XBT_DEBUG("Next pair already visited !");
894 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
897 MC_ddfs(search_cycle);
906 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
908 XBT_DEBUG("Next pair already visited !");
913 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
915 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
919 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
924 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
927 MC_ddfs(search_cycle);
933 /* Restore system before checking others successors */
934 if(cursor != xbt_dynar_length(successors) - 1)
935 MC_replay_liveness(mc_stack_liveness, 1);
943 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
944 if(MC_state_interleave_size(current_pair->graph_state) > 0){
945 XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
946 XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
951 if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
952 XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
954 XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
959 pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
960 xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
961 pair_to_remove = NULL;
962 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
963 remove_acceptance_pair(current_pair->num);