1 #include "mc_private.h"
4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
5 "Logging specific to algorithms for liveness properties verification");
7 xbt_dynar_t reached_pairs;
8 xbt_dynar_t reached_pairs_hash;
9 xbt_dynar_t visited_pairs;
10 xbt_dynar_t visited_pairs_hash;
11 xbt_dynar_t successors;
13 xbt_dynar_t hosts_table;
16 /* fast implementation of djb2 algorithm */
17 unsigned int hash_region(char *str, int str_len){
20 register unsigned int hash = 5381;
24 hash = ((hash << 5) + hash) + c; /* hash * 33 + c */
31 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
34 if(s1->num_reg != s2->num_reg){
35 XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
42 for(i=0 ; i< s1->num_reg ; i++){
44 if(s1->regions[i]->type != s2->regions[i]->type){
45 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
46 XBT_DEBUG("Different type of region");
53 switch(s1->regions[i]->type){
55 if(s1->regions[i]->size != s2->regions[i]->size){
56 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
57 XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
63 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
64 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
65 XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
71 if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data, std_heap)){
72 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
73 XBT_DEBUG("Different heap (mmalloc_compare)");
81 if(s1->regions[i]->size != s2->regions[i]->size){
82 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
83 XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
89 if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
90 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
91 XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
97 if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
98 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
99 XBT_DEBUG("Different memcmp for data in libsimgrid");
100 XBT_DEBUG("Size : %zu", s1->regions[i]->size);
117 int reached(xbt_state_t st){
120 if(xbt_dynar_is_empty(reached_pairs)){
128 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
129 MC_take_snapshot_liveness(sn);
131 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
135 /* Get values of propositional symbols */
136 unsigned int cursor = 0;
137 xbt_propositional_symbol_t ps = NULL;
138 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
141 xbt_dynar_push_as(prop_ato, int, res);
145 mc_pair_reached_t pair_test = NULL;
147 //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points();
149 xbt_dynar_foreach(reached_pairs, cursor, pair_test){
150 XBT_DEBUG("Pair reached #%d", cursor+1);
151 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
152 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
153 //XBT_DEBUG("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
154 //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
155 //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
156 if(snapshot_compare(pair_test->system_state, sn) == 0){
157 MC_free_snapshot(sn);
158 xbt_dynar_reset(prop_ato);
165 XBT_DEBUG("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
168 XBT_DEBUG("Different values of propositional symbols");
171 XBT_DEBUG("Different automaton state");
175 MC_free_snapshot(sn);
176 xbt_dynar_reset(prop_ato);
184 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */
186 xbt_dict_cursor_t cursor_dict = NULL;
189 smx_rdv_t rdv1, rdv2;
190 xbt_fifo_item_t item1, item2;
191 smx_action_t action1, action2;
192 xbt_fifo_item_t item_req1, item_req2;
193 smx_simcall_t req1, req2;
197 xbt_dict_foreach(d1, cursor_dict, key, data){
198 rdv1 = (smx_rdv_t)data;
199 rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
201 XBT_DEBUG("Rdv point unknown");
204 if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
205 XBT_DEBUG("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
209 XBT_DEBUG("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo));
211 item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);
212 item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
214 while(i<xbt_fifo_size(rdv1->comm_fifo)){
215 action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
216 action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
218 if(action1->type != action2->type){
219 XBT_DEBUG("Different type of action");
223 if(action1->state != action2->state){
224 XBT_DEBUG("Different state of action");
228 if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
229 XBT_DEBUG("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
233 item_req1 = xbt_fifo_get_first_item(action1->simcalls);
234 item_req2 = xbt_fifo_get_first_item(action2->simcalls);
236 while(j<xbt_fifo_size(action1->simcalls)){
238 req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
239 req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
241 if(req1->call != req2->call){
242 XBT_DEBUG("Different simcall call in simcalls of action (%d - %d)", req1->call, req2->call);
245 if(req1->issuer->pid != req2->issuer->pid){
246 XBT_DEBUG("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
250 item_req1 = xbt_fifo_get_next_item(item_req1);
251 item_req2 = xbt_fifo_get_next_item(item_req2);
257 switch(action1->type){
258 case 0: /* execution */
259 case 1: /* parallel execution */
260 if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
264 if(action1->comm.type != action2->comm.type)
266 //XBT_DEBUG("Type of comm : %d", action1->comm.type);
268 switch(action1->comm.type){
270 if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
272 if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
275 case 1: /* RECEIVE */
276 if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
278 if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
282 if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
284 if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
286 if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
288 if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
292 if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
294 if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
296 if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
298 if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
302 } /* end of switch on type of comm */
304 if(action1->comm.refcount != action2->comm.refcount)
306 if(action1->comm.detached != action2->comm.detached)
308 if(action1->comm.rate != action2->comm.rate)
310 if(action1->comm.task_size != action2->comm.task_size)
312 if(action1->comm.src_buff != action2->comm.src_buff)
314 if(action1->comm.dst_buff != action2->comm.dst_buff)
316 if(action1->comm.src_data != action2->comm.src_data)
318 if(action1->comm.dst_data != action2->comm.dst_data)
323 if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
326 case 4: /* synchro */
333 item1 = xbt_fifo_get_next_item(item1);
334 item2 = xbt_fifo_get_next_item(item2);
345 void set_pair_reached(xbt_state_t st){
350 mc_pair_reached_t pair = NULL;
351 pair = xbt_new0(s_mc_pair_reached_t, 1);
352 pair->automaton_state = st;
353 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
354 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
355 //pair->rdv_points = xbt_dict_new();
356 MC_take_snapshot_liveness(pair->system_state);
358 /* Get values of propositional symbols */
359 unsigned int cursor = 0;
360 xbt_propositional_symbol_t ps = NULL;
364 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
367 xbt_dynar_push_as(pair->prop_ato, int, res);
370 /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
372 xbt_dict_cursor_t cursor_dict = NULL;
375 xbt_fifo_item_t item;
378 xbt_dict_foreach(rdv_points, cursor_dict, key, data){
379 smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
380 new_rdv->name = strdup(((smx_rdv_t)data)->name);
381 new_rdv->comm_fifo = xbt_fifo_new();
382 xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
383 smx_action_t a = xbt_new0(s_smx_action_t, 1);
384 memcpy(a, action, sizeof(s_smx_action_t));
385 xbt_fifo_push(new_rdv->comm_fifo, a);
386 XBT_DEBUG("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
388 XBT_DEBUG("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
390 //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
391 xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
394 xbt_dynar_push(reached_pairs, &pair);
401 int reached_hash(xbt_state_t st){
404 if(xbt_dynar_is_empty(reached_pairs_hash)){
412 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
413 MC_take_snapshot_liveness(sn);
416 unsigned int hash_regions[sn->num_reg];
417 for(j=0; j<sn->num_reg; j++){
418 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
422 /* Get values of propositional symbols */
423 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
424 unsigned int cursor = 0;
425 xbt_propositional_symbol_t ps = NULL;
429 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
432 xbt_dynar_push_as(prop_ato, int, res);
435 mc_pair_reached_hash_t pair_test = NULL;
441 xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
443 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
444 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
445 for(j=0 ; j< sn->num_reg ; j++){
446 if(hash_regions[j] != pair_test->hash_regions[j]){
450 if(region_diff == 0){
451 MC_free_snapshot(sn);
452 xbt_dynar_reset(prop_ato);
457 XBT_DEBUG("Different snapshot");
460 XBT_DEBUG("Different values of propositional symbols");
463 XBT_DEBUG("Different automaton state");
469 MC_free_snapshot(sn);
470 xbt_dynar_reset(prop_ato);
478 void set_pair_reached_hash(xbt_state_t st){
482 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
483 MC_take_snapshot_liveness(sn);
485 mc_pair_reached_hash_t pair = NULL;
486 pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
487 pair->automaton_state = st;
488 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
489 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
493 for(i=0 ; i< sn->num_reg ; i++){
494 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
497 /* Get values of propositional symbols */
498 unsigned int cursor = 0;
499 xbt_propositional_symbol_t ps = NULL;
503 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
506 xbt_dynar_push_as(pair->prop_ato, int, res);
509 xbt_dynar_push(reached_pairs_hash, &pair);
511 MC_free_snapshot(sn);
518 int visited(xbt_state_t st, int sc){
521 if(xbt_dynar_is_empty(visited_pairs)){
529 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
530 MC_take_snapshot_liveness(sn);
532 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
534 /* Get values of propositional symbols */
535 unsigned int cursor = 0;
536 xbt_propositional_symbol_t ps = NULL;
540 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
543 xbt_dynar_push_as(prop_ato, int, res);
547 mc_pair_visited_t pair_test = NULL;
549 xbt_dynar_foreach(visited_pairs, cursor, pair_test){
550 if(pair_test->search_cycle == sc) {
551 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
552 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
553 if(snapshot_compare(pair_test->system_state, sn) == 0){
555 MC_free_snapshot(sn);
556 xbt_dynar_reset(prop_ato);
563 XBT_DEBUG("Different snapshot");
566 XBT_DEBUG("Different values of propositional symbols");
569 XBT_DEBUG("Different automaton state");
572 XBT_DEBUG("Different value of search_cycle");
577 MC_free_snapshot(sn);
578 xbt_dynar_reset(prop_ato);
587 int visited_hash(xbt_state_t st, int sc){
590 if(xbt_dynar_is_empty(visited_pairs_hash)){
598 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
599 MC_take_snapshot_liveness(sn);
602 unsigned int hash_regions[sn->num_reg];
603 for(j=0; j<sn->num_reg; j++){
604 hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
608 /* Get values of propositional symbols */
609 xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
610 unsigned int cursor = 0;
611 xbt_propositional_symbol_t ps = NULL;
615 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
618 xbt_dynar_push_as(prop_ato, int, res);
621 mc_pair_visited_hash_t pair_test = NULL;
626 xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
628 if(pair_test->search_cycle == sc) {
629 if(automaton_state_compare(pair_test->automaton_state, st) == 0){
630 if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
631 for(j=0 ; j< sn->num_reg ; j++){
632 if(hash_regions[j] != pair_test->hash_regions[j]){
636 if(region_diff == 0){
637 MC_free_snapshot(sn);
638 xbt_dynar_reset(prop_ato);
643 XBT_DEBUG("Different snapshot");
646 XBT_DEBUG("Different values of propositional symbols");
649 XBT_DEBUG("Different automaton state");
652 XBT_DEBUG("Different value of search_cycle");
658 MC_free_snapshot(sn);
659 xbt_dynar_reset(prop_ato);
667 void set_pair_visited_hash(xbt_state_t st, int sc){
671 mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
672 MC_take_snapshot_liveness(sn);
674 mc_pair_visited_hash_t pair = NULL;
675 pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
676 pair->automaton_state = st;
677 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
678 pair->search_cycle = sc;
679 pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
683 for(i=0 ; i< sn->num_reg ; i++){
684 pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
687 /* Get values of propositional symbols */
688 unsigned int cursor = 0;
689 xbt_propositional_symbol_t ps = NULL;
693 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
696 xbt_dynar_push_as(pair->prop_ato, int, res);
699 xbt_dynar_push(visited_pairs_hash, &pair);
701 MC_free_snapshot(sn);
707 void set_pair_visited(xbt_state_t st, int sc){
712 mc_pair_visited_t pair = NULL;
713 pair = xbt_new0(s_mc_pair_visited_t, 1);
714 pair->automaton_state = st;
715 pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
716 pair->search_cycle = sc;
717 pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
718 MC_take_snapshot_liveness(pair->system_state);
721 /* Get values of propositional symbols */
722 unsigned int cursor = 0;
723 xbt_propositional_symbol_t ps = NULL;
727 xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
730 xbt_dynar_push_as(pair->prop_ato, int, res);
733 xbt_dynar_push(visited_pairs, &pair);
740 void MC_pair_delete(mc_pair_t pair){
741 xbt_free(pair->graph_state->proc_status);
742 xbt_free(pair->graph_state);
748 int MC_automaton_evaluate_label(xbt_exp_label_t l){
752 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
753 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
754 return (left_res || right_res);
758 int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
759 int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
760 return (left_res && right_res);
764 int res = MC_automaton_evaluate_label(l->u.exp_not);
769 unsigned int cursor = 0;
770 xbt_propositional_symbol_t p = NULL;
772 xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
773 if(strcmp(p->pred, l->u.predicat) == 0){
792 /********************* Double-DFS stateless *******************/
794 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
795 xbt_free(pair->graph_state->proc_status);
796 xbt_free(pair->graph_state);
800 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
801 mc_pair_stateless_t p = NULL;
802 p = xbt_new0(s_mc_pair_stateless_t, 1);
803 p->automaton_state = st;
806 mc_stats_pair->expanded_pairs++;
810 void MC_ddfs_init(void){
812 XBT_DEBUG("**************************************************");
813 XBT_DEBUG("Double-DFS init");
814 XBT_DEBUG("**************************************************");
816 mc_pair_stateless_t mc_initial_pair = NULL;
817 mc_state_t initial_graph_state = NULL;
818 smx_process_t process;
820 MC_wait_for_requests();
824 initial_graph_state = MC_state_pair_new();
825 xbt_swag_foreach(process, simix_global->process_list){
826 if(MC_process_is_enabled(process)){
827 MC_state_interleave_process(initial_graph_state, process);
831 reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
832 //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
833 //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
834 visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
835 successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
837 /* Save the initial state */
838 initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
839 MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
843 unsigned int cursor = 0;
846 xbt_dynar_foreach(automaton->states, cursor, state){
847 if(state->type == -1){
850 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
851 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
855 MC_restore_snapshot(initial_snapshot_liveness);
862 if(state->type == 2){
865 mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
866 xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
869 set_pair_reached(state);
870 //set_pair_reached_hash(state);
873 MC_restore_snapshot(initial_snapshot_liveness);
886 void MC_ddfs(int search_cycle){
888 smx_process_t process;
889 mc_pair_stateless_t current_pair = NULL;
891 if(xbt_fifo_size(mc_stack_liveness) == 0)
895 /* Get current pair */
896 current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
898 /* Update current state in buchi automaton */
899 automaton->current_state = current_pair->automaton_state;
902 XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
903 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));
905 mc_stats_pair->visited_pairs++;
910 mc_state_t next_graph_state = NULL;
911 smx_simcall_t req = NULL;
914 xbt_transition_t transition_succ;
915 unsigned int cursor = 0;
918 mc_pair_stateless_t next_pair = NULL;
919 mc_pair_stateless_t pair_succ;
921 if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
923 //set_pair_visited(current_pair->automaton_state, search_cycle);
924 set_pair_visited_hash(current_pair->automaton_state, search_cycle);
926 //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
927 XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
929 if(current_pair->requests > 0){
931 while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
933 /* Debug information */
934 if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
935 req_str = MC_request_to_string(req, value);
936 XBT_DEBUG("Execute: %s", req_str);
940 MC_state_set_executed_request(current_pair->graph_state, req, value);
942 /* Answer the request */
943 SIMIX_simcall_pre(req, value);
945 /* Wait for requests (schedules processes) */
946 MC_wait_for_requests();
951 /* Create the new expanded graph_state */
952 next_graph_state = MC_state_pair_new();
954 /* Get enabled process and insert it in the interleave set of the next graph_state */
955 xbt_swag_foreach(process, simix_global->process_list){
956 if(MC_process_is_enabled(process)){
957 MC_state_interleave_process(next_graph_state, process);
961 xbt_dynar_reset(successors);
967 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
969 res = MC_automaton_evaluate_label(transition_succ->label);
971 if(res == 1){ // enabled transition in automaton
973 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
974 xbt_dynar_push(successors, &next_pair);
982 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
984 res = MC_automaton_evaluate_label(transition_succ->label);
986 if(res == 2){ // true transition in automaton
988 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
989 xbt_dynar_push(successors, &next_pair);
997 xbt_dynar_foreach(successors, cursor, pair_succ){
999 if(search_cycle == 1){
1001 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1003 if(reached(pair_succ->automaton_state)){
1004 //if(reached_hash(pair_succ->automaton_state)){
1006 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
1008 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1009 XBT_INFO("| ACCEPTANCE CYCLE |");
1010 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1011 XBT_INFO("Counter-example that violates formula :");
1012 MC_show_stack_liveness(mc_stack_liveness);
1013 MC_dump_stack_liveness(mc_stack_liveness);
1014 MC_print_statistics_pairs(mc_stats_pair);
1019 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1021 set_pair_reached(pair_succ->automaton_state);
1022 //set_pair_reached_hash(pair_succ->automaton_state);
1024 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1025 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1028 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1031 MC_ddfs(search_cycle);
1037 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1038 //if(!visited(pair_succ->automaton_state, search_cycle)){
1041 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1044 MC_ddfs(search_cycle);
1048 XBT_DEBUG("Next pair already visited ! ");
1056 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1058 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1060 set_pair_reached(pair_succ->automaton_state);
1061 //set_pair_reached_hash(pair_succ->automaton_state);
1065 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1066 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1070 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1071 //if(!visited(pair_succ->automaton_state, search_cycle)){
1074 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1077 MC_ddfs(search_cycle);
1081 XBT_DEBUG("Next pair already visited ! ");
1088 /* Restore system before checking others successors */
1089 if(cursor != (xbt_dynar_length(successors) - 1))
1090 MC_replay_liveness(mc_stack_liveness, 1);
1095 if(MC_state_interleave_size(current_pair->graph_state) > 0){
1096 XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
1097 MC_replay_liveness(mc_stack_liveness, 0);
1102 }else{ /*No request to execute, search evolution in Büchi automaton */
1106 /* Create the new expanded graph_state */
1107 next_graph_state = MC_state_pair_new();
1109 xbt_dynar_reset(successors);
1115 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1117 res = MC_automaton_evaluate_label(transition_succ->label);
1119 if(res == 1){ // enabled transition in automaton
1121 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1122 xbt_dynar_push(successors, &next_pair);
1130 xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1132 res = MC_automaton_evaluate_label(transition_succ->label);
1134 if(res == 2){ // true transition in automaton
1136 next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1137 xbt_dynar_push(successors, &next_pair);
1145 xbt_dynar_foreach(successors, cursor, pair_succ){
1147 if(search_cycle == 1){
1149 if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1151 if(reached(pair_succ->automaton_state)){
1152 //if(reached_hash(pair_succ->automaton_state)){
1154 XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1156 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1157 XBT_INFO("| ACCEPTANCE CYCLE |");
1158 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1159 XBT_INFO("Counter-example that violates formula :");
1160 MC_show_stack_liveness(mc_stack_liveness);
1161 MC_dump_stack_liveness(mc_stack_liveness);
1162 MC_print_statistics_pairs(mc_stats_pair);
1167 XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1169 set_pair_reached(pair_succ->automaton_state);
1170 //set_pair_reached_hash(pair_succ->automaton_state);
1172 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1173 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1176 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1179 MC_ddfs(search_cycle);
1185 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1186 //if(!visited(pair_succ->automaton_state, search_cycle)){
1189 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1192 MC_ddfs(search_cycle);
1196 XBT_DEBUG("Next pair already visited ! ");
1204 if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1206 set_pair_reached(pair_succ->automaton_state);
1207 //set_pair_reached_hash(pair_succ->automaton_state);
1211 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1212 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1216 if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1217 //if(!visited(pair_succ->automaton_state, search_cycle)){
1220 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1223 MC_ddfs(search_cycle);
1227 XBT_DEBUG("Next pair already visited ! ");
1233 /* Restore system before checking others successors */
1234 if(cursor != xbt_dynar_length(successors) - 1)
1235 MC_replay_liveness(mc_stack_liveness, 1);
1244 XBT_DEBUG("Max depth reached");
1248 if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1249 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1251 XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1256 xbt_fifo_shift(mc_stack_liveness);
1257 if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1258 xbt_dynar_pop(reached_pairs, NULL);
1259 //xbt_dynar_pop(reached_pairs_hash, NULL);