Logo AND Algorithmique Numérique Distribuée

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