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 visited_pairs;
10 xbt_dynar_t reached_pairs;
13 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
15 p = xbt_new0(s_mc_pairs_t, 1);
17 p->automaton_state = st;
21 mc_stats_pair->expanded_pairs++;
26 void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){
29 mc_visited_pairs_t p = NULL;
30 p = xbt_new0(s_mc_visited_pairs_t, 1);
32 p->automaton_state = as;
34 char *hash = malloc(sizeof(char)*128);
35 xbt_sha((char *)&p, hash);
36 xbt_dynar_push(visited_pairs, &hash);
41 int reached(mc_state_t gs, xbt_state_t as ){
43 /*mc_reached_pairs_t rp = NULL;
46 int different_process;
49 xbt_dynar_foreach(reached_pairs, c, rp){
50 if(rp->automaton_state == as){
52 for(i=0; i < gs->max_pid; i++){
53 if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){
57 if(different_process==0){
59 XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached (graph=%p)!", gs, as, as->id, rp->graph_state);
66 //XBT_DEBUG("Search acceptance pair already reach !");
68 char* hash_reached = malloc(sizeof(char)*128);
72 mc_reached_pairs_t p = NULL;
73 p = xbt_new0(s_mc_reached_pairs_t, 1);
75 p->automaton_state = as;
76 char *hash = malloc(sizeof(char)*128);
77 xbt_sha((char *)&p, hash);
78 //XBT_DEBUG("Hash : %s", hash);
79 xbt_dynar_foreach(reached_pairs, c, hash_reached){
80 if(strcmp(hash, hash_reached) == 0){
82 //XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached !", gs, as, as->id);
91 void set_pair_reached(mc_state_t gs, xbt_state_t as){
93 //XBT_DEBUG("Set pair (graph=%p, automaton=%p) reached ", gs, as);
94 if(reached(gs, as) == 0){
96 mc_reached_pairs_t p = NULL;
97 p = xbt_new0(s_mc_reached_pairs_t, 1);
99 p->automaton_state = as;
100 char *hash = malloc(sizeof(char)*128) ;
101 xbt_sha((char *)&p, hash);
102 xbt_dynar_push(reached_pairs, &hash);
103 //XBT_DEBUG("New reached pair : graph=%p, automaton=%p(%s)", gs, as, as->id);
109 int visited(mc_state_t gs, xbt_state_t as, int sc){
110 /*unsigned int c = 0;
111 mc_visited_pairs_t p = NULL;
113 int different_process;
115 //XBT_DEBUG("Visited pair length : %lu", xbt_dynar_length(visited_pairs));
118 xbt_dynar_foreach(visited_pairs, c, p){
119 //XBT_DEBUG("Test pair visited");
121 if((p->automaton_state == as) && (p->search_cycle == sc)){
123 for(i=0; i < gs->max_pid; i++){
124 if(gs->proc_status[i].state != p->graph_state->proc_status[i].state){
128 if(different_process==0){
137 //XBT_DEBUG("Test visited pair");
139 char* hash_visited = malloc(sizeof(char)*128);
143 mc_visited_pairs_t p = NULL;
144 p = xbt_new0(s_mc_visited_pairs_t, 1);
146 p->automaton_state = as;
147 char *hash = malloc(sizeof(char)*128);
148 xbt_sha((char *)&p, hash);
149 //XBT_DEBUG("Hash : %s", hash);
150 xbt_dynar_foreach(visited_pairs, c, hash_visited){
151 if(strcmp(hash, hash_visited) == 0){
158 //XBT_DEBUG("End test visited pair");
163 void MC_dfs_init(xbt_automaton_t a){
165 XBT_DEBUG("**************************************************");
166 XBT_DEBUG("DFS init");
167 XBT_DEBUG("**************************************************");
169 mc_pairs_t mc_initial_pair;
170 mc_state_t initial_graph_state;
171 smx_process_t process;
172 mc_snapshot_t init_snapshot;
174 MC_wait_for_requests();
178 init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
180 initial_graph_state = MC_state_pair_new();
181 xbt_swag_foreach(process, simix_global->process_list){
182 if(MC_process_is_enabled(process)){
183 MC_state_interleave_process(initial_graph_state, process);
187 visited_pairs = xbt_dynar_new(sizeof(char *), NULL);
188 reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
190 MC_take_snapshot(init_snapshot);
194 /* unsigned int cursor = 0; */
195 /* xbt_state_t state = NULL; */
196 /* int nb_init_state = 0; */
198 /* xbt_dynar_foreach(a->states, cursor, state){ */
199 /* if(state->type == -1){ */
201 /* MC_SET_RAW_MEM; */
202 /* mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); */
204 /* xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); */
206 /* XBT_DEBUG("**************************************************"); */
207 /* XBT_DEBUG("Initial state=%p ", mc_initial_pair); */
209 /* MC_UNSET_RAW_MEM; */
211 /* set_pair_visited(mc_initial_pair->graph_state, mc_initial_pair->automaton_state, 0); */
213 /* if(nb_init_state == 0) */
214 /* MC_dfs(a, 0, 0); */
216 /* MC_dfs(a, 0, 1); */
218 /* nb_init_state++; */
222 /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
223 -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
225 unsigned int cursor = 0;
226 unsigned int cursor2 = 0;
227 xbt_state_t state = NULL;
229 xbt_transition_t transition_succ;
230 xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
231 mc_pairs_t pair_succ;
233 xbt_dynar_foreach(a->states, cursor, state){
234 if(state->type == -1){
235 xbt_dynar_foreach(state->out, cursor2, transition_succ){
236 res = MC_automaton_evaluate_label(a, transition_succ->label);
238 if((res == 1) || (res == 2)){
242 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
243 xbt_dynar_push(successors, &mc_initial_pair);
254 if(xbt_dynar_length(successors) == 0){
255 xbt_dynar_foreach(a->states, cursor, state){
256 if(state->type == -1){
259 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
260 xbt_dynar_push(successors, &mc_initial_pair);
268 xbt_dynar_foreach(successors, cursor, pair_succ){
271 xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
272 set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
283 void MC_dfs(xbt_automaton_t a, int search_cycle){
285 smx_process_t process = NULL;
288 if(xbt_fifo_size(mc_snapshot_stack) == 0)
293 /* Get current state */
294 mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
297 XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
298 XBT_DEBUG("State : 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;
308 mc_pairs_t pair_succ;
309 xbt_transition_t transition_succ;
312 //int enabled_transition = 0;
314 xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
316 mc_pairs_t next_pair;
317 mc_snapshot_t next_snapshot;
318 mc_snapshot_t current_snapshot;
321 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
324 current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
325 MC_take_snapshot(current_snapshot);
329 /* Debug information */
330 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
331 req_str = MC_request_to_string(req, value);
332 XBT_DEBUG("Execute: %s", req_str);
336 MC_state_set_executed_request(current_pair->graph_state, req, value);
338 /* Answer the request */
339 SIMIX_request_pre(req, value);
341 /* Wait for requests (schedules processes) */
342 MC_wait_for_requests();
345 /* Create the new expanded graph_state */
348 next_graph_state = MC_state_pair_new();
350 /* Get enabled process and insert it in the interleave set of the next graph_state */
351 xbt_swag_foreach(process, simix_global->process_list){
352 if(MC_process_is_enabled(process)){
353 MC_state_interleave_process(next_graph_state, process);
357 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
358 MC_take_snapshot(next_snapshot);
362 xbt_dynar_reset(successors);
365 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
367 res = MC_automaton_evaluate_label(a, transition_succ->label);
371 if((res == 1) || (res == 2)){ // enabled transition in automaton
372 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
373 xbt_dynar_push(successors, &next_pair);
380 if(xbt_dynar_length(successors) == 0){
383 next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
384 xbt_dynar_push(successors, &next_pair);
391 xbt_dynar_foreach(successors, cursor, pair_succ){
393 //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
395 if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
396 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
397 XBT_INFO("| ACCEPTANCE CYCLE |");
398 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
399 XBT_INFO("Counter-example that violates formula :");
400 MC_show_snapshot_stack(mc_snapshot_stack);
401 MC_dump_snapshot_stack(mc_snapshot_stack);
402 MC_print_statistics_pairs(mc_stats_pair);
406 if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
408 //XBT_DEBUG("Unvisited pair !");
410 mc_stats_pair->executed_transitions++;
413 xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
414 set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
417 MC_dfs(a, search_cycle);
419 if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
421 MC_restore_snapshot(current_pair->system_state);
424 /*xbt_swag_foreach(process, simix_global->process_list){
425 if(MC_process_is_enabled(process)){
426 //XBT_DEBUG("Pid : %lu", process->pid);
427 MC_state_interleave_process(current_pair->graph_state, process);
431 set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
432 XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
440 if(MC_state_interleave_size(current_pair->graph_state) > 0){
441 MC_restore_snapshot(current_snapshot);
443 //XBT_DEBUG("Snapshot restored");
449 //remove_pair_reached(current_pair->graph_state);
450 xbt_fifo_shift(mc_snapshot_stack);
451 XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
456 void MC_show_snapshot_stack(xbt_fifo_t stack){
459 xbt_fifo_item_t item;
461 char *req_str = NULL;
463 for (item = xbt_fifo_get_last_item(stack);
464 (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
465 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
466 req = MC_state_get_executed_request(pair->graph_state, &value);
468 req_str = MC_request_to_string(req, value);
469 XBT_INFO("%s", req_str);
475 void MC_dump_snapshot_stack(xbt_fifo_t stack){
479 while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
480 MC_pair_delete(pair);
484 void MC_pair_delete(mc_pairs_t pair){
485 xbt_free(pair->graph_state->proc_status);
486 xbt_free(pair->graph_state);
487 //xbt_free(pair->automaton_state); -> FIXME : à implémenter
492 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
496 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
497 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
498 return (left_res || right_res);
502 int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
503 int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
504 return (left_res && right_res);
508 int res = MC_automaton_evaluate_label(a, l->u.exp_not);
513 unsigned int cursor = 0;
514 xbt_propositional_symbol_t p = NULL;
515 xbt_dynar_foreach(a->propositional_symbols, cursor, p){
516 if(strcmp(p->pred, l->u.predicat) == 0){
517 int (*f)() = p->function;
534 /********************* Double DFS using color pair *********************/
541 /********************* DPOR without replay *********************/
545 void MC_dpor_with_restore_snapshot_init(xbt_automaton_t a){
547 XBT_DEBUG("**************************************************");
548 XBT_DEBUG("DPOR (with restore snapshot) init");
549 XBT_DEBUG("**************************************************");
551 mc_pairs_t initial_pair;
552 mc_state_t initial_graph_state;
553 smx_process_t process;
554 mc_snapshot_t initial_snapshot;
556 MC_wait_for_requests();
560 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
562 initial_graph_state = MC_state_pair_new();
563 xbt_swag_foreach(process, simix_global->process_list){
564 if(MC_process_is_enabled(process)){
565 MC_state_interleave_process(initial_graph_state, process);
570 visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL);
571 reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL);
573 MC_take_snapshot(initial_snapshot);
577 unsigned int cursor = 0;
578 unsigned int cursor2 = 0;
579 xbt_state_t state = NULL;
581 xbt_transition_t transition_succ;
583 xbt_dynar_foreach(a->states, cursor, state){
584 if(state->type == -1){
585 xbt_dynar_foreach(state->out, cursor2, transition_succ){
586 res = MC_automaton_evaluate_label(a, transition_succ->label);
588 if((res == 1) || (res == 2)){
592 initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst);
593 xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
597 /* Add pair to list of visited pairs*/
598 set_pair_visited(initial_pair->graph_state, initial_pair->automaton_state, 0);
600 MC_dpor_with_restore_snapshot(a, 0, 0);
608 if(xbt_fifo_size(mc_snapshot_stack)>0)
612 /* Initial state of automaton is initial state for initial pair*/
613 if(xbt_fifo_size(mc_snapshot_stack) == 0){
617 xbt_dynar_foreach(a->states, cursor, state){
618 if(state->type == -1){
622 initial_pair = new_pair(initial_snapshot, initial_graph_state, state);
623 xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
627 /* Add pair to list of visited pairs*/
628 set_pair_visited(initial_pair->graph_state, initial_pair->automaton_state, 0);
630 MC_dpor_with_restore_snapshot(a, 0, 0);
641 /* Test du dpor sans rejeu des états de la pile à partir de l'état initial du système mais avec restauration au milieu de l'arbre -> s'applique aux safety properties mais pas d'intégration pour les liveness */
642 void MC_dpor_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
644 smx_process_t process = NULL;
646 if(xbt_fifo_size(mc_snapshot_stack) == 0)
650 mc_state_t next_graph_state = NULL;
651 smx_req_t req = NULL, prev_req = NULL;
653 xbt_fifo_item_t item = NULL;
655 xbt_transition_t transition_succ;
659 mc_pairs_t next_pair;
660 mc_snapshot_t next_snapshot;
661 mc_snapshot_t current_snapshot;
662 mc_pairs_t current_pair;
663 mc_pairs_t prev_pair;
664 int new_pair_created;
666 while(xbt_fifo_size(mc_snapshot_stack) > 0){
668 current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
671 XBT_DEBUG("**************************************************");
672 XBT_DEBUG("Depth : %d, State : g=%p, a=%p(%s), %u interleave", xbt_fifo_size(mc_snapshot_stack),current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
674 mc_stats_pair->visited_pairs++;
676 /* Add pair to list of visited pairs*/
677 set_pair_visited(current_pair->graph_state, current_pair->automaton_state, search_cycle);
679 if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_pair->graph_state, &value))){
682 current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
683 MC_take_snapshot(current_snapshot);
686 /* Debug information */
687 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
688 req_str = MC_request_to_string(req, value);
689 XBT_DEBUG("Execute: %s", req_str);
693 MC_state_set_executed_request(current_pair->graph_state, req, value);
695 /* Answer the request */
696 SIMIX_request_pre(req, value);
698 /* Wait for requests (schedules processes) */
699 MC_wait_for_requests();
701 /* Create the new expanded graph_state */
704 next_graph_state = MC_state_pair_new();
706 /* Get an enabled process and insert it in the interleave set of the next graph_state */
707 xbt_swag_foreach(process, simix_global->process_list){
708 if(MC_process_is_enabled(process)){
709 MC_state_interleave_process(next_graph_state, process);
714 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
715 MC_take_snapshot(next_snapshot);
719 new_pair_created = 0;
722 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
723 res = MC_automaton_evaluate_label(a, transition_succ->label);
725 if((res == 1) || (res == 2)){
728 next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
729 xbt_fifo_unshift(mc_snapshot_stack, next_pair);
732 new_pair_created = 1;
739 /* Pas d'avancement possible dans l'automate */
740 if(new_pair_created == 0){
743 next_pair = new_pair(next_snapshot,next_graph_state,current_pair->automaton_state);
744 xbt_fifo_unshift(mc_snapshot_stack, next_pair);
750 XBT_DEBUG("There are no more processes to interleave.");
752 /* Trash the current state, no longer needed */
754 xbt_fifo_shift(mc_snapshot_stack);
757 while((current_pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
758 req = MC_state_get_internal_request(current_pair->graph_state);
759 xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pairs_t) {
760 if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
761 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
762 XBT_DEBUG("Dependent Transitions:");
763 prev_req = MC_state_get_executed_request(prev_pair->graph_state, &value);
764 req_str = MC_request_to_string(prev_req, value);
765 XBT_DEBUG("%s (state=%p)", req_str, prev_pair->graph_state);
767 prev_req = MC_state_get_executed_request(current_pair->graph_state, &value);
768 req_str = MC_request_to_string(prev_req, value);
769 XBT_DEBUG("%s (state=%p)", req_str, current_pair->graph_state);
773 if(!MC_state_process_is_done(prev_pair->graph_state, req->issuer)){
774 MC_state_interleave_process(prev_pair->graph_state, req->issuer);
777 XBT_DEBUG("Process %p is in done set", req->issuer);
784 if(MC_state_interleave_size(current_pair->graph_state)){
785 MC_restore_snapshot(current_pair->system_state);
786 xbt_fifo_unshift(mc_snapshot_stack, current_pair);
787 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));