Logo AND Algorithmique Numérique Distribuée

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