Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
f7cf92d4bcecccc85b39011a5b8c64074b83e27e
[simgrid.git] / src / mc / mc_liveness.c
1 #include "private.h"
2 #include "unistd.h"
3
4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
5                                 "Logging specific to algorithms for liveness properties verification");
6
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;
12
13
14 /* fast implementation of djb2 algorithm */
15 unsigned int hash_region(char *str, int str_len){
16
17   int c;
18   register unsigned int hash = 5381;
19
20   while (str_len--) {
21     c = *str++;
22     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
23   }
24
25   return hash;
26
27 }
28
29 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
30
31   
32   if(s1->num_reg != s2->num_reg){
33     //XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
34     return 1;
35   }
36
37   int i;
38
39   for(i=0 ; i< s1->num_reg ; i++){
40
41     if(s1->regions[i]->type != s2->regions[i]->type){
42       //XBT_DEBUG("Different type of region");
43       return 1;
44     }
45
46     switch(s1->regions[i]->type){
47     case 0:
48       if(s1->regions[i]->size != s2->regions[i]->size){
49         //XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
50         return 1;
51       }
52       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
53         //XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
54         return 1;
55       }
56       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
57         //XBT_DEBUG("Different heap (mmalloc_compare)");
58         return 1; 
59       }
60       break;
61     case 1 :
62       if(s1->regions[i]->size != s2->regions[i]->size){
63         //XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
64         return 1;
65       }
66       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
67         //XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
68         return 1;
69       }
70       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
71         //XBT_DEBUG("Different memcmp for data in libsimgrid");
72         return 1;
73       }
74       break;
75     case 2:
76       if(s1->regions[i]->size != s2->regions[i]->size){
77         //XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
78         return 1;
79       }
80       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
81         //XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
82         return 1;
83       }
84       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
85         //XBT_DEBUG("Different memcmp for data in program");
86         return 1;
87       }
88       break;
89     case 3:
90       if(s1->regions[i]->size != s2->regions[i]->size){
91         //XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
92         return 1;
93       }
94       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
95         //XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
96         return 1;
97       }
98       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
99         //XBT_DEBUG("Different memcmp for data in stack");
100         return 1;
101       }
102       break;
103     }
104   }
105
106   return 0;
107   
108 }
109
110 int reached(xbt_state_t st){
111
112
113   if(xbt_dynar_is_empty(reached_pairs)){
114
115     return 0;
116
117   }else{
118
119     MC_SET_RAW_MEM;
120
121     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
122     MC_take_snapshot_liveness(sn);    
123     
124     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
125     int res;
126     int (*f)();
127
128     /* Get values of propositional symbols */
129     unsigned int cursor = 0;
130     xbt_propositional_symbol_t ps = NULL;
131     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
132       f = ps->function;
133       res = (*f)();
134       xbt_dynar_push_as(prop_ato, int, res);
135     }
136
137     cursor = 0;
138     mc_pair_reached_t pair_test = NULL;
139
140
141     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
142       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
143         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
144           if(snapshot_compare(pair_test->system_state, sn) == 0){
145             MC_free_snapshot(sn);
146             xbt_dynar_reset(prop_ato);
147             xbt_free(prop_ato);
148             MC_UNSET_RAW_MEM;
149             return 1;
150           }
151         }
152       }
153     }
154
155     MC_free_snapshot(sn);
156     xbt_dynar_reset(prop_ato);
157     xbt_free(prop_ato);
158     MC_UNSET_RAW_MEM;
159     return 0;
160     
161   }
162 }
163
164 void set_pair_reached(xbt_state_t st){
165
166  
167   MC_SET_RAW_MEM;
168   
169   mc_pair_reached_t pair = NULL;
170   pair = xbt_new0(s_mc_pair_reached_t, 1);
171   pair->automaton_state = st;
172   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
173   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
174   MC_take_snapshot_liveness(pair->system_state);
175
176   /* Get values of propositional symbols */
177   unsigned int cursor = 0;
178   xbt_propositional_symbol_t ps = NULL;
179   int res;
180   int (*f)(); 
181
182   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
183     f = ps->function;
184     res = (*f)();
185     xbt_dynar_push_as(pair->prop_ato, int, res);
186   }
187   
188   xbt_dynar_push(reached_pairs, &pair); 
189
190   MC_UNSET_RAW_MEM;
191   
192 }
193
194 int reached_hash(xbt_state_t st){
195
196
197   if(xbt_dynar_is_empty(reached_pairs_hash)){
198
199     return 0;
200
201   }else{
202
203     MC_SET_RAW_MEM;
204
205     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
206     MC_take_snapshot_liveness(sn);
207
208     int j;
209     unsigned int hash_regions[sn->num_reg];
210     for(j=0; j<sn->num_reg; j++){
211       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
212     }
213
214
215     /* Get values of propositional symbols */
216     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
217     unsigned int cursor = 0;
218     xbt_propositional_symbol_t ps = NULL;
219     int res;
220     int (*f)();
221
222     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
223       f = ps->function;
224       res = (*f)();
225       xbt_dynar_push_as(prop_ato, int, res);
226     }
227
228     mc_pair_reached_hash_t pair_test = NULL;
229
230     int region_diff = 0;
231
232     cursor = 0;
233
234     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
235
236       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
237         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
238           for(j=0 ; j< sn->num_reg ; j++){
239             if(hash_regions[j] != pair_test->hash_regions[j]){
240               region_diff++;
241             }
242           }
243           if(region_diff == 0){
244             MC_free_snapshot(sn);
245             xbt_dynar_reset(prop_ato);
246             xbt_free(prop_ato);
247             MC_UNSET_RAW_MEM;
248             return 1;
249           }
250         }
251       }
252       
253      
254       region_diff = 0;
255     }
256     
257     MC_free_snapshot(sn);
258     xbt_dynar_reset(prop_ato);
259     xbt_free(prop_ato);
260     MC_UNSET_RAW_MEM;
261     return 0;
262     
263   }
264 }
265
266 void set_pair_reached_hash(xbt_state_t st){
267  
268   MC_SET_RAW_MEM;
269
270   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
271   MC_take_snapshot_liveness(sn);
272  
273   mc_pair_reached_hash_t pair = NULL;
274   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
275   pair->automaton_state = st;
276   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
277   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
278   
279   int i;
280
281   for(i=0 ; i< sn->num_reg ; i++){
282     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
283   }
284   
285   /* Get values of propositional symbols */
286   unsigned int cursor = 0;
287   xbt_propositional_symbol_t ps = NULL;
288   int res;
289   int (*f)();
290
291   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
292     f = ps->function;
293     res = (*f)();
294     xbt_dynar_push_as(pair->prop_ato, int, res);
295   }
296   
297   xbt_dynar_push(reached_pairs_hash, &pair);
298
299   MC_free_snapshot(sn);
300   
301   MC_UNSET_RAW_MEM;
302     
303 }
304
305
306 int visited(xbt_state_t st, int sc){
307
308
309   if(xbt_dynar_is_empty(visited_pairs)){
310
311     return 0;
312
313   }else{
314
315     MC_SET_RAW_MEM;
316
317     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
318     MC_take_snapshot_liveness(sn);
319
320     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
321
322     /* Get values of propositional symbols */
323     unsigned int cursor = 0;
324     xbt_propositional_symbol_t ps = NULL;
325     int res;
326     int (*f)();
327
328     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
329       f = ps->function;
330       res = (*f)();
331       xbt_dynar_push_as(prop_ato, int, res);
332     }
333
334     cursor = 0;
335     mc_pair_visited_t pair_test = NULL;
336
337     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
338       if(pair_test->search_cycle == sc) {
339         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
340           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
341             if(snapshot_compare(pair_test->system_state, sn) == 0){
342             
343               MC_free_snapshot(sn);
344               xbt_dynar_reset(prop_ato);
345               xbt_free(prop_ato);
346               MC_UNSET_RAW_MEM;
347                 
348               return 1;
349         
350             }
351           }
352         }
353       }
354     }
355
356
357     MC_free_snapshot(sn);
358     xbt_dynar_reset(prop_ato);
359     xbt_free(prop_ato);
360     MC_UNSET_RAW_MEM;
361     return 0;
362     
363   }
364 }
365
366
367 int visited_hash(xbt_state_t st, int sc){
368
369
370   if(xbt_dynar_is_empty(visited_pairs_hash)){
371
372     return 0;
373
374   }else{
375
376     MC_SET_RAW_MEM;
377
378     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
379     MC_take_snapshot_liveness(sn);
380
381     int j;
382     unsigned int hash_regions[sn->num_reg];
383     for(j=0; j<sn->num_reg; j++){
384       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
385     }
386
387     
388     /* Get values of propositional symbols */
389     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
390     unsigned int cursor = 0;
391     xbt_propositional_symbol_t ps = NULL;
392     int res;
393     int (*f)();
394
395     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
396       f = ps->function;
397       res = (*f)();
398       xbt_dynar_push_as(prop_ato, int, res);
399     }
400
401     mc_pair_visited_hash_t pair_test = NULL;
402
403     int region_diff = 0;
404     cursor = 0;
405
406     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
407   
408       if(pair_test->search_cycle == sc) {
409         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
410           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
411             for(j=0 ; j< sn->num_reg ; j++){
412               if(hash_regions[j] != pair_test->hash_regions[j]){
413                 region_diff++;
414               }
415             }
416             if(region_diff == 0){
417               MC_free_snapshot(sn);
418               xbt_dynar_reset(prop_ato);
419               xbt_free(prop_ato);
420               MC_UNSET_RAW_MEM;
421               return 1;
422             }
423           }
424         }
425       }
426      
427       region_diff = 0;
428     }
429     
430     MC_free_snapshot(sn);
431     xbt_dynar_reset(prop_ato);
432     xbt_free(prop_ato);
433     MC_UNSET_RAW_MEM;
434     return 0;
435     
436   }
437 }
438
439 void set_pair_visited_hash(xbt_state_t st, int sc){
440  
441   MC_SET_RAW_MEM;
442
443   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
444   MC_take_snapshot_liveness(sn);
445  
446   mc_pair_visited_hash_t pair = NULL;
447   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
448   pair->automaton_state = st;
449   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
450   pair->search_cycle = sc;
451   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
452   
453   int i;
454
455   for(i=0 ; i< sn->num_reg ; i++){
456     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
457   }
458   
459   /* Get values of propositional symbols */
460   unsigned int cursor = 0;
461   xbt_propositional_symbol_t ps = NULL;
462   int res;
463   int (*f)();
464
465   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
466     f = ps->function;
467     res = (*f)();
468     xbt_dynar_push_as(pair->prop_ato, int, res);
469   }
470   
471   xbt_dynar_push(visited_pairs_hash, &pair);
472
473   MC_free_snapshot(sn);
474   
475   MC_UNSET_RAW_MEM;
476     
477 }
478
479 void set_pair_visited(xbt_state_t st, int sc){
480
481  
482   MC_SET_RAW_MEM;
483  
484   mc_pair_visited_t pair = NULL;
485   pair = xbt_new0(s_mc_pair_visited_t, 1);
486   pair->automaton_state = st;
487   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
488   pair->search_cycle = sc;
489   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
490   MC_take_snapshot_liveness(pair->system_state);
491
492
493   /* Get values of propositional symbols */
494   unsigned int cursor = 0;
495   xbt_propositional_symbol_t ps = NULL;
496   int res;
497   int (*f)();
498
499   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
500     f = ps->function;
501     res = (*f)();
502     xbt_dynar_push_as(pair->prop_ato, int, res);
503   }
504   
505   xbt_dynar_push(visited_pairs, &pair);
506   
507   MC_UNSET_RAW_MEM;
508   
509   
510 }
511
512 void MC_pair_delete(mc_pair_t pair){
513   xbt_free(pair->graph_state->proc_status);
514   xbt_free(pair->graph_state);
515   xbt_free(pair);
516 }
517
518
519
520 int MC_automaton_evaluate_label(xbt_exp_label_t l){
521   
522   switch(l->type){
523   case 0 : {
524     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
525     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
526     return (left_res || right_res);
527     break;
528   }
529   case 1 : {
530     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
531     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
532     return (left_res && right_res);
533     break;
534   }
535   case 2 : {
536     int res = MC_automaton_evaluate_label(l->u.exp_not);
537     return (!res);
538     break;
539   }
540   case 3 : { 
541     unsigned int cursor = 0;
542     xbt_propositional_symbol_t p = NULL;
543     int (*f)();
544     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
545       if(strcmp(p->pred, l->u.predicat) == 0){
546         f = p->function;
547         return (*f)();
548       }
549     }
550     return -1;
551     break;
552   }
553   case 4 : {
554     return 2;
555     break;
556   }
557   default : 
558     return -1;
559   }
560 }
561
562
563
564
565
566 /********************* Double-DFS stateless *******************/
567
568 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
569   xbt_free(pair->graph_state->proc_status);
570   xbt_free(pair->graph_state);
571   xbt_free(pair);
572 }
573
574 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
575   mc_pair_stateless_t p = NULL;
576   p = xbt_new0(s_mc_pair_stateless_t, 1);
577   p->automaton_state = st;
578   p->graph_state = sg;
579   p->requests = r;
580   mc_stats_pair->expanded_pairs++;
581   return p;
582 }
583
584 void MC_ddfs_init(){
585
586   XBT_DEBUG("**************************************************");
587   XBT_DEBUG("Double-DFS init");
588   XBT_DEBUG("**************************************************");
589
590   mc_pair_stateless_t mc_initial_pair = NULL;
591   mc_state_t initial_graph_state = NULL;
592   smx_process_t process; 
593  
594   MC_wait_for_requests();
595
596   MC_SET_RAW_MEM;
597
598   initial_graph_state = MC_state_pair_new();
599   xbt_swag_foreach(process, simix_global->process_list){
600     if(MC_process_is_enabled(process)){
601       MC_state_interleave_process(initial_graph_state, process);
602     }
603   }
604
605   //reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
606   reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
607   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
608   visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
609   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
610
611   /* Save the initial state */
612   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
613   MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
614
615   MC_UNSET_RAW_MEM; 
616
617   unsigned int cursor = 0;
618   xbt_state_t state;
619
620   xbt_dynar_foreach(automaton->states, cursor, state){
621     if(state->type == -1){
622       
623       MC_SET_RAW_MEM;
624       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
625       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
626       MC_UNSET_RAW_MEM;
627       
628       if(cursor != 0){
629         MC_restore_snapshot(initial_snapshot_liveness);
630         MC_UNSET_RAW_MEM;
631       }
632
633       MC_ddfs(0);
634
635     }else{
636       if(state->type == 2){
637       
638         MC_SET_RAW_MEM;
639         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
640         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
641         MC_UNSET_RAW_MEM;
642
643         //set_pair_reached(state);
644         set_pair_reached_hash(state);
645
646         if(cursor != 0){
647           MC_restore_snapshot(initial_snapshot_liveness);
648           MC_UNSET_RAW_MEM;
649         }
650         
651         MC_ddfs(1);
652         
653       }
654     }
655   } 
656
657 }
658
659
660 void MC_ddfs(int search_cycle){
661
662   smx_process_t process;
663   mc_pair_stateless_t current_pair = NULL;
664
665   if(xbt_fifo_size(mc_stack_liveness) == 0)
666     return;
667
668
669   /* Get current pair */
670   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
671
672   /* Update current state in buchi automaton */
673   automaton->current_state = current_pair->automaton_state;
674
675  
676   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
677   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));
678  
679   mc_stats_pair->visited_pairs++;
680
681   //sleep(1);
682
683   int value;
684   mc_state_t next_graph_state = NULL;
685   smx_req_t req = NULL;
686   char *req_str;
687
688   xbt_transition_t transition_succ;
689   unsigned int cursor = 0;
690   int res;
691
692   mc_pair_stateless_t next_pair = NULL;
693   mc_pair_stateless_t pair_succ;
694
695   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
696
697     //set_pair_visited(current_pair->automaton_state, search_cycle);
698     set_pair_visited_hash(current_pair->automaton_state, search_cycle);
699
700     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
701     XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
702
703     if(current_pair->requests > 0){
704
705       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
706    
707         /* Debug information */
708         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
709           req_str = MC_request_to_string(req, value);
710           XBT_DEBUG("Execute: %s", req_str);
711           xbt_free(req_str);
712         }
713
714         MC_state_set_executed_request(current_pair->graph_state, req, value);   
715     
716         /* Answer the request */
717         SIMIX_request_pre(req, value);
718
719         /* Wait for requests (schedules processes) */
720         MC_wait_for_requests();
721
722
723         MC_SET_RAW_MEM;
724
725         /* Create the new expanded graph_state */
726         next_graph_state = MC_state_pair_new();
727
728         /* Get enabled process and insert it in the interleave set of the next graph_state */
729         xbt_swag_foreach(process, simix_global->process_list){
730           if(MC_process_is_enabled(process)){
731             MC_state_interleave_process(next_graph_state, process);
732           }
733         }
734
735         xbt_dynar_reset(successors);
736
737         MC_UNSET_RAW_MEM;
738
739
740         cursor= 0;
741         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
742
743           res = MC_automaton_evaluate_label(transition_succ->label);
744
745           if(res == 1){ // enabled transition in automaton
746             MC_SET_RAW_MEM;
747             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
748             xbt_dynar_push(successors, &next_pair);
749             MC_UNSET_RAW_MEM;
750           }
751
752         }
753
754         cursor = 0;
755    
756         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
757       
758           res = MC_automaton_evaluate_label(transition_succ->label);
759         
760           if(res == 2){ // true transition in automaton
761             MC_SET_RAW_MEM;
762             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
763             xbt_dynar_push(successors, &next_pair);
764             MC_UNSET_RAW_MEM;
765           }
766
767         }
768
769         cursor = 0; 
770         
771         xbt_dynar_foreach(successors, cursor, pair_succ){
772
773           if(search_cycle == 1){
774
775             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
776                       
777               //if(reached(pair_succ->automaton_state)){
778               if(reached_hash(pair_succ->automaton_state)){
779               
780                 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));
781
782                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
783                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
784                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
785                 XBT_INFO("Counter-example that violates formula :");
786                 MC_show_stack_liveness(mc_stack_liveness);
787                 MC_dump_stack_liveness(mc_stack_liveness);
788                 MC_print_statistics_pairs(mc_stats_pair);
789                 exit(0);
790
791               }else{
792
793                 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);
794               
795                 //set_pair_reached(pair_succ->automaton_state);
796                 set_pair_reached_hash(pair_succ->automaton_state);
797
798                 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
799                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
800
801                 MC_SET_RAW_MEM;
802                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
803                 MC_UNSET_RAW_MEM;
804                 
805                 MC_ddfs(search_cycle);
806
807               }
808
809             }else{
810
811               if(!visited_hash(pair_succ->automaton_state, search_cycle)){
812                 //if(!visited(pair_succ->automaton_state, search_cycle)){
813                 
814                 MC_SET_RAW_MEM;
815                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
816                 MC_UNSET_RAW_MEM;
817                 
818                 MC_ddfs(search_cycle);
819                 
820               }else{
821
822                 XBT_DEBUG("Next pair already visited ! ");
823
824               }
825               
826             }
827
828           }else{
829           
830             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
831
832               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);
833             
834               //set_pair_reached(pair_succ->automaton_state); 
835               set_pair_reached_hash(pair_succ->automaton_state);
836
837               search_cycle = 1;
838
839               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
840               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
841
842             }
843
844             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
845               //if(!visited(pair_succ->automaton_state, search_cycle)){
846               
847               MC_SET_RAW_MEM;
848               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
849               MC_UNSET_RAW_MEM;
850               
851               MC_ddfs(search_cycle);
852               
853             }else{
854
855               XBT_DEBUG("Next pair already visited ! ");
856
857             }
858
859           }
860
861          
862           /* Restore system before checking others successors */
863           if(cursor != (xbt_dynar_length(successors) - 1))
864             MC_replay_liveness(mc_stack_liveness, 1);
865         
866           
867         }
868
869         if(MC_state_interleave_size(current_pair->graph_state) > 0){
870           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
871           MC_replay_liveness(mc_stack_liveness, 0);
872         }
873       }
874
875  
876     }else{  /*No request to execute, search evolution in B├╝chi automaton */
877
878       MC_SET_RAW_MEM;
879
880       /* Create the new expanded graph_state */
881       next_graph_state = MC_state_pair_new();
882
883       xbt_dynar_reset(successors);
884
885       MC_UNSET_RAW_MEM;
886
887
888       cursor= 0;
889       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
890
891         res = MC_automaton_evaluate_label(transition_succ->label);
892
893         if(res == 1){ // enabled transition in automaton
894           MC_SET_RAW_MEM;
895           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
896           xbt_dynar_push(successors, &next_pair);
897           MC_UNSET_RAW_MEM;
898         }
899
900       }
901
902       cursor = 0;
903    
904       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
905       
906         res = MC_automaton_evaluate_label(transition_succ->label);
907         
908         if(res == 2){ // true transition in automaton
909           MC_SET_RAW_MEM;
910           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
911           xbt_dynar_push(successors, &next_pair);
912           MC_UNSET_RAW_MEM;
913         }
914
915       }
916
917       cursor = 0; 
918      
919       xbt_dynar_foreach(successors, cursor, pair_succ){
920
921         if(search_cycle == 1){
922
923           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
924
925             //if(reached(pair_succ->automaton_state)){
926             if(reached_hash(pair_succ->automaton_state)){
927
928               XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
929
930               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
931               XBT_INFO("|             ACCEPTANCE CYCLE            |");
932               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
933               XBT_INFO("Counter-example that violates formula :");
934               MC_show_stack_liveness(mc_stack_liveness);
935               MC_dump_stack_liveness(mc_stack_liveness);
936               MC_print_statistics_pairs(mc_stats_pair);
937               exit(0);
938
939             }else{
940
941               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);
942               
943               //set_pair_reached(pair_succ->automaton_state);
944               set_pair_reached_hash(pair_succ->automaton_state);
945                 
946               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
947               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
948
949               MC_SET_RAW_MEM;
950               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
951               MC_UNSET_RAW_MEM;
952               
953               MC_ddfs(search_cycle);
954
955             }
956
957           }else{
958
959             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
960               //if(!visited(pair_succ->automaton_state, search_cycle)){
961
962               MC_SET_RAW_MEM;
963               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
964               MC_UNSET_RAW_MEM;
965               
966               MC_ddfs(search_cycle);
967               
968             }else{
969
970               XBT_DEBUG("Next pair already visited ! ");
971
972             }
973           }
974             
975
976         }else{
977             
978           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
979
980             //set_pair_reached(pair_succ->automaton_state);
981             set_pair_reached_hash(pair_succ->automaton_state);
982                     
983             search_cycle = 1;
984
985             //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
986             XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
987
988           }
989
990           //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
991           if(!visited(pair_succ->automaton_state, search_cycle)){
992
993             MC_SET_RAW_MEM;
994             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
995             MC_UNSET_RAW_MEM;
996             
997             MC_ddfs(search_cycle);
998             
999           }else{
1000
1001             XBT_DEBUG("Next pair already visited ! ");
1002
1003           }
1004
1005         }
1006
1007         /* Restore system before checking others successors */
1008         if(cursor != xbt_dynar_length(successors) - 1)
1009           MC_replay_liveness(mc_stack_liveness, 1);
1010
1011          
1012       }
1013            
1014     }
1015     
1016   }else{
1017     
1018     XBT_DEBUG("Max depth reached");
1019
1020   }
1021
1022   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1023     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) );
1024   }else{
1025     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) );
1026   }
1027
1028   
1029   MC_SET_RAW_MEM;
1030   xbt_fifo_shift(mc_stack_liveness);
1031   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1032     //xbt_dynar_pop(reached_pairs, NULL);
1033     xbt_dynar_pop(reached_pairs_hash, NULL);
1034   }
1035   MC_UNSET_RAW_MEM;
1036   
1037   
1038
1039 }