Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : more condition (state with processes interleaved > 0) for detection...
[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 initial_pairs = NULL;
8 xbt_dynar_t reached_pairs;
9 xbt_dynar_t successors = NULL;
10 extern mc_snapshot_t initial_snapshot;
11
12 /* Global variables for stateless algorithm */
13 mc_snapshot_t snapshot = NULL;
14
15 /* Global variables for stateful algorithm */
16 mc_snapshot_t next_snapshot = NULL;
17 mc_snapshot_t current_snapshot = NULL;
18
19
20 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
21   mc_pair_t p = NULL;
22   p = xbt_new0(s_mc_pair_t, 1);
23   p->system_state = sn;
24   p->automaton_state = st;
25   p->graph_state = sg;
26   mc_stats_pair->expanded_pairs++;
27   return p;
28     
29 }
30
31 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
32   
33   if(s1->num_reg != s2->num_reg)
34     return 1;
35
36   int i, errors=0;
37
38   for(i=0 ; i< s1->num_reg ; i++){
39     
40     if(s1->regions[i]->size != s2->regions[i]->size)
41       return 1;
42     
43     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
44       return 1;
45     
46     if(s1->regions[i]->type != s2->regions[i]->type)
47       return 1;
48
49     if(s1->regions[i]->type == 0){ 
50       if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
51         XBT_DEBUG("Different heap (mmalloc_compare)");
52         sleep(1);
53         errors++; 
54       }
55     }else{
56       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
57         XBT_DEBUG("Different memcmp for data in libsimgrid");
58         sleep(1);
59         errors++;
60       }
61     }
62     
63     
64   }
65
66   return (errors>0);
67
68 }
69
70 int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
71
72
73   if(xbt_dynar_is_empty(reached_pairs)){
74     return 0;
75   }else{
76     MC_SET_RAW_MEM;
77     
78     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
79
80     /* Get values of propositional symbols */
81     unsigned int cursor = 0;
82     xbt_propositional_symbol_t ps = NULL;
83     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
84       int (*f)() = ps->function;
85       int res = (*f)();
86       xbt_dynar_push_as(prop_ato, int, res);
87     }
88     
89     cursor = 0;
90     mc_pair_reached_t pair_test;
91
92     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
93       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
94         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
95           if(snapshot_compare(pair_test->system_state, s) == 0){
96             MC_UNSET_RAW_MEM;
97             return 1;
98           }
99         }
100       }
101     }
102
103     MC_UNSET_RAW_MEM;
104     return 0;
105     
106   }
107 }
108
109 void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
110
111  
112   MC_SET_RAW_MEM;
113   
114   mc_pair_reached_t pair = NULL;
115   pair = xbt_new0(s_mc_pair_reached_t, 1);
116   pair->automaton_state = st;
117   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
118   pair->system_state = sn;
119   
120   /* Get values of propositional symbols */
121   unsigned int cursor = 0;
122   xbt_propositional_symbol_t ps = NULL;
123   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
124     int (*f)() = ps->function;
125     int res = (*f)();
126     xbt_dynar_push_as(pair->prop_ato, int, res);
127   }
128   
129   xbt_dynar_push(reached_pairs, &pair); 
130   
131   MC_UNSET_RAW_MEM;
132   
133   
134 }
135
136 void MC_pair_delete(mc_pair_t pair){
137   xbt_free(pair->graph_state->proc_status);
138   xbt_free(pair->graph_state);
139   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
140   xbt_free(pair);
141 }
142
143
144
145 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
146   
147   switch(l->type){
148   case 0 : {
149     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
150     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
151     return (left_res || right_res);
152     break;
153   }
154   case 1 : {
155     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
156     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
157     return (left_res && right_res);
158     break;
159   }
160   case 2 : {
161     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
162     return (!res);
163     break;
164   }
165   case 3 : { 
166     unsigned int cursor = 0;
167     xbt_propositional_symbol_t p = NULL;
168     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
169       if(strcmp(p->pred, l->u.predicat) == 0){
170         int (*f)() = p->function;
171         return (*f)();
172       }
173     }
174     return -1;
175     break;
176   }
177   case 4 : {
178     return 2;
179     break;
180   }
181   default : 
182     return -1;
183   }
184 }
185
186
187
188
189
190 /********************* Double-DFS stateless *******************/
191
192 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
193   xbt_free(pair->graph_state->proc_status);
194   xbt_free(pair->graph_state);
195   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
196   xbt_free(pair);
197 }
198
199 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
200   mc_pair_stateless_t p = NULL;
201   p = xbt_new0(s_mc_pair_stateless_t, 1);
202   p->automaton_state = st;
203   p->graph_state = sg;
204   mc_stats_pair->expanded_pairs++;
205   return p;
206 }
207
208
209
210 void MC_ddfs_stateless_init(xbt_automaton_t a){
211
212   XBT_DEBUG("**************************************************");
213   XBT_DEBUG("Double-DFS stateless init");
214   XBT_DEBUG("**************************************************");
215  
216   mc_pair_stateless_t mc_initial_pair = NULL;
217   mc_state_t initial_graph_state = NULL;
218   smx_process_t process; 
219  
220   MC_wait_for_requests();
221
222   MC_SET_RAW_MEM;
223
224   initial_graph_state = MC_state_pair_new();
225   xbt_swag_foreach(process, simix_global->process_list){
226     if(MC_process_is_enabled(process)){
227       MC_state_interleave_process(initial_graph_state, process);
228     }
229   }
230
231   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
232   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
233   snapshot = xbt_new0(s_mc_snapshot_t, 1);
234
235   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
236   MC_take_snapshot(initial_snapshot);
237
238   MC_UNSET_RAW_MEM; 
239
240   unsigned int cursor = 0;
241   xbt_state_t state;
242
243   xbt_dynar_foreach(a->states, cursor, state){
244     if(state->type == -1){
245       
246       MC_SET_RAW_MEM;
247       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
248       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
249       MC_UNSET_RAW_MEM;
250       
251       if(cursor == 0){
252         MC_ddfs_stateless(a, 0, 0);
253       }else{
254         MC_restore_snapshot(initial_snapshot);
255         MC_UNSET_RAW_MEM;
256         MC_ddfs_stateless(a, 0, 0);
257       }
258     }else{
259       if(state->type == 2){
260       
261         MC_SET_RAW_MEM;
262         mc_initial_pair = new_pair_stateless(initial_graph_state, state);
263         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
264         MC_UNSET_RAW_MEM;
265         
266         if(cursor == 0){
267           MC_ddfs_stateless(a, 1, 0);
268         }else{
269           MC_restore_snapshot(initial_snapshot);
270           MC_UNSET_RAW_MEM;
271           MC_ddfs_stateless(a, 1, 0);
272         }
273       }
274     }
275   } 
276
277 }
278
279
280 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
281
282   smx_process_t process;
283   mc_pair_stateless_t current_pair = NULL;
284
285   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
286     return;
287
288   if(replay == 1){
289     MC_replay_liveness(mc_stack_liveness_stateless);
290     current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
291     xbt_swag_foreach(process, simix_global->process_list){
292       if(MC_process_is_enabled(process)){
293         MC_state_interleave_process(current_pair->graph_state, process);
294       }
295     }
296   }
297
298   /* Get current pair */
299   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
300
301   /* Update current state in buchi automaton */
302   a->current_state = current_pair->automaton_state;
303
304  
305   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
306   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));
307   
308
309   
310   mc_stats_pair->visited_pairs++;
311
312   int value;
313   mc_state_t next_graph_state = NULL;
314   smx_req_t req = NULL;
315   char *req_str;
316
317   xbt_transition_t transition_succ;
318   unsigned int cursor = 0;
319   int res;
320
321   mc_pair_stateless_t next_pair = NULL;
322   mc_pair_stateless_t pair_succ;
323   //mc_snapshot_t next_snapshot = NULL;
324
325   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
326    
327     /* Debug information */
328     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
329       req_str = MC_request_to_string(req, value);
330       XBT_DEBUG("Execute: %s", req_str);
331       xbt_free(req_str);
332     }
333
334     //sleep(1);
335
336     MC_state_set_executed_request(current_pair->graph_state, req, value);   
337     
338     /* Answer the request */
339     SIMIX_request_pre(req, value);
340
341     /* Wait for requests (schedules processes) */
342     MC_wait_for_requests();
343
344
345     MC_SET_RAW_MEM;
346
347     /* Create the new expanded graph_state */
348     next_graph_state = MC_state_pair_new();
349
350     /* Get enabled process and insert it in the interleave set of the next graph_state */
351     xbt_swag_foreach(process, simix_global->process_list){
352       if(MC_process_is_enabled(process)){
353         MC_state_interleave_process(next_graph_state, process);
354       }
355     }
356
357     xbt_dynar_reset(successors);
358
359     MC_UNSET_RAW_MEM;
360
361
362     cursor= 0;
363     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
364
365       res = MC_automaton_evaluate_label(a, transition_succ->label);
366
367       if(res == 1){ // enabled transition in automaton
368         MC_SET_RAW_MEM;
369         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
370         xbt_dynar_push(successors, &next_pair);
371         MC_UNSET_RAW_MEM;
372       }
373
374     }
375
376     cursor = 0;
377    
378     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
379       
380       res = MC_automaton_evaluate_label(a, transition_succ->label);
381         
382       if(res == 2){ // true transition in automaton
383         MC_SET_RAW_MEM;
384         next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
385         xbt_dynar_push(successors, &next_pair);
386         MC_UNSET_RAW_MEM;
387       }
388
389     }
390
391    
392     if(xbt_dynar_length(successors) == 0){
393       MC_SET_RAW_MEM;
394       next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
395       xbt_dynar_push(successors, &next_pair);
396       MC_UNSET_RAW_MEM;
397     }
398
399     cursor = 0; 
400
401     xbt_dynar_foreach(successors, cursor, pair_succ){
402
403      
404
405       if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (MC_state_interleave_size(pair_succ->graph_state) > 0)){
406         
407         //XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
408         
409         MC_SET_RAW_MEM;
410         MC_take_snapshot(snapshot);
411         MC_UNSET_RAW_MEM;
412
413         if(reached(a, pair_succ->automaton_state, snapshot) == 1){
414           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
415           XBT_INFO("|             ACCEPTANCE CYCLE            |");
416           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
417           XBT_INFO("Counter-example that violates formula :");
418           MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
419           MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
420           MC_print_statistics_pairs(mc_stats_pair);
421           exit(1);
422         }
423       }
424       
425       MC_SET_RAW_MEM;
426       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
427       MC_UNSET_RAW_MEM;
428       
429
430       MC_ddfs_stateless(a, search_cycle, 0);
431
432       /* If pair_succ is the last state of the execution (0 interleave), no acceptance cycle possible */
433       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (MC_state_interleave_size(pair_succ->graph_state) > 0)){
434        
435         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
436
437         MC_SET_RAW_MEM;
438         MC_take_snapshot(snapshot);
439         MC_UNSET_RAW_MEM;
440                 
441         set_pair_reached(a, pair_succ->automaton_state, snapshot);
442
443         
444         /* Pair shifted from stack when first MC_ddfs finished and returned at this point */
445         MC_SET_RAW_MEM;
446         xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
447         MC_UNSET_RAW_MEM;
448       
449         MC_ddfs_stateless(a, 1, 1);
450
451         /* No acceptance cycle with this acceptance pair, we remove it from the list reached_pairs */
452         MC_SET_RAW_MEM;
453         xbt_dynar_pop(reached_pairs, NULL);
454         MC_UNSET_RAW_MEM;
455           
456       }
457     }
458
459     if(MC_state_interleave_size(current_pair->graph_state) > 0){
460       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
461       MC_replay_liveness(mc_stack_liveness_stateless);
462     }    
463    
464   }
465   
466   MC_SET_RAW_MEM;
467   xbt_fifo_shift(mc_stack_liveness_stateless);
468   XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
469   MC_UNSET_RAW_MEM;
470
471 }
472
473 /********************* Double-DFS stateful without visited state *******************/
474
475
476 void MC_ddfs_stateful_init(xbt_automaton_t a){
477
478   XBT_DEBUG("**************************************************");
479   XBT_DEBUG("Double-DFS stateful without visited state init");
480   XBT_DEBUG("**************************************************");
481  
482   mc_pair_t mc_initial_pair;
483   mc_state_t initial_graph_state;
484   smx_process_t process; 
485   mc_snapshot_t init_snapshot;
486  
487   MC_wait_for_requests();
488
489   MC_SET_RAW_MEM;
490
491   initial_graph_state = MC_state_pair_new();
492   xbt_swag_foreach(process, simix_global->process_list){
493     if(MC_process_is_enabled(process)){
494       MC_state_interleave_process(initial_graph_state, process);
495     }
496   }
497
498   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
499   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); 
500   current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
501   next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
502   
503   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
504   MC_take_snapshot(init_snapshot);
505
506   MC_UNSET_RAW_MEM; 
507
508   unsigned int cursor = 0;
509   xbt_state_t state = NULL;
510
511   xbt_dynar_foreach(a->states, cursor, state){
512     if(state->type == -1){
513     
514       MC_SET_RAW_MEM;
515       mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
516       xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
517       MC_UNSET_RAW_MEM;
518
519       if(cursor == 0){
520         MC_ddfs_stateful(a, 0, 0);
521       }else{
522         MC_restore_snapshot(init_snapshot);
523         MC_UNSET_RAW_MEM;
524         MC_ddfs_stateful(a, 0, 0);
525       }
526     }else{
527        if(state->type == 2){
528     
529          MC_SET_RAW_MEM;
530          mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
531          xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
532          MC_UNSET_RAW_MEM;
533          
534          if(cursor == 0){
535            MC_ddfs_stateful(a, 1, 0);
536          }else{
537            MC_restore_snapshot(init_snapshot);
538            MC_UNSET_RAW_MEM;
539            MC_ddfs_stateful(a, 1, 0);
540          }
541        }
542     }
543   } 
544 }
545
546
547 void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
548
549   smx_process_t process = NULL;
550   mc_pair_t current_pair = NULL;
551
552   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
553     return;
554
555   if(restore == 1){
556     current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
557     MC_restore_snapshot(current_pair->system_state);
558     xbt_swag_foreach(process, simix_global->process_list){
559       if(MC_process_is_enabled(process)){
560         MC_state_interleave_process(current_pair->graph_state, process);
561       }
562     }
563     MC_UNSET_RAW_MEM;
564   }
565
566   /* Get current state */
567   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
568
569
570   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
571   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));
572
573   a->current_state = current_pair->automaton_state;
574   
575   //sleep(1);
576
577   mc_stats_pair->visited_pairs++;
578
579   int value;
580   mc_state_t next_graph_state = NULL;
581   smx_req_t req = NULL;
582   char *req_str;
583
584   mc_pair_t pair_succ;
585   xbt_transition_t transition_succ;
586   unsigned int cursor;
587   int res;
588
589   mc_pair_t next_pair = NULL;
590   
591   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
592
593     MC_SET_RAW_MEM;
594     MC_take_snapshot(current_snapshot);
595     MC_UNSET_RAW_MEM;
596      
597     /* Debug information */
598     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
599       req_str = MC_request_to_string(req, value);
600       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));
601       XBT_DEBUG("Execute: %s", req_str);
602       xbt_free(req_str);
603     }
604
605     MC_state_set_executed_request(current_pair->graph_state, req, value);
606
607     /* Answer the request */
608     SIMIX_request_pre(req, value);
609
610     /* Wait for requests (schedules processes) */
611     MC_wait_for_requests();
612
613
614     /* Create the new expanded graph_state */
615     MC_SET_RAW_MEM;
616
617     next_graph_state = MC_state_pair_new();
618     
619     /* Get enabled process and insert it in the interleave set of the next graph_state */
620     xbt_swag_foreach(process, simix_global->process_list){
621       if(MC_process_is_enabled(process)){
622         MC_state_interleave_process(next_graph_state, process);
623       }
624     }
625
626     MC_take_snapshot(next_snapshot);
627
628     xbt_dynar_reset(successors);
629
630     MC_UNSET_RAW_MEM;
631
632     
633     cursor = 0;
634     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
635
636       res = MC_automaton_evaluate_label(a, transition_succ->label);
637         
638       if(res == 1){ // enabled transition in automaton
639         MC_SET_RAW_MEM;
640         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
641         xbt_dynar_push(successors, &next_pair);
642         MC_UNSET_RAW_MEM;
643       }
644
645     }
646
647     cursor = 0;
648     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
649
650       res = MC_automaton_evaluate_label(a, transition_succ->label);
651         
652       if(res == 2){ // transition always enabled in automaton
653         MC_SET_RAW_MEM;
654         next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
655         xbt_dynar_push(successors, &next_pair);
656         MC_UNSET_RAW_MEM;
657       }
658
659      
660     }
661
662    
663     if(xbt_dynar_length(successors) == 0){
664
665       MC_SET_RAW_MEM;
666       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
667       xbt_dynar_push(successors, &next_pair);
668       MC_UNSET_RAW_MEM;
669         
670     }
671
672     cursor = 0;
673     xbt_dynar_foreach(successors, cursor, pair_succ){
674
675       if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
676         
677         if(reached(a, pair_succ->automaton_state, next_snapshot) == 1){
678           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
679           XBT_INFO("|             ACCEPTANCE CYCLE            |");
680           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
681           XBT_INFO("Counter-example that violates formula :");
682           MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
683           MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
684           MC_print_statistics_pairs(mc_stats_pair);
685           exit(1);
686         }
687       }
688         
689  
690       MC_SET_RAW_MEM;
691       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
692       MC_UNSET_RAW_MEM;
693
694       MC_ddfs_stateful(a, search_cycle, 0);
695     
696     
697       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
698
699         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
700         set_pair_reached(a, pair_succ->automaton_state, next_snapshot);
701         
702         MC_SET_RAW_MEM;
703         xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
704         MC_UNSET_RAW_MEM;
705         
706         MC_ddfs_stateful(a, 1, 1);
707
708
709         MC_SET_RAW_MEM;
710         xbt_dynar_pop(reached_pairs, NULL);
711         MC_UNSET_RAW_MEM;
712       }
713
714     }
715
716     if(MC_state_interleave_size(current_pair->graph_state) > 0){
717       XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
718       MC_restore_snapshot(current_snapshot);
719       MC_UNSET_RAW_MEM;
720     }
721
722   }
723
724   
725   MC_SET_RAW_MEM;
726   xbt_fifo_shift(mc_stack_liveness_stateful);
727   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
728   MC_UNSET_RAW_MEM;
729
730 }