Logo AND Algorithmique Numérique Distribuée

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