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 XBT_DEBUG("Compare with state %d", pair_test->num);
98 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
103 return pair_test->num;
107 /* Search another pair with same number of bytes used in std_heap */
108 previous_cursor = cursor - 1;
109 while(previous_cursor >= 0){
110 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_pair_t);
111 bytes_used_test = pair_test->heap_bytes_used;
112 if(bytes_used_test != current_bytes_used)
114 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
115 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
116 XBT_DEBUG("Compare with state %d", pair_test->num);
117 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
122 return pair_test->num;
128 next_cursor = cursor + 1;
129 while(next_cursor < xbt_dynar_length(acceptance_pairs)){
130 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_pair_t);
131 bytes_used_test = pair_test->heap_bytes_used;
132 if(bytes_used_test != current_bytes_used)
134 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
135 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
136 XBT_DEBUG("Compare with state %d", pair_test->num);
137 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
142 return pair_test->num;
152 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
153 bytes_used_test = pair_test->heap_bytes_used;
155 if(bytes_used_test < current_bytes_used)
156 xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
158 xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
173 static void set_acceptance_pair_reached(mc_pair_t pair){
175 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
177 if(xbt_dynar_is_empty(acceptance_pairs)){
180 if(pair->graph_state->system_state == NULL){
181 pair->graph_state->system_state = MC_take_snapshot();
182 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
184 xbt_dynar_push(acceptance_pairs, &pair);
191 if(pair->graph_state->system_state == NULL){
192 pair->graph_state->system_state = MC_take_snapshot();
193 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
196 size_t current_bytes_used = pair->heap_bytes_used;
197 int current_nb_processes = pair->nb_processes;
199 unsigned int cursor = 0;
201 int end = xbt_dynar_length(acceptance_pairs) - 1;
203 mc_pair_t pair_test = NULL;
204 size_t bytes_used_test = 0;
205 int nb_processes_test;
208 cursor = (start + end) / 2;
209 pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
210 bytes_used_test = pair_test->heap_bytes_used;
211 nb_processes_test = pair_test->nb_processes;
212 if(nb_processes_test < current_nb_processes)
214 if(nb_processes_test > current_nb_processes)
216 if(nb_processes_test == current_nb_processes){
217 if(bytes_used_test < current_bytes_used)
219 if(bytes_used_test > current_bytes_used)
221 if(bytes_used_test == current_bytes_used)
226 if(bytes_used_test < current_bytes_used)
227 xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
229 xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
240 static void remove_acceptance_pair(mc_pair_t pair){
242 unsigned int cursor = 0;
246 xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
247 if(pair_test->num == pair->num){
254 xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
256 pair->acceptance_removed = 1;
258 if(pair->stack_removed && pair->acceptance_removed){
259 if(_sg_mc_visited == 0){
260 MC_pair_delete(pair);
261 }else if(pair->visited_removed){
262 MC_pair_delete(pair);
268 static int is_visited_pair(mc_pair_t pair){
270 if(_sg_mc_visited == 0)
273 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
275 if(xbt_dynar_is_empty(visited_pairs)){
278 if(pair->graph_state->system_state == NULL)
279 pair->graph_state->system_state = MC_take_snapshot();
280 xbt_dynar_push(visited_pairs, &pair);
292 if(pair->graph_state->system_state == NULL)
293 pair->graph_state->system_state = MC_take_snapshot();
295 size_t current_bytes_used = pair->heap_bytes_used;
296 int current_nb_processes = pair->nb_processes;
298 unsigned int cursor = 0;
299 int previous_cursor = 0, next_cursor = 0;
301 int end = xbt_dynar_length(visited_pairs) - 1;
303 mc_pair_t pair_test = NULL;
304 size_t bytes_used_test;
305 int nb_processes_test;
306 int same_processes_and_bytes_not_found = 1;
309 while(start <= end && same_processes_and_bytes_not_found){
310 cursor = (start + end) / 2;
311 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
312 bytes_used_test = pair_test->heap_bytes_used;
313 nb_processes_test = pair_test->nb_processes;
314 if(nb_processes_test < current_nb_processes)
316 else if(nb_processes_test > current_nb_processes)
318 else if(nb_processes_test == current_nb_processes){
319 if(bytes_used_test < current_bytes_used)
321 else if(bytes_used_test > current_bytes_used)
323 else if(bytes_used_test == current_bytes_used){
324 same_processes_and_bytes_not_found = 0;
325 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
326 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
327 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
328 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
329 xbt_dynar_insert_at(visited_pairs, cursor, &pair);
330 pair_test->visited_removed = 1;
331 result = pair_test->num;
332 if(pair_test->stack_removed && pair_test->visited_removed){
333 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
334 if(pair_test->acceptance_removed){
335 MC_pair_delete(pair_test);
338 MC_pair_delete(pair_test);
349 /* Search another pair with same number of bytes used in std_heap */
350 previous_cursor = cursor - 1;
351 while(previous_cursor >= 0){
352 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_pair_t);
353 bytes_used_test = pair_test->heap_bytes_used;
354 if(bytes_used_test != current_bytes_used)
356 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
357 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
358 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
359 xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
360 xbt_dynar_insert_at(visited_pairs, previous_cursor, &pair);
361 pair_test->visited_removed = 1;
362 result = pair_test->num;
363 if(pair_test->stack_removed && pair_test->visited_removed){
364 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
365 if(pair_test->acceptance_removed){
366 MC_pair_delete(pair_test);
369 MC_pair_delete(pair_test);
382 next_cursor = cursor + 1;
383 while(next_cursor < xbt_dynar_length(visited_pairs)){
384 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_pair_t);
385 bytes_used_test = pair_test->heap_bytes_used;
386 if(bytes_used_test != current_bytes_used)
388 if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
389 if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
390 if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
391 xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
392 xbt_dynar_insert_at(visited_pairs, next_cursor, &pair);
393 pair_test->visited_removed = 1;
394 result = pair_test->num;
395 if(pair_test->stack_removed && pair_test->visited_removed){
396 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
397 if(pair_test->acceptance_removed){
398 MC_pair_delete(pair_test);
401 MC_pair_delete(pair_test);
418 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
419 bytes_used_test = pair_test->heap_bytes_used;
421 if(bytes_used_test < current_bytes_used)
422 xbt_dynar_insert_at(visited_pairs, cursor + 1, &pair);
424 xbt_dynar_insert_at(visited_pairs, cursor, &pair);
426 if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
427 int min = mc_stats->expanded_states;
428 unsigned int cursor2 = 0;
429 unsigned int index = 0;
430 xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
431 if(pair_test->num < min){
433 min = pair_test->num;
436 xbt_dynar_remove_at(visited_pairs, index, &pair_test);
437 pair_test->visited_removed = 1;
438 if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
439 MC_pair_delete(pair_test);
454 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
458 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
459 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
460 return (left_res || right_res);
463 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
464 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
465 return (left_res && right_res);
468 int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
472 unsigned int cursor = 0;
473 xbt_automaton_propositional_symbol_t p = NULL;
474 xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
475 if(strcmp(p->pred, l->u.predicat) == 0)
476 return (int)xbt_dynar_get_as(atomic_propositions_values, cursor, int);
489 /********* DDFS Algorithm *********/
492 void MC_ddfs_init(void){
494 initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
496 XBT_DEBUG("**************************************************");
497 XBT_DEBUG("Double-DFS init");
498 XBT_DEBUG("**************************************************");
500 mc_pair_t initial_pair = NULL;
501 smx_process_t process;
503 MC_wait_for_requests();
507 acceptance_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL);
508 visited_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL);
509 successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
511 initial_state_liveness->snapshot = MC_take_snapshot();
512 initial_state_liveness->prev_pair = 0;
516 unsigned int cursor = 0;
517 xbt_automaton_state_t automaton_state;
519 xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
520 if(automaton_state->type == -1){ /* Initial automaton state */
524 initial_pair = MC_pair_new();
525 initial_pair->automaton_state = automaton_state;
526 initial_pair->graph_state = MC_state_new();
527 initial_pair->atomic_propositions = get_atomic_propositions_values();
529 /* Get enabled process and insert it in the interleave set of the graph_state */
530 xbt_swag_foreach(process, simix_global->process_list){
531 if(MC_process_is_enabled(process)){
532 MC_state_interleave_process(initial_pair->graph_state, process);
536 initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
537 initial_pair->search_cycle = 0;
539 xbt_fifo_unshift(mc_stack_liveness, initial_pair);
546 MC_restore_snapshot(initial_state_liveness->snapshot);
551 }else if(automaton_state->type == 2){ /* Acceptance automaton state */
555 initial_pair = MC_pair_new();
556 initial_pair->automaton_state = automaton_state;
557 initial_pair->graph_state = MC_state_new();
558 initial_pair->atomic_propositions = get_atomic_propositions_values();
560 /* Get enabled process and insert it in the interleave set of the graph_state */
561 xbt_swag_foreach(process, simix_global->process_list){
562 if(MC_process_is_enabled(process)){
563 MC_state_interleave_process(initial_pair->graph_state, process);
567 initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
568 initial_pair->search_cycle = 1;
570 xbt_fifo_unshift(mc_stack_liveness, initial_pair);
574 set_acceptance_pair_reached(initial_pair);
579 MC_restore_snapshot(initial_state_liveness->snapshot);
585 if(initial_state_liveness->raw_mem_set)
596 smx_process_t process;
597 mc_pair_t current_pair = NULL;
599 if(xbt_fifo_size(mc_stack_liveness) == 0)
602 /* Get current pair */
603 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
605 /* Update current state in buchi automaton */
606 _mc_property_automaton->current_state = current_pair->automaton_state;
608 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle);
610 mc_stats->visited_pairs++;
613 smx_simcall_t req = NULL;
616 xbt_automaton_transition_t transition_succ;
617 unsigned int cursor = 0;
619 int reached_num, visited_num;
622 mc_pair_t next_pair = NULL;
623 xbt_dynar_t prop_values = NULL;
625 if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
627 if(current_pair->requests > 0){
629 if(current_pair->search_cycle){
631 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
633 if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
635 XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
638 xbt_fifo_shift(mc_stack_liveness);
639 if(dot_output != NULL)
640 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req);
643 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
644 XBT_INFO("| ACCEPTANCE CYCLE |");
645 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
646 XBT_INFO("Counter-example that violates formula :");
647 MC_show_stack_liveness(mc_stack_liveness);
648 MC_dump_stack_liveness(mc_stack_liveness);
649 MC_print_statistics(mc_stats);
656 if((visited_num = is_visited_pair(current_pair)) != -1){
658 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
661 if(dot_output != NULL)
662 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
668 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
671 if(dot_output != NULL){
672 if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
673 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
674 xbt_free(initial_state_liveness->prev_req);
676 initial_state_liveness->prev_pair = current_pair->num;
680 /* Debug information */
681 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
682 req_str = MC_request_to_string(req, value);
683 XBT_DEBUG("Execute: %s", req_str);
688 if(dot_output != NULL){
689 initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
690 if(current_pair->search_cycle)
691 fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
695 MC_state_set_executed_request(current_pair->graph_state, req, value);
696 mc_stats->executed_transitions++;
698 /* Answer the request */
699 SIMIX_simcall_pre(req, value);
701 /* Wait for requests (schedules processes) */
702 MC_wait_for_requests();
705 prop_values = get_atomic_propositions_values();
708 /* Evaluate enabled transition according to atomic propositions values */
710 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
712 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
714 if(res == 1){ // enabled transition in automaton
717 MC_replay_liveness(mc_stack_liveness, 1);
721 next_pair = MC_pair_new();
722 next_pair->graph_state = MC_state_new();
723 next_pair->automaton_state = transition_succ->dst;
724 next_pair->atomic_propositions = get_atomic_propositions_values();
726 /* Get enabled process and insert it in the interleave set of the next graph_state */
727 xbt_swag_foreach(process, simix_global->process_list){
728 if(MC_process_is_enabled(process)){
729 MC_state_interleave_process(next_pair->graph_state, process);
733 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
735 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
736 next_pair->search_cycle = 1;
738 xbt_fifo_unshift(mc_stack_liveness, next_pair);
740 if(mc_stats->expanded_pairs%1000000 == 0)
741 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
753 /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
755 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
757 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
759 if(res == 2){ // true transition in automaton
762 MC_replay_liveness(mc_stack_liveness, 1);
766 next_pair = MC_pair_new();
767 next_pair->graph_state = MC_state_new();
768 next_pair->automaton_state = transition_succ->dst;
769 next_pair->atomic_propositions = get_atomic_propositions_values();
771 /* Get enabled process and insert it in the interleave set of the next graph_state */
772 xbt_swag_foreach(process, simix_global->process_list){
773 if(MC_process_is_enabled(process)){
774 MC_state_interleave_process(next_pair->graph_state, process);
778 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
780 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
781 next_pair->search_cycle = 1;
783 xbt_fifo_unshift(mc_stack_liveness, next_pair);
785 if(mc_stats->expanded_pairs%1000000 == 0)
786 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
798 if(MC_state_interleave_size(current_pair->graph_state) > 0){
799 XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
800 MC_replay_liveness(mc_stack_liveness, 0);
809 mc_stats->executed_transitions++;
811 XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
813 if(current_pair->search_cycle){
815 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
817 if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
819 XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
822 xbt_fifo_shift(mc_stack_liveness);
825 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
826 XBT_INFO("| ACCEPTANCE CYCLE |");
827 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
828 XBT_INFO("Counter-example that violates formula :");
829 MC_show_stack_liveness(mc_stack_liveness);
830 MC_dump_stack_liveness(mc_stack_liveness);
831 MC_print_statistics(mc_stats);
838 if((visited_num = is_visited_pair(current_pair)) != -1){
840 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
845 prop_values = get_atomic_propositions_values();
848 /* Evaluate enabled transition according to atomic propositions values */
850 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
852 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
854 if(res == 1){ // enabled transition in automaton
857 MC_replay_liveness(mc_stack_liveness, 1);
861 next_pair = MC_pair_new();
862 next_pair->graph_state = MC_state_new();
863 next_pair->automaton_state = transition_succ->dst;
864 next_pair->atomic_propositions = get_atomic_propositions_values();
865 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
867 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
868 next_pair->search_cycle = 1;
870 xbt_fifo_unshift(mc_stack_liveness, next_pair);
872 if(mc_stats->expanded_pairs%1000 == 0)
873 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
875 if(dot_output != NULL)
876 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
888 /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
890 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
892 res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
894 if(res == 2){ // true transition in automaton
897 MC_replay_liveness(mc_stack_liveness, 1);
901 next_pair = MC_pair_new();
902 next_pair->graph_state = MC_state_new();
903 next_pair->automaton_state = transition_succ->dst;
904 next_pair->atomic_propositions = get_atomic_propositions_values();
905 next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
907 if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
908 next_pair->search_cycle = 1;
910 xbt_fifo_unshift(mc_stack_liveness, next_pair);
912 if(mc_stats->expanded_pairs%1000 == 0)
913 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
915 if(dot_output != NULL)
916 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
932 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
933 if(MC_state_interleave_size(current_pair->graph_state) > 0){
934 XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
935 if(_sg_mc_max_depth == 1000)
936 XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
941 if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
942 XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
944 XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
949 xbt_dynar_free(&prop_values);
950 current_pair = xbt_fifo_shift(mc_stack_liveness);
951 current_pair->stack_removed = 1;
952 if(current_pair->search_cycle){
953 remove_acceptance_pair(current_pair);
955 if(_sg_mc_visited == 0)
956 MC_pair_delete(current_pair);
957 else if(current_pair->visited_removed)
958 MC_pair_delete(current_pair);