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;
610 mc_pair_t next_pair = NULL;
613 mc_pair_t pair_to_remove;
615 if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
617 if(current_pair->requests > 0){
619 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
621 /* Debug information */
623 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
624 req_str = MC_request_to_string(req, value);
625 XBT_DEBUG("Execute: %s", req_str);
629 MC_state_set_executed_request(current_pair->graph_state, req, value);
630 mc_stats->executed_transitions++;
632 /* Answer the request */
633 SIMIX_simcall_pre(req, value);
635 /* Wait for requests (schedules processes) */
636 MC_wait_for_requests();
640 /* Create the new expanded graph_state */
641 next_graph_state = MC_state_new();
643 /* Get enabled process and insert it in the interleave set of the next graph_state */
644 xbt_swag_foreach(process, simix_global->process_list){
645 if(MC_process_is_enabled(process)){
646 XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
650 xbt_swag_foreach(process, simix_global->process_list){
651 if(MC_process_is_enabled(process)){
652 MC_state_interleave_process(next_graph_state, process);
656 xbt_dynar_reset(successors);
662 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
664 res = MC_automaton_evaluate_label(transition_succ->label);
666 if(res == 1){ // enabled transition in automaton
668 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
669 xbt_dynar_push(successors, &next_pair);
677 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
679 res = MC_automaton_evaluate_label(transition_succ->label);
681 if(res == 2){ // true transition in automaton
683 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
684 xbt_dynar_push(successors, &next_pair);
692 xbt_dynar_foreach(successors, cursor, pair_succ){
694 if(search_cycle == 1){
696 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
698 if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){
700 XBT_INFO("Next pair (depth = %d, %u interleave) already reached (equal to state %d) !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state), reached_num);
702 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
703 XBT_INFO("| ACCEPTANCE CYCLE |");
704 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
705 XBT_INFO("Counter-example that violates formula :");
706 MC_show_stack_liveness(mc_stack_liveness);
707 MC_dump_stack_liveness(mc_stack_liveness);
708 MC_print_statistics(mc_stats);
713 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
715 XBT_DEBUG("Next pair already visited !");
720 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
722 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
725 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
728 MC_ddfs(search_cycle);
736 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
738 XBT_DEBUG("Next pair already visited !");
744 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
747 MC_ddfs(search_cycle);
754 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
756 XBT_DEBUG("Next pair already visited !");
761 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
763 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
765 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
769 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
774 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
777 MC_ddfs(search_cycle);
783 /* Restore system before checking others successors */
784 if(cursor != (xbt_dynar_length(successors) - 1))
785 MC_replay_liveness(mc_stack_liveness, 1);
789 if(MC_state_interleave_size(current_pair->graph_state) > 0){
790 XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
791 MC_replay_liveness(mc_stack_liveness, 0);
798 mc_stats->executed_transitions++;
800 XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
804 /* Create the new expanded graph_state */
805 next_graph_state = MC_state_new();
807 xbt_dynar_reset(successors);
813 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
815 res = MC_automaton_evaluate_label(transition_succ->label);
817 if(res == 1){ // enabled transition in automaton
819 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
820 xbt_dynar_push(successors, &next_pair);
828 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
830 res = MC_automaton_evaluate_label(transition_succ->label);
832 if(res == 2){ // true transition in automaton
834 next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
835 xbt_dynar_push(successors, &next_pair);
843 xbt_dynar_foreach(successors, cursor, pair_succ){
845 if(search_cycle == 1){
847 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
849 if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){
851 XBT_INFO("Next pair (depth = %d) already reached (equal to state %d)!", xbt_fifo_size(mc_stack_liveness) + 1, reached_num);
853 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
854 XBT_INFO("| ACCEPTANCE CYCLE |");
855 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
856 XBT_INFO("Counter-example that violates formula :");
857 MC_show_stack_liveness(mc_stack_liveness);
858 MC_dump_stack_liveness(mc_stack_liveness);
859 MC_print_statistics(mc_stats);
864 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
866 XBT_DEBUG("Next pair already visited !");
871 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
873 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
876 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
879 MC_ddfs(search_cycle);
887 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
889 XBT_DEBUG("Next pair already visited !");
895 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
898 MC_ddfs(search_cycle);
907 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
909 XBT_DEBUG("Next pair already visited !");
914 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
916 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
920 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
925 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
928 MC_ddfs(search_cycle);
934 /* Restore system before checking others successors */
935 if(cursor != xbt_dynar_length(successors) - 1)
936 MC_replay_liveness(mc_stack_liveness, 1);
944 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
945 if(MC_state_interleave_size(current_pair->graph_state) > 0){
946 XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
947 XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
952 if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
953 XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
955 XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
960 pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
961 xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
962 pair_to_remove = NULL;
963 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
964 remove_acceptance_pair(current_pair->num);