4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
5 "Logging specific to algorithms for liveness properties verification");
7 xbt_dynar_t initial_pairs = NULL;
8 xbt_dynar_t reached_pairs;
9 extern mc_snapshot_t initial_snapshot;
11 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
13 p = xbt_new0(s_mc_pair_t, 1);
15 p->automaton_state = st;
17 mc_stats_pair->expanded_pairs++;
22 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
24 if(s1->num_reg != s2->num_reg)
28 for(i=0 ; i< s1->num_reg ; i++){
30 if(s1->regions[i]->size != s2->regions[i]->size)
33 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
36 XBT_DEBUG("(%d) Snapshot ok before memcmp on data", i);
38 if(s1->regions[i]->type != s2->regions[i]->type)
41 if(s1->regions[i]->type == 0){
42 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0)
52 int reached(xbt_automaton_t a, mc_snapshot_t s){
54 if(xbt_dynar_is_empty(reached_pairs)){
59 mc_pair_reached_t pair = NULL;
60 pair = xbt_new0(s_mc_pair_reached_t, 1);
61 pair->automaton_state = a->current_state;
62 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
63 pair->system_state = s;
65 /* Get values of propositional symbols */
66 unsigned int cursor = 0;
67 xbt_propositional_symbol_t ps = NULL;
68 xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
69 int (*f)() = ps->function;
71 xbt_dynar_push(pair->prop_ato, &res);
75 mc_pair_reached_t pair_test;
77 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
78 if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
79 if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
80 if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
94 int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){
96 if(reached(a, s) == 0){
100 mc_pair_reached_t pair = NULL;
101 pair = xbt_new0(s_mc_pair_reached_t, 1);
102 pair->automaton_state = a->current_state;
103 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
104 pair->system_state = s;
106 /* Get values of propositional symbols */
107 unsigned int cursor = 0;
108 xbt_propositional_symbol_t ps = NULL;
109 xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
110 int (*f)() = ps->function;
112 xbt_dynar_push(pair->prop_ato, &res);
115 xbt_dynar_push(reached_pairs, &pair);
126 void MC_pair_delete(mc_pair_t pair){
127 xbt_free(pair->graph_state->proc_status);
128 xbt_free(pair->graph_state);
129 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
134 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
138 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
139 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
140 return (left_res || right_res);
144 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
145 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
146 return (left_res && right_res);
150 int res = MC_automaton_evaluate_label(a, l->u.exp_not);
155 unsigned int cursor = 0;
156 xbt_propositional_symbol_t p = NULL;
157 xbt_dynar_foreach(a->propositional_symbols, cursor, p){
158 if(strcmp(p->pred, l->u.predicat) == 0){
159 int (*f)() = p->function;
176 /********************* Double-DFS stateful without visited state *******************/
179 void MC_ddfs_stateful_init(xbt_automaton_t a){
181 XBT_DEBUG("**************************************************");
182 XBT_DEBUG("Double-DFS stateful without visited state init");
183 XBT_DEBUG("**************************************************");
185 mc_pair_t mc_initial_pair;
186 mc_state_t initial_graph_state;
187 smx_process_t process;
188 mc_snapshot_t init_snapshot;
190 MC_wait_for_requests();
194 init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
196 initial_graph_state = MC_state_pair_new();
197 xbt_swag_foreach(process, simix_global->process_list){
198 if(MC_process_is_enabled(process)){
199 MC_state_interleave_process(initial_graph_state, process);
203 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
205 MC_take_snapshot(init_snapshot);
209 unsigned int cursor = 0;
210 xbt_state_t state = NULL;
212 xbt_dynar_foreach(a->states, cursor, state){
213 if(state->type == -1){
216 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
217 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
221 MC_ddfs_stateful(a, 0, 0);
223 MC_restore_snapshot(init_snapshot);
225 MC_ddfs_stateful(a, 0, 0);
228 if(state->type == 2){
231 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
232 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
236 MC_ddfs_stateful(a, 1, 0);
238 MC_restore_snapshot(init_snapshot);
240 MC_ddfs_stateful(a, 1, 0);
248 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
250 smx_process_t process = NULL;
251 mc_pair_t current_pair = NULL;
253 if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
257 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
258 MC_restore_snapshot(current_pair->system_state);
259 xbt_swag_foreach(process, simix_global->process_list){
260 if(MC_process_is_enabled(process)){
261 MC_state_interleave_process(current_pair->graph_state, process);
267 /* Get current state */
268 current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
271 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
272 XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
274 a->current_state = current_pair->automaton_state;
276 mc_stats_pair->visited_pairs++;
279 mc_state_t next_graph_state = NULL;
280 smx_req_t req = NULL;
284 xbt_transition_t transition_succ;
288 xbt_dynar_t successors = NULL;
290 mc_pair_t next_pair = NULL;
291 mc_snapshot_t next_snapshot = NULL;
292 mc_snapshot_t current_snapshot = NULL;
296 successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
299 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
302 current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
303 MC_take_snapshot(current_snapshot);
307 /* Debug information */
308 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
309 req_str = MC_request_to_string(req, value);
310 XBT_DEBUG("Execute: %s", req_str);
314 MC_state_set_executed_request(current_pair->graph_state, req, value);
316 /* Answer the request */
317 SIMIX_request_pre(req, value);
319 /* Wait for requests (schedules processes) */
320 MC_wait_for_requests();
323 /* Create the new expanded graph_state */
326 next_graph_state = MC_state_pair_new();
328 /* Get enabled process and insert it in the interleave set of the next graph_state */
329 xbt_swag_foreach(process, simix_global->process_list){
330 if(MC_process_is_enabled(process)){
331 MC_state_interleave_process(next_graph_state, process);
335 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
336 MC_take_snapshot(next_snapshot);
338 xbt_dynar_reset(successors);
344 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
346 res = MC_automaton_evaluate_label(a, transition_succ->label);
348 if(res == 1){ // enabled transition in automaton
350 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
351 xbt_dynar_push(successors, &next_pair);
358 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
360 res = MC_automaton_evaluate_label(a, transition_succ->label);
362 if(res == 2){ // transition always enabled in automaton
364 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
365 xbt_dynar_push(successors, &next_pair);
373 if(xbt_dynar_length(successors) == 0){
376 next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
377 xbt_dynar_push(successors, &next_pair);
382 //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors));
385 xbt_dynar_foreach(successors, cursor, pair_succ){
387 //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
389 if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
390 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
391 XBT_INFO("| ACCEPTANCE CYCLE |");
392 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
393 XBT_INFO("Counter-example that violates formula :");
394 MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
395 MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
396 MC_print_statistics_pairs(mc_stats_pair);
400 //mc_stats_pair->executed_transitions++;
403 xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
406 MC_ddfs_stateful(a, search_cycle, 0);
409 if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
411 int res = set_pair_reached(a, next_snapshot);
412 XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
415 xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
418 MC_ddfs_stateful(a, 1, 1);
422 xbt_dynar_pop(reached_pairs, NULL);
429 if(MC_state_interleave_size(current_pair->graph_state) > 0){
430 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
431 MC_restore_snapshot(current_snapshot);
439 xbt_fifo_shift(mc_stack_liveness_stateful);
440 XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
447 /********************* Double-DFS stateless *******************/
449 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
450 xbt_free(pair->graph_state->proc_status);
451 xbt_free(pair->graph_state);
452 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
456 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
457 mc_pair_stateless_t p = NULL;
458 p = xbt_new0(s_mc_pair_stateless_t, 1);
459 p->automaton_state = st;
461 mc_stats_pair->expanded_pairs++;
467 void MC_ddfs_stateless_init(xbt_automaton_t a){
469 XBT_DEBUG("**************************************************");
470 XBT_DEBUG("Double-DFS stateless init");
471 XBT_DEBUG("**************************************************");
473 mc_pair_stateless_t mc_initial_pair = NULL;
474 mc_state_t initial_graph_state = NULL;
475 smx_process_t process;
477 MC_wait_for_requests();
480 initial_graph_state = MC_state_pair_new();
481 xbt_swag_foreach(process, simix_global->process_list){
482 if(MC_process_is_enabled(process)){
483 MC_state_interleave_process(initial_graph_state, process);
487 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
489 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
490 MC_take_snapshot(initial_snapshot);
494 unsigned int cursor = 0;
497 xbt_dynar_foreach(a->states, cursor, state){
498 if(state->type == -1){
501 mc_initial_pair = new_pair_stateless(initial_graph_state, state);
502 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
506 MC_ddfs_stateless(a, 0, 0);
508 MC_restore_snapshot(initial_snapshot);
510 MC_ddfs_stateless(a, 0, 0);
513 if(state->type == 2){
516 mc_initial_pair = new_pair_stateless(initial_graph_state, state);
517 xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
521 MC_ddfs_stateless(a, 1, 0);
523 MC_restore_snapshot(initial_snapshot);
525 MC_ddfs_stateless(a, 1, 0);
534 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
536 smx_process_t process;
537 mc_pair_stateless_t current_pair = NULL;
539 if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
543 MC_replay_liveness(mc_stack_liveness_stateless);
544 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
545 xbt_swag_foreach(process, simix_global->process_list){
546 if(MC_process_is_enabled(process)){
547 MC_state_interleave_process(current_pair->graph_state, process);
552 /* Get current pair */
553 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
555 /* Update current state in buchi automaton */
556 a->current_state = current_pair->automaton_state;
558 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
559 XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
562 mc_stats_pair->visited_pairs++;
565 mc_state_t next_graph_state = NULL;
566 smx_req_t req = NULL;
569 xbt_transition_t transition_succ;
570 unsigned int cursor = 0;
573 mc_pair_stateless_t next_pair = NULL;
574 mc_pair_stateless_t pair_succ;
575 mc_snapshot_t next_snapshot = NULL;
577 xbt_dynar_t successors = NULL;
580 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
583 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
586 /* Debug information */
587 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
588 req_str = MC_request_to_string(req, value);
589 XBT_DEBUG("Execute: %s", req_str);
595 MC_state_set_executed_request(current_pair->graph_state, req, value);
597 /* Answer the request */
598 SIMIX_request_pre(req, value);
600 /* Wait for requests (schedules processes) */
601 MC_wait_for_requests();
606 /* Create the new expanded graph_state */
607 next_graph_state = MC_state_pair_new();
609 /* Get enabled process and insert it in the interleave set of the next graph_state */
610 xbt_swag_foreach(process, simix_global->process_list){
611 if(MC_process_is_enabled(process)){
612 MC_state_interleave_process(next_graph_state, process);
616 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
617 MC_take_snapshot(next_snapshot);
619 xbt_dynar_reset(successors);
625 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
627 res = MC_automaton_evaluate_label(a, transition_succ->label);
629 if(res == 1){ // enabled transition in automaton
631 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
632 xbt_dynar_push(successors, &next_pair);
640 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
642 res = MC_automaton_evaluate_label(a, transition_succ->label);
644 if(res == 2){ // enabled transition in automaton
646 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
647 xbt_dynar_push(successors, &next_pair);
654 if(xbt_dynar_length(successors) == 0){
656 next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
657 xbt_dynar_push(successors, &next_pair);
663 xbt_dynar_foreach(successors, cursor, pair_succ){
665 if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
666 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
667 XBT_INFO("| ACCEPTANCE CYCLE |");
668 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
669 XBT_INFO("Counter-example that violates formula :");
670 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
671 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
672 MC_print_statistics_pairs(mc_stats_pair);
677 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
680 MC_ddfs_stateless(a, search_cycle, 0);
683 if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
685 XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
686 int res = set_pair_reached(a, next_snapshot);
689 xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
692 MC_ddfs_stateless(a, 1, 1);
696 xbt_dynar_pop(reached_pairs, NULL);
702 if(MC_state_interleave_size(current_pair->graph_state) > 0){
703 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
704 MC_replay_liveness(mc_stack_liveness_stateless);
710 xbt_fifo_shift(mc_stack_liveness_stateless);
711 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);