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;
9 xbt_dynar_t reached_pairs;
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;
19 mc_stats_pair->expanded_pairs++;
25 int reached(mc_pair_t pair){
27 char* hash_reached = malloc(sizeof(char)*160);
31 char *hash = malloc(sizeof(char)*160);
32 xbt_sha((char *)&pair, hash);
33 xbt_dynar_foreach(reached_pairs, c, hash_reached){
34 if(strcmp(hash, hash_reached) == 0){
44 void set_pair_reached(mc_pair_t pair){
46 if(reached(pair) == 0){
48 char *hash = malloc(sizeof(char)*160) ;
49 xbt_sha((char *)&pair, hash);
50 xbt_dynar_push(reached_pairs, &hash);
56 void MC_show_snapshot_stack(xbt_fifo_t stack){
63 for (item = xbt_fifo_get_last_item(stack);
64 (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
65 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
66 req = MC_state_get_executed_request(pair->graph_state, &value);
68 req_str = MC_request_to_string(req, value);
69 XBT_INFO("%s", req_str);
75 void MC_dump_snapshot_stack(xbt_fifo_t stack){
79 while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
84 void MC_pair_delete(mc_pair_t pair){
85 xbt_free(pair->graph_state->proc_status);
86 xbt_free(pair->graph_state);
87 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
92 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
96 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
97 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
98 return (left_res || right_res);
102 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
103 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
104 return (left_res && right_res);
108 int res = MC_automaton_evaluate_label(a, l->u.exp_not);
113 unsigned int cursor = 0;
114 xbt_propositional_symbol_t p = NULL;
115 xbt_dynar_foreach(a->propositional_symbols, cursor, p){
116 if(strcmp(p->pred, l->u.predicat) == 0){
117 int (*f)() = p->function;
135 /******************************* DFS with visited state *******************************/
137 xbt_dynar_t visited_pairs;
139 void set_pair_visited(mc_pair_t pair, int sc){
142 mc_visited_pair_t p = NULL;
143 p = xbt_new0(s_mc_visited_pair_t, 1);
145 p->search_cycle = sc;
146 char *hash = malloc(sizeof(char)*160);
147 xbt_sha((char *)&p, hash);
148 xbt_dynar_push(visited_pairs, &hash);
153 int visited(mc_pair_t pair, int sc){
155 char* hash_visited = malloc(sizeof(char)*160);
159 mc_visited_pair_t p = NULL;
160 p = xbt_new0(s_mc_visited_pair_t, 1);
162 p->search_cycle = sc;
163 char *hash = malloc(sizeof(char)*160);
164 xbt_sha((char *)&p, hash);
165 xbt_dynar_foreach(visited_pairs, c, hash_visited){
166 if(strcmp(hash, hash_visited) == 0){
178 void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a){
180 XBT_DEBUG("**************************************************");
181 XBT_DEBUG("Double-DFS with visited state and restore snapshot init");
182 XBT_DEBUG("**************************************************");
184 mc_pair_t mc_initial_pair;
185 mc_state_t initial_graph_state;
186 smx_process_t process;
187 mc_snapshot_t init_snapshot;
189 MC_wait_for_requests();
193 init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
195 initial_graph_state = MC_state_pair_new();
196 xbt_swag_foreach(process, simix_global->process_list){
197 if(MC_process_is_enabled(process)){
198 MC_state_interleave_process(initial_graph_state, process);
202 visited_pairs = xbt_dynar_new(sizeof(char *), NULL);
203 reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
205 MC_take_snapshot(init_snapshot);
209 /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
210 -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
212 unsigned int cursor = 0;
213 unsigned int cursor2 = 0;
214 xbt_state_t state = NULL;
216 xbt_transition_t transition_succ;
217 xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
220 xbt_dynar_foreach(a->states, cursor, state){
221 if(state->type == -1){
222 xbt_dynar_foreach(state->out, cursor2, transition_succ){
223 res = MC_automaton_evaluate_label(a, transition_succ->label);
225 if((res == 1) || (res == 2)){
229 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
230 xbt_dynar_push(successors, &mc_initial_pair);
241 if(xbt_dynar_length(successors) == 0){
242 xbt_dynar_foreach(a->states, cursor, state){
243 if(state->type == -1){
246 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
247 xbt_dynar_push(successors, &mc_initial_pair);
255 xbt_dynar_foreach(successors, cursor, pair_succ){
258 xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
259 set_pair_visited(pair_succ, 0);
264 MC_vddfs_with_restore_snapshot(a, 0, 0);
266 MC_vddfs_with_restore_snapshot(a, 0, 1);
272 void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
274 smx_process_t process = NULL;
277 if(xbt_fifo_size(mc_snapshot_stack) == 0)
281 MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
286 /* Get current state */
287 mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
290 xbt_swag_foreach(process, simix_global->process_list){
291 if(MC_process_is_enabled(process)){
292 MC_state_interleave_process(current_pair->graph_state, process);
297 XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
298 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));
301 mc_stats_pair->visited_pairs++;
304 mc_state_t next_graph_state = NULL;
305 smx_req_t req = NULL;
309 xbt_transition_t transition_succ;
313 xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
316 mc_snapshot_t next_snapshot;
317 mc_snapshot_t current_snapshot;
320 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
323 current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
324 MC_take_snapshot(current_snapshot);
328 /* Debug information */
329 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
330 req_str = MC_request_to_string(req, value);
331 XBT_DEBUG("Execute: %s", req_str);
335 MC_state_set_executed_request(current_pair->graph_state, req, value);
337 /* Answer the request */
338 SIMIX_request_pre(req, value);
340 /* Wait for requests (schedules processes) */
341 MC_wait_for_requests();
344 /* Create the new expanded graph_state */
347 next_graph_state = MC_state_pair_new();
349 /* Get enabled process and insert it in the interleave set of the next graph_state */
350 xbt_swag_foreach(process, simix_global->process_list){
351 if(MC_process_is_enabled(process)){
352 MC_state_interleave_process(next_graph_state, process);
356 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
357 MC_take_snapshot(next_snapshot);
361 xbt_dynar_reset(successors);
364 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
366 res = MC_automaton_evaluate_label(a, transition_succ->label);
370 if((res == 1) || (res == 2)){ // enabled transition in automaton
371 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
372 xbt_dynar_push(successors, &next_pair);
379 if(xbt_dynar_length(successors) == 0){
382 next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
383 xbt_dynar_push(successors, &next_pair);
390 xbt_dynar_foreach(successors, cursor, pair_succ){
392 //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
394 if((search_cycle == 1) && (reached(pair_succ) == 1)){
395 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
396 XBT_INFO("| ACCEPTANCE CYCLE |");
397 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
398 XBT_INFO("Counter-example that violates formula :");
399 MC_show_snapshot_stack(mc_snapshot_stack);
400 MC_dump_snapshot_stack(mc_snapshot_stack);
401 MC_print_statistics_pairs(mc_stats_pair);
405 if(visited(pair_succ, search_cycle) == 0){
407 mc_stats_pair->executed_transitions++;
410 xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
411 set_pair_visited(pair_succ, search_cycle);
414 MC_vddfs_with_restore_snapshot(a, search_cycle, 0);
416 if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
418 MC_restore_snapshot(current_pair->system_state);
421 xbt_swag_foreach(process, simix_global->process_list){
422 if(MC_process_is_enabled(process)){
423 MC_state_interleave_process(current_pair->graph_state, process);
427 set_pair_reached(current_pair);
428 XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
429 MC_vddfs_with_restore_snapshot(a, 1, 1);
434 XBT_DEBUG("Pair already visited !");
440 if(MC_state_interleave_size(current_pair->graph_state) > 0){
441 MC_restore_snapshot(current_snapshot);
448 xbt_fifo_shift(mc_snapshot_stack);
449 XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
456 /********************* Double-DFS without visited state *******************/
458 void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
460 XBT_DEBUG("**************************************************");
461 XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
462 XBT_DEBUG("**************************************************");
464 mc_pair_t mc_initial_pair;
465 mc_state_t initial_graph_state;
466 smx_process_t process;
467 mc_snapshot_t init_snapshot;
469 MC_wait_for_requests();
473 init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
475 initial_graph_state = MC_state_pair_new();
476 xbt_swag_foreach(process, simix_global->process_list){
477 if(MC_process_is_enabled(process)){
478 MC_state_interleave_process(initial_graph_state, process);
482 reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
484 MC_take_snapshot(init_snapshot);
488 /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
489 -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
491 unsigned int cursor = 0;
492 unsigned int cursor2 = 0;
493 xbt_state_t state = NULL;
495 xbt_transition_t transition_succ;
496 xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
499 xbt_dynar_foreach(a->states, cursor, state){
500 if(state->type == -1){
501 xbt_dynar_foreach(state->out, cursor2, transition_succ){
502 res = MC_automaton_evaluate_label(a, transition_succ->label);
504 if((res == 1) || (res == 2)){
508 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
509 xbt_dynar_push(successors, &mc_initial_pair);
520 if(xbt_dynar_length(successors) == 0){
521 xbt_dynar_foreach(a->states, cursor, state){
522 if(state->type == -1){
525 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
526 xbt_dynar_push(successors, &mc_initial_pair);
534 xbt_dynar_foreach(successors, cursor, pair_succ){
537 xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
542 MC_ddfs_with_restore_snapshot(a, 0, 0);
544 MC_ddfs_with_restore_snapshot(a, 0, 1);
550 void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
552 smx_process_t process = NULL;
555 if(xbt_fifo_size(mc_snapshot_stack) == 0)
559 MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
564 /* Get current state */
565 mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
568 xbt_swag_foreach(process, simix_global->process_list){
569 if(MC_process_is_enabled(process)){
570 MC_state_interleave_process(current_pair->graph_state, process);
575 XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
576 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));
579 mc_stats_pair->visited_pairs++;
582 mc_state_t next_graph_state = NULL;
583 smx_req_t req = NULL;
587 xbt_transition_t transition_succ;
591 xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
594 mc_snapshot_t next_snapshot;
595 mc_snapshot_t current_snapshot;
598 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
601 current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
602 MC_take_snapshot(current_snapshot);
606 /* Debug information */
607 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
608 req_str = MC_request_to_string(req, value);
609 XBT_DEBUG("Execute: %s", req_str);
613 MC_state_set_executed_request(current_pair->graph_state, req, value);
615 /* Answer the request */
616 SIMIX_request_pre(req, value);
618 /* Wait for requests (schedules processes) */
619 MC_wait_for_requests();
622 /* Create the new expanded graph_state */
625 next_graph_state = MC_state_pair_new();
627 /* Get enabled process and insert it in the interleave set of the next graph_state */
628 xbt_swag_foreach(process, simix_global->process_list){
629 if(MC_process_is_enabled(process)){
630 MC_state_interleave_process(next_graph_state, process);
634 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
635 MC_take_snapshot(next_snapshot);
639 xbt_dynar_reset(successors);
642 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
644 res = MC_automaton_evaluate_label(a, transition_succ->label);
648 if((res == 1) || (res == 2)){ // enabled transition in automaton
649 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
650 xbt_dynar_push(successors, &next_pair);
657 if(xbt_dynar_length(successors) == 0){
660 next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
661 xbt_dynar_push(successors, &next_pair);
668 xbt_dynar_foreach(successors, cursor, pair_succ){
670 //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
672 if((search_cycle == 1) && (reached(pair_succ) == 1)){
673 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
674 XBT_INFO("| ACCEPTANCE CYCLE |");
675 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
676 XBT_INFO("Counter-example that violates formula :");
677 MC_show_snapshot_stack(mc_snapshot_stack);
678 MC_dump_snapshot_stack(mc_snapshot_stack);
679 MC_print_statistics_pairs(mc_stats_pair);
683 mc_stats_pair->executed_transitions++;
686 xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
689 MC_ddfs_with_restore_snapshot(a, search_cycle, 0);
691 if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
693 MC_restore_snapshot(current_pair->system_state);
696 xbt_swag_foreach(process, simix_global->process_list){
697 if(MC_process_is_enabled(process)){
698 MC_state_interleave_process(current_pair->graph_state, process);
702 set_pair_reached(current_pair);
703 XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
704 MC_ddfs_with_restore_snapshot(a, 1, 1);
710 if(MC_state_interleave_size(current_pair->graph_state) > 0){
711 MC_restore_snapshot(current_snapshot);
718 xbt_fifo_shift(mc_snapshot_stack);
719 XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);