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 xbt_dynar_t get_atomic_propositions_values(){
25 unsigned int cursor = 0;
26 xbt_automaton_propositional_symbol_t ps = NULL;
27 xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
29 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
30 f = (int_f_void_t)ps->function;
32 xbt_dynar_push_as(values, int, res);
38 static int is_reached_acceptance_pair(mc_pair_t pair){
40 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
42 if(xbt_dynar_is_empty(acceptance_pairs)){
45 if(pair->graph_state->system_state == NULL){
46 pair->graph_state->system_state = MC_take_snapshot();
47 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
49 xbt_dynar_push(acceptance_pairs, &pair);
61 if(pair->graph_state->system_state == NULL){
62 pair->graph_state->system_state = MC_take_snapshot();
63 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
66 size_t current_bytes_used = pair->heap_bytes_used;
67 int current_nb_processes = pair->nb_processes;
69 unsigned int cursor = 0;
70 int previous_cursor = 0, next_cursor = 0;
72 int end = xbt_dynar_length(acceptance_pairs) - 1;
74 mc_pair_t pair_test = NULL;
75 size_t bytes_used_test;
76 int nb_processes_test;
77 int same_processes_and_bytes_not_found = 1;
79 while(start <= end && same_processes_and_bytes_not_found){
80 cursor = (start + end) / 2;
81 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
82 bytes_used_test = pair_test->heap_bytes_used;
83 nb_processes_test = pair_test->nb_processes;
84 if(nb_processes_test < current_nb_processes)
86 else if(nb_processes_test > current_nb_processes)
88 else if(nb_processes_test == current_nb_processes){
89 if(bytes_used_test < current_bytes_used)
91 else if(bytes_used_test > current_bytes_used)
93 else if(bytes_used_test == current_bytes_used){
94 same_processes_and_bytes_not_found = 0;
95 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
96 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
97 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
102 return pair_test->num;
106 /* Search another pair with same number of bytes used in std_heap */
107 previous_cursor = cursor - 1;
108 while(previous_cursor >= 0){
109 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_pair_t);
110 bytes_used_test = pair_test->heap_bytes_used;
111 if(bytes_used_test != current_bytes_used)
113 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
114 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
115 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
120 return pair_test->num;
126 next_cursor = cursor + 1;
127 while(next_cursor < xbt_dynar_length(acceptance_pairs)){
128 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_pair_t);
129 bytes_used_test = pair_test->heap_bytes_used;
130 if(bytes_used_test != current_bytes_used)
132 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
133 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
134 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
139 return pair_test->num;
149 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
150 bytes_used_test = pair_test->heap_bytes_used;
152 if(bytes_used_test < current_bytes_used)
153 xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
155 xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
170 static void set_acceptance_pair_reached(mc_pair_t pair){
172 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
174 if(xbt_dynar_is_empty(acceptance_pairs)){
177 if(pair->graph_state->system_state == NULL){
178 pair->graph_state->system_state = MC_take_snapshot();
179 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
181 xbt_dynar_push(acceptance_pairs, &pair);
188 if(pair->graph_state->system_state == NULL){
189 pair->graph_state->system_state = MC_take_snapshot();
190 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
193 size_t current_bytes_used = pair->heap_bytes_used;
194 int current_nb_processes = pair->nb_processes;
196 unsigned int cursor = 0;
198 int end = xbt_dynar_length(acceptance_pairs) - 1;
200 mc_pair_t pair_test = NULL;
201 size_t bytes_used_test = 0;
202 int nb_processes_test;
205 cursor = (start + end) / 2;
206 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
207 bytes_used_test = pair_test->heap_bytes_used;
208 nb_processes_test = pair_test->nb_processes;
209 if(nb_processes_test < current_nb_processes)
211 if(nb_processes_test > current_nb_processes)
213 if(nb_processes_test == current_nb_processes){
214 if(bytes_used_test < current_bytes_used)
216 if(bytes_used_test > current_bytes_used)
218 if(bytes_used_test == current_bytes_used)
223 if(bytes_used_test < current_bytes_used)
224 xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
226 xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
237 static void remove_acceptance_pair(mc_pair_t pair){
239 unsigned int cursor = 0;
243 xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
244 if(pair_test->num == pair->num){
251 xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
253 pair->acceptance_removed = 1;
255 if(pair->stack_removed && pair->acceptance_removed){
256 if(_sg_mc_visited == 0){
257 MC_pair_delete(pair);
258 }else if(pair->visited_removed){
259 MC_pair_delete(pair);
265 static int is_visited_pair(mc_pair_t pair){
267 if(_sg_mc_visited == 0)
270 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
272 if(xbt_dynar_is_empty(visited_pairs)){
275 if(pair->graph_state->system_state == NULL)
276 pair->graph_state->system_state = MC_take_snapshot();
277 xbt_dynar_push(visited_pairs, &pair);
289 if(pair->graph_state->system_state == NULL)
290 pair->graph_state->system_state = MC_take_snapshot();
292 size_t current_bytes_used = pair->heap_bytes_used;
293 int current_nb_processes = pair->nb_processes;
295 unsigned int cursor = 0;
296 int previous_cursor = 0, next_cursor = 0;
298 int end = xbt_dynar_length(visited_pairs) - 1;
300 mc_pair_t pair_test = NULL;
301 size_t bytes_used_test;
302 int nb_processes_test;
303 int same_processes_and_bytes_not_found = 1;
306 while(start <= end && same_processes_and_bytes_not_found){
307 cursor = (start + end) / 2;
308 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
309 bytes_used_test = pair_test->heap_bytes_used;
310 nb_processes_test = pair_test->nb_processes;
311 if(nb_processes_test < current_nb_processes)
313 else if(nb_processes_test > current_nb_processes)
315 else if(nb_processes_test == current_nb_processes){
316 if(bytes_used_test < current_bytes_used)
318 else if(bytes_used_test > current_bytes_used)
320 else if(bytes_used_test == current_bytes_used){
321 same_processes_and_bytes_not_found = 0;
322 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
323 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
324 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
325 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
326 xbt_dynar_insert_at(visited_pairs, cursor, &pair);
327 pair_test->visited_removed = 1;
328 result = pair_test->num;
329 if(pair_test->stack_removed && pair_test->visited_removed){
330 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
331 if(pair_test->acceptance_removed){
332 MC_pair_delete(pair_test);
335 MC_pair_delete(pair_test);
346 /* Search another pair with same number of bytes used in std_heap */
347 previous_cursor = cursor - 1;
348 while(previous_cursor >= 0){
349 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_pair_t);
350 bytes_used_test = pair_test->heap_bytes_used;
351 if(bytes_used_test != current_bytes_used)
353 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
354 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
355 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
356 xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
357 xbt_dynar_insert_at(visited_pairs, previous_cursor, &pair);
358 pair_test->visited_removed = 1;
359 result = pair_test->num;
360 if(pair_test->stack_removed && pair_test->visited_removed){
361 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
362 if(pair_test->acceptance_removed){
363 MC_pair_delete(pair_test);
366 MC_pair_delete(pair_test);
379 next_cursor = cursor + 1;
380 while(next_cursor < xbt_dynar_length(visited_pairs)){
381 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_pair_t);
382 bytes_used_test = pair_test->heap_bytes_used;
383 if(bytes_used_test != current_bytes_used)
385 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
386 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
387 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
388 xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
389 xbt_dynar_insert_at(visited_pairs, next_cursor, &pair);
390 pair_test->visited_removed = 1;
391 result = pair_test->num;
392 if(pair_test->stack_removed && pair_test->visited_removed){
393 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
394 if(pair_test->acceptance_removed){
395 MC_pair_delete(pair_test);
398 MC_pair_delete(pair_test);
415 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
416 bytes_used_test = pair_test->heap_bytes_used;
418 if(bytes_used_test < current_bytes_used)
419 xbt_dynar_insert_at(visited_pairs, cursor + 1, &pair);
421 xbt_dynar_insert_at(visited_pairs, cursor, &pair);
423 if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
424 int min = mc_stats->expanded_states;
425 unsigned int cursor2 = 0;
426 unsigned int index = 0;
427 xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
428 if(pair_test->num < min){
430 min = pair_test->num;
433 xbt_dynar_remove_at(visited_pairs, index, &pair_test);
434 pair_test->visited_removed = 1;
435 if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
436 MC_pair_delete(pair_test);
451 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
455 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
456 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
457 return (left_res || right_res);
460 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
461 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
462 return (left_res && right_res);
465 int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
469 unsigned int cursor = 0;
470 xbt_automaton_propositional_symbol_t p = NULL;
471 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
472 if(strcmp(p->pred, l->u.predicat) == 0)
473 return (int)xbt_dynar_get_as(atomic_propositions_values, cursor, int);
486 /********* DDFS Algorithm *********/
489 void MC_ddfs_init(void){
491 initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
493 XBT_DEBUG("**************************************************");
494 XBT_DEBUG("Double-DFS init");
495 XBT_DEBUG("**************************************************");
497 mc_pair_t initial_pair = NULL;
498 smx_process_t process;
500 MC_wait_for_requests();
504 acceptance_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL);
505 visited_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL);
506 successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
508 initial_state_liveness->snapshot = MC_take_snapshot();
512 unsigned int cursor = 0;
513 xbt_automaton_state_t automaton_state;
515 xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
516 if(automaton_state->type == -1){ /* Initial automaton state */
520 initial_pair = MC_pair_new();
521 initial_pair->automaton_state = automaton_state;
522 initial_pair->graph_state = MC_state_new();
523 initial_pair->atomic_propositions = get_atomic_propositions_values();
525 /* Get enabled process and insert it in the interleave set of the graph_state */
526 xbt_swag_foreach(process, simix_global->process_list){
527 if(MC_process_is_enabled(process)){
528 MC_state_interleave_process(initial_pair->graph_state, process);
532 initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
533 initial_pair->search_cycle = 0;
535 xbt_fifo_unshift(mc_stack_liveness, initial_pair);
542 MC_restore_snapshot(initial_state_liveness->snapshot);
547 }else if(automaton_state->type == 2){ /* Acceptance automaton state */
551 initial_pair = MC_pair_new();
552 initial_pair->automaton_state = automaton_state;
553 initial_pair->graph_state = MC_state_new();
554 initial_pair->atomic_propositions = get_atomic_propositions_values();
556 /* Get enabled process and insert it in the interleave set of the graph_state */
557 xbt_swag_foreach(process, simix_global->process_list){
558 if(MC_process_is_enabled(process)){
559 MC_state_interleave_process(initial_pair->graph_state, process);
563 initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
564 initial_pair->search_cycle = 1;
566 xbt_fifo_unshift(mc_stack_liveness, initial_pair);
570 set_acceptance_pair_reached(initial_pair);
575 MC_restore_snapshot(initial_state_liveness->snapshot);
581 if(initial_state_liveness->raw_mem_set)
592 smx_process_t process;
593 mc_pair_t current_pair = NULL;
595 if(xbt_fifo_size(mc_stack_liveness) == 0)
598 /* Get current pair */
599 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
601 /* Update current state in buchi automaton */
602 _mc_property_automaton->current_state = current_pair->automaton_state;
604 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle);
606 mc_stats->visited_pairs++;
609 smx_simcall_t req = NULL;
612 xbt_automaton_transition_t transition_succ;
613 unsigned int cursor = 0;
615 int reached_num, visited_num;
618 mc_pair_t next_pair = NULL;
619 xbt_dynar_t prop_values = NULL;
621 if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
623 if(current_pair->requests > 0){
625 if(current_pair->search_cycle){
627 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
629 if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
631 XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
634 xbt_fifo_shift(mc_stack_liveness);
637 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
638 XBT_INFO("| ACCEPTANCE CYCLE |");
639 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
640 XBT_INFO("Counter-example that violates formula :");
641 MC_show_stack_liveness(mc_stack_liveness);
642 MC_dump_stack_liveness(mc_stack_liveness);
643 MC_print_statistics(mc_stats);
650 if((visited_num = is_visited_pair(current_pair)) != -1){
652 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
656 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
658 /* Debug information */
660 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
661 req_str = MC_request_to_string(req, value);
662 XBT_DEBUG("Execute: %s", req_str);
666 MC_state_set_executed_request(current_pair->graph_state, req, value);
667 mc_stats->executed_transitions++;
669 /* Answer the request */
670 SIMIX_simcall_pre(req, value);
672 /* Wait for requests (schedules processes) */
673 MC_wait_for_requests();
676 prop_values = get_atomic_propositions_values();
679 /* Evaluate enabled transition according to atomic propositions values */
681 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
683 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
685 if(res == 1){ // enabled transition in automaton
688 MC_replay_liveness(mc_stack_liveness, 1);
692 next_pair = MC_pair_new();
693 next_pair->graph_state = MC_state_new();
694 next_pair->automaton_state = transition_succ->dst;
695 next_pair->atomic_propositions = get_atomic_propositions_values();
697 /* Get enabled process and insert it in the interleave set of the next graph_state */
698 xbt_swag_foreach(process, simix_global->process_list){
699 if(MC_process_is_enabled(process)){
700 MC_state_interleave_process(next_pair->graph_state, process);
704 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
706 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
707 next_pair->search_cycle = 1;
709 xbt_fifo_unshift(mc_stack_liveness, next_pair);
711 if(mc_stats->expanded_pairs%1000000 == 0)
712 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
724 /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
726 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
728 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
730 if(res == 2){ // true transition in automaton
733 MC_replay_liveness(mc_stack_liveness, 1);
737 next_pair = MC_pair_new();
738 next_pair->graph_state = MC_state_new();
739 next_pair->automaton_state = transition_succ->dst;
740 next_pair->atomic_propositions = get_atomic_propositions_values();
742 /* Get enabled process and insert it in the interleave set of the next graph_state */
743 xbt_swag_foreach(process, simix_global->process_list){
744 if(MC_process_is_enabled(process)){
745 MC_state_interleave_process(next_pair->graph_state, process);
749 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
751 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
752 next_pair->search_cycle = 1;
754 xbt_fifo_unshift(mc_stack_liveness, next_pair);
756 if(mc_stats->expanded_pairs%1000000 == 0)
757 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
769 if(MC_state_interleave_size(current_pair->graph_state) > 0){
770 XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
771 MC_replay_liveness(mc_stack_liveness, 0);
780 mc_stats->executed_transitions++;
782 XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
784 if(current_pair->search_cycle){
786 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
788 if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
790 XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
793 xbt_fifo_shift(mc_stack_liveness);
796 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
797 XBT_INFO("| ACCEPTANCE CYCLE |");
798 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
799 XBT_INFO("Counter-example that violates formula :");
800 MC_show_stack_liveness(mc_stack_liveness);
801 MC_dump_stack_liveness(mc_stack_liveness);
802 MC_print_statistics(mc_stats);
809 if((visited_num = is_visited_pair(current_pair)) != -1){
811 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
816 prop_values = get_atomic_propositions_values();
819 /* Evaluate enabled transition according to atomic propositions values */
821 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
823 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
825 if(res == 1){ // enabled transition in automaton
828 MC_replay_liveness(mc_stack_liveness, 1);
832 next_pair = MC_pair_new();
833 next_pair->graph_state = MC_state_new();
834 next_pair->automaton_state = transition_succ->dst;
835 next_pair->atomic_propositions = get_atomic_propositions_values();
836 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
838 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
839 next_pair->search_cycle = 1;
841 xbt_fifo_unshift(mc_stack_liveness, next_pair);
843 if(mc_stats->expanded_pairs%1000 == 0)
844 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
856 /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
858 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
860 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
862 if(res == 2){ // true transition in automaton
865 MC_replay_liveness(mc_stack_liveness, 1);
869 next_pair = MC_pair_new();
870 next_pair->graph_state = MC_state_new();
871 next_pair->automaton_state = transition_succ->dst;
872 next_pair->atomic_propositions = get_atomic_propositions_values();
873 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
875 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
876 next_pair->search_cycle = 1;
878 xbt_fifo_unshift(mc_stack_liveness, next_pair);
880 if(mc_stats->expanded_pairs%1000 == 0)
881 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
897 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
898 if(MC_state_interleave_size(current_pair->graph_state) > 0){
899 XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
900 if(_sg_mc_max_depth == 1000)
901 XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
906 if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
907 XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
909 XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
914 xbt_dynar_free(&prop_values);
915 current_pair = xbt_fifo_shift(mc_stack_liveness);
916 current_pair->stack_removed = 1;
917 if(current_pair->search_cycle){
918 remove_acceptance_pair(current_pair);
920 if(_sg_mc_visited == 0)
921 MC_pair_delete(current_pair);
922 else if(current_pair->visited_removed)
923 MC_pair_delete(current_pair);