Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix sendBounded java binding
[simgrid.git] / src / mc / mc_liveness.c
1 /* Copyright (c) 2011-2013 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 /********* Global variables *********/
14
15 xbt_dynar_t acceptance_pairs;
16 xbt_dynar_t visited_pairs;
17 xbt_dynar_t successors;
18
19
20 /********* Static functions *********/
21
22 static int is_reached_acceptance_pair(xbt_automaton_state_t st){
23
24   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
25
26   MC_SET_RAW_MEM;
27
28   mc_acceptance_pair_t new_pair = NULL;
29   new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
30   new_pair->num = xbt_dynar_length(acceptance_pairs) + 1;
31   new_pair->automaton_state = st;
32   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
33   new_pair->system_state = MC_take_snapshot();  
34   
35   /* Get values of propositional symbols */
36   int res;
37   int_f_void_t f;
38   unsigned int cursor = 0;
39   xbt_automaton_propositional_symbol_t ps = NULL;
40   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
41     f = (int_f_void_t)ps->function;
42     res = f();
43     xbt_dynar_push_as(new_pair->prop_ato, int, res);
44   }
45   
46   MC_UNSET_RAW_MEM;
47   
48   if(xbt_dynar_is_empty(acceptance_pairs)){
49
50     MC_SET_RAW_MEM;
51     /* New acceptance pair */
52     xbt_dynar_push(acceptance_pairs, &new_pair); 
53     MC_UNSET_RAW_MEM;
54
55     if(raw_mem_set)
56       MC_SET_RAW_MEM;
57  
58     return 0;
59
60   }else{
61
62     MC_SET_RAW_MEM;
63     
64     cursor = 0;
65     mc_acceptance_pair_t pair_test = NULL;
66      
67     xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
68       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
69         XBT_DEBUG("****** Pair reached #%d ******", pair_test->num);
70       if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
71         if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
72           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
73             
74             if(raw_mem_set)
75               MC_SET_RAW_MEM;
76             else
77               MC_UNSET_RAW_MEM;
78             
79             return 1;
80           }
81         }else{
82           XBT_DEBUG("Different values of propositional symbols");
83         }
84       }else{
85         XBT_DEBUG("Different automaton state");
86       }
87     }
88
89     /* New acceptance pair */
90     xbt_dynar_push(acceptance_pairs, &new_pair); 
91     
92     MC_UNSET_RAW_MEM;
93
94     if(raw_mem_set)
95       MC_SET_RAW_MEM;
96  
97     compare = 0;
98     
99     return 0;
100     
101   }
102 }
103
104
105 static void set_acceptance_pair_reached(xbt_automaton_state_t st){
106
107   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
108  
109   MC_SET_RAW_MEM;
110
111   mc_acceptance_pair_t pair = NULL;
112   pair = xbt_new0(s_mc_acceptance_pair_t, 1);
113   pair->num = xbt_dynar_length(acceptance_pairs) + 1;
114   pair->automaton_state = st;
115   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
116   pair->system_state = MC_take_snapshot();
117
118   /* Get values of propositional symbols */
119   unsigned int cursor = 0;
120   xbt_automaton_propositional_symbol_t ps = NULL;
121   int res;
122   int_f_void_t f;
123
124   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
125     f = (int_f_void_t)ps->function;
126     res = f();
127     xbt_dynar_push_as(pair->prop_ato, int, res);
128   }
129
130   xbt_dynar_push(acceptance_pairs, &pair); 
131   
132   MC_UNSET_RAW_MEM;
133
134   if(raw_mem_set)
135     MC_SET_RAW_MEM;
136     
137 }
138
139 static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){
140
141   mc_visited_pair_t new_pair = NULL;
142   new_pair = xbt_new0(s_mc_visited_pair_t, 1);
143   new_pair->automaton_state = as;
144   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
145   new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
146   new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
147   new_pair->system_state = MC_take_snapshot();  
148   
149   /* Get values of propositional symbols */
150   int res;
151   int_f_void_t f;
152   unsigned int cursor = 0;
153   xbt_automaton_propositional_symbol_t ps = NULL;
154   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
155     f = (int_f_void_t)ps->function;
156     res = f();
157     xbt_dynar_push_as(new_pair->prop_ato, int, res);
158   }
159
160   return new_pair;
161
162 }
163
164 static int is_visited_pair(xbt_automaton_state_t as){
165
166   if(_sg_mc_visited == 0)
167     return -1;
168
169   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
170
171   MC_SET_RAW_MEM;
172   mc_visited_pair_t new_pair = visited_pair_new(as);
173   MC_UNSET_RAW_MEM;
174
175   if(xbt_dynar_is_empty(visited_pairs)){
176
177     MC_SET_RAW_MEM;
178     xbt_dynar_push(visited_pairs, &new_pair); 
179     MC_UNSET_RAW_MEM;
180
181     if(raw_mem_set)
182       MC_SET_RAW_MEM;
183
184     return -1;
185
186   }else{
187
188     MC_SET_RAW_MEM;
189     
190     size_t current_bytes_used = new_pair->heap_bytes_used;
191     int current_nb_processes = new_pair->nb_processes;
192
193     unsigned int cursor = 0;
194     int previous_cursor = 0, next_cursor = 0;
195     int start = 0;
196     int end = xbt_dynar_length(visited_pairs) - 1;
197
198     mc_visited_pair_t pair_test = NULL;
199     size_t bytes_used_test;
200     int nb_processes_test;
201     int same_processes_and_bytes_not_found = 1;
202
203     while(start <= end && same_processes_and_bytes_not_found){
204       cursor = (start + end) / 2;
205       pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
206       bytes_used_test = pair_test->heap_bytes_used;
207       nb_processes_test = pair_test->nb_processes;
208       if(nb_processes_test < current_nb_processes)
209         start = cursor + 1;
210       if(nb_processes_test > current_nb_processes)
211         end = cursor - 1; 
212       if(nb_processes_test == current_nb_processes){
213         if(bytes_used_test < current_bytes_used)
214           start = cursor + 1;
215         if(bytes_used_test > current_bytes_used)
216           end = cursor - 1;
217         if(bytes_used_test == current_bytes_used){
218           same_processes_and_bytes_not_found = 0;
219           if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
220             if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
221               if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
222                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
223                 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
224                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
225                 if(raw_mem_set)
226                   MC_SET_RAW_MEM;
227                 else
228                   MC_UNSET_RAW_MEM;
229                 return pair_test->num;
230               }
231             }
232           }
233           /* Search another pair with same number of bytes used in std_heap */
234           previous_cursor = cursor - 1;
235           while(previous_cursor >= 0){
236             pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_visited_pair_t);
237             bytes_used_test = pair_test->system_state->heap_bytes_used;
238             if(bytes_used_test != current_bytes_used)
239               break;
240             if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
241               if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){  
242                 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
243                   xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
244                   xbt_dynar_insert_at(visited_pairs, previous_cursor, &new_pair);
245                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
246                   if(raw_mem_set)
247                     MC_SET_RAW_MEM;
248                   else
249                     MC_UNSET_RAW_MEM;
250                   return pair_test->num;
251                 }
252               }
253             }
254             previous_cursor--;
255           }
256           next_cursor = cursor + 1;
257           while(next_cursor < xbt_dynar_length(visited_pairs)){
258             pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_visited_pair_t);
259             bytes_used_test = pair_test->system_state->heap_bytes_used;
260             if(bytes_used_test != current_bytes_used)
261               break;
262             if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
263               if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
264                 if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
265                   xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
266                   xbt_dynar_insert_at(visited_pairs, next_cursor, &new_pair);
267                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
268                   if(raw_mem_set)
269                     MC_SET_RAW_MEM;
270                   else
271                     MC_UNSET_RAW_MEM;
272                   return pair_test->num;
273                 }
274               }
275             }
276             next_cursor++;
277           }
278         }
279       }
280     }
281
282     pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
283     bytes_used_test = pair_test->heap_bytes_used;
284
285     if(bytes_used_test < current_bytes_used)
286       xbt_dynar_insert_at(visited_pairs, cursor + 1, &new_pair);
287     else
288       xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
289
290     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
291       int min = mc_stats->expanded_states;
292       unsigned int cursor2 = 0;
293       unsigned int index = 0;
294       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
295         if(pair_test->num < min){
296           index = cursor2;
297           min = pair_test->num;
298         }
299       }
300       xbt_dynar_remove_at(visited_pairs, index, NULL);
301     }
302
303     /*cursor = 0;
304     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
305       fprintf(stderr, "Visited pair %d, nb_processes %d and heap_bytes_used %zu\n", pair_test->num, pair_test->nb_processes, pair_test->heap_bytes_used);
306       }*/
307     
308     MC_UNSET_RAW_MEM;
309
310     if(raw_mem_set)
311       MC_SET_RAW_MEM;
312     
313     return -1;
314     
315   }
316  
317 }
318
319 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
320   
321   switch(l->type){
322   case 0 : {
323     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
324     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
325     return (left_res || right_res);
326   }
327   case 1 : {
328     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
329     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
330     return (left_res && right_res);
331   }
332   case 2 : {
333     int res = MC_automaton_evaluate_label(l->u.exp_not);
334     return (!res);
335   }
336   case 3 : { 
337     unsigned int cursor = 0;
338     xbt_automaton_propositional_symbol_t p = NULL;
339     int_f_void_t f;
340     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
341       if(strcmp(p->pred, l->u.predicat) == 0){
342         f = (int_f_void_t)p->function;
343         return f();
344       }
345     }
346     return -1;
347   }
348   case 4 : {
349     return 2;
350   }
351   default : 
352     return -1;
353   }
354 }
355
356
357 /********* Free functions *********/
358
359 static void visited_pair_free(mc_visited_pair_t pair){
360   if(pair){
361     xbt_dynar_free(&(pair->prop_ato));
362     MC_free_snapshot(pair->system_state);
363     xbt_free(pair);
364   }
365 }
366
367 static void visited_pair_free_voidp(void *p){
368   visited_pair_free((mc_visited_pair_t) * (void **) p);
369 }
370
371 static void acceptance_pair_free(mc_acceptance_pair_t pair){
372   if(pair){
373     xbt_dynar_free(&(pair->prop_ato));
374     MC_free_snapshot(pair->system_state);
375     xbt_free(pair);
376   }
377 }
378
379 static void acceptance_pair_free_voidp(void *p){
380   acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
381 }
382
383
384 /********* DDFS Algorithm *********/
385
386
387 void MC_ddfs_init(void){
388
389   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
390
391   XBT_DEBUG("**************************************************");
392   XBT_DEBUG("Double-DFS init");
393   XBT_DEBUG("**************************************************");
394
395   mc_pair_t mc_initial_pair = NULL;
396   mc_state_t initial_graph_state = NULL;
397   smx_process_t process; 
398
399  
400   MC_wait_for_requests();
401
402   MC_SET_RAW_MEM;
403
404   initial_graph_state = MC_state_new();
405   xbt_swag_foreach(process, simix_global->process_list){
406     if(MC_process_is_enabled(process)){
407       MC_state_interleave_process(initial_graph_state, process);
408     }
409   }
410
411   acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
412   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
413   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
414
415   /* Save the initial state */
416   initial_state_liveness->snapshot = MC_take_snapshot();
417
418   MC_UNSET_RAW_MEM; 
419   
420   unsigned int cursor = 0;
421   xbt_automaton_state_t automaton_state;
422
423   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
424     if(automaton_state->type == -1){
425       
426       MC_SET_RAW_MEM;
427       mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
428       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
429       MC_UNSET_RAW_MEM;
430       
431       if(cursor != 0){
432         MC_restore_snapshot(initial_state_liveness->snapshot);
433         MC_UNSET_RAW_MEM;
434       }
435
436       MC_ddfs(0);
437
438     }else{
439       if(automaton_state->type == 2){
440       
441         MC_SET_RAW_MEM;
442         mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
443         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
444         MC_UNSET_RAW_MEM;
445
446         set_acceptance_pair_reached(automaton_state);
447
448         if(cursor != 0){
449           MC_restore_snapshot(initial_state_liveness->snapshot);
450           MC_UNSET_RAW_MEM;
451         }
452   
453         MC_ddfs(1);
454   
455       }
456     }
457   }
458
459   if(initial_state_liveness->raw_mem_set)
460     MC_SET_RAW_MEM;
461   else
462     MC_UNSET_RAW_MEM;
463   
464
465 }
466
467
468 void MC_ddfs(int search_cycle){
469
470   smx_process_t process;
471   mc_pair_t current_pair = NULL;
472
473   if(xbt_fifo_size(mc_stack_liveness) == 0)
474     return;
475
476
477   /* Get current pair */
478   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
479
480   /* Update current state in buchi automaton */
481   _mc_property_automaton->current_state = current_pair->automaton_state;
482
483  
484   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
485  
486   mc_stats->visited_states++;
487
488   int value;
489   mc_state_t next_graph_state = NULL;
490   smx_simcall_t req = NULL;
491   char *req_str;
492
493   xbt_automaton_transition_t transition_succ;
494   unsigned int cursor = 0;
495   int res;
496
497   mc_pair_t next_pair = NULL;
498   mc_pair_t pair_succ;
499
500   mc_pair_t pair_to_remove;
501   mc_acceptance_pair_t acceptance_pair_to_remove;
502   
503   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
504
505     if(current_pair->requests > 0){
506
507       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
508    
509         /* Debug information */
510        
511         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
512           req_str = MC_request_to_string(req, value);
513           XBT_DEBUG("Execute: %s", req_str);
514           xbt_free(req_str);
515         }
516
517         MC_state_set_executed_request(current_pair->graph_state, req, value);  
518         mc_stats->executed_transitions++;
519
520         /* Answer the request */
521         SIMIX_simcall_pre(req, value);
522
523         /* Wait for requests (schedules processes) */
524         MC_wait_for_requests();
525
526         MC_SET_RAW_MEM;
527
528         /* Create the new expanded graph_state */
529         next_graph_state = MC_state_new();
530
531         /* Get enabled process and insert it in the interleave set of the next graph_state */
532         xbt_swag_foreach(process, simix_global->process_list){
533           if(MC_process_is_enabled(process)){
534             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
535           }
536         }
537
538         xbt_swag_foreach(process, simix_global->process_list){
539           if(MC_process_is_enabled(process)){
540             MC_state_interleave_process(next_graph_state, process);
541           }
542         }
543
544         xbt_dynar_reset(successors);
545
546         MC_UNSET_RAW_MEM;
547
548
549         cursor= 0;
550         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
551
552           res = MC_automaton_evaluate_label(transition_succ->label);
553
554           if(res == 1){ // enabled transition in automaton
555             MC_SET_RAW_MEM;
556             next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
557             xbt_dynar_push(successors, &next_pair);
558             MC_UNSET_RAW_MEM;
559           }
560
561         }
562
563         cursor = 0;
564    
565         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
566       
567           res = MC_automaton_evaluate_label(transition_succ->label);
568   
569           if(res == 2){ // true transition in automaton
570             MC_SET_RAW_MEM;
571             next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));
572             xbt_dynar_push(successors, &next_pair);
573             MC_UNSET_RAW_MEM;
574           }
575
576         }
577
578         cursor = 0; 
579   
580         xbt_dynar_foreach(successors, cursor, pair_succ){
581
582           if(search_cycle == 1){
583
584             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
585           
586               if(is_reached_acceptance_pair(pair_succ->automaton_state)){
587         
588                 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));
589
590                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
591                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
592                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
593                 XBT_INFO("Counter-example that violates formula :");
594                 MC_show_stack_liveness(mc_stack_liveness);
595                 MC_dump_stack_liveness(mc_stack_liveness);
596                 MC_print_statistics(mc_stats);
597                 xbt_abort();
598
599               }else{
600
601                 if(is_visited_pair(pair_succ->automaton_state) != -1){
602
603                   XBT_DEBUG("Next pair already visited !");
604                   break;
605             
606                 }else{
607
608                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
609
610                   XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
611
612                   MC_SET_RAW_MEM;
613                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
614                   MC_UNSET_RAW_MEM;
615     
616                   MC_ddfs(search_cycle);
617                 
618                 }
619
620               }
621
622             }else{
623
624               if(is_visited_pair(pair_succ->automaton_state) != -1){
625
626                 XBT_DEBUG("Next pair already visited !");
627                 break;
628                 
629               }else{
630
631                 MC_SET_RAW_MEM;
632                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
633                 MC_UNSET_RAW_MEM;
634                 
635                 MC_ddfs(search_cycle);
636               }
637                
638             }
639
640           }else{
641
642             if(is_visited_pair(pair_succ->automaton_state) != -1){
643
644               XBT_DEBUG("Next pair already visited !");
645               break;
646             
647             }else{
648     
649               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
650
651                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
652       
653                 set_acceptance_pair_reached(pair_succ->automaton_state); 
654
655                 search_cycle = 1;
656
657                 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
658
659               }
660
661               MC_SET_RAW_MEM;
662               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
663               MC_UNSET_RAW_MEM;
664             
665               MC_ddfs(search_cycle);
666
667             }
668            
669           }
670
671           /* Restore system before checking others successors */
672           if(cursor != (xbt_dynar_length(successors) - 1))
673             MC_replay_liveness(mc_stack_liveness, 1);
674             
675         }
676
677         if(MC_state_interleave_size(current_pair->graph_state) > 0){
678           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
679           MC_replay_liveness(mc_stack_liveness, 0);
680         }
681       }
682
683  
684     }else{
685
686       mc_stats->executed_transitions++;
687       
688       XBT_DEBUG("No more request to execute in this state, search evolution in B├╝chi Automaton.");
689
690       MC_SET_RAW_MEM;
691
692       /* Create the new expanded graph_state */
693       next_graph_state = MC_state_new();
694
695       xbt_dynar_reset(successors);
696
697       MC_UNSET_RAW_MEM;
698
699
700       cursor= 0;
701       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
702
703         res = MC_automaton_evaluate_label(transition_succ->label);
704
705         if(res == 1){ // enabled transition in automaton
706           MC_SET_RAW_MEM;
707           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
708           xbt_dynar_push(successors, &next_pair);
709           MC_UNSET_RAW_MEM;
710         }
711
712       }
713
714       cursor = 0;
715    
716       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
717       
718         res = MC_automaton_evaluate_label(transition_succ->label);
719   
720         if(res == 2){ // true transition in automaton
721           MC_SET_RAW_MEM;
722           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
723           xbt_dynar_push(successors, &next_pair);
724           MC_UNSET_RAW_MEM;
725         }
726
727       }
728
729       cursor = 0; 
730      
731       xbt_dynar_foreach(successors, cursor, pair_succ){
732
733         if(search_cycle == 1){
734
735           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
736
737             if(is_reached_acceptance_pair(pair_succ->automaton_state)){
738            
739               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
740         
741               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
742               XBT_INFO("|             ACCEPTANCE CYCLE            |");
743               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
744               XBT_INFO("Counter-example that violates formula :");
745               MC_show_stack_liveness(mc_stack_liveness);
746               MC_dump_stack_liveness(mc_stack_liveness);
747               MC_print_statistics(mc_stats);
748               xbt_abort();
749
750             }else{
751
752               if(is_visited_pair(pair_succ->automaton_state) != -1){
753                 
754                 XBT_DEBUG("Next pair already visited !");
755                 break;
756                 
757               }else{
758
759                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
760         
761                 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
762
763                 MC_SET_RAW_MEM;
764                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
765                 MC_UNSET_RAW_MEM;
766         
767                 MC_ddfs(search_cycle);
768               
769               }
770
771             }
772
773           }else{
774             
775             if(is_visited_pair(pair_succ->automaton_state) != -1){
776               
777               XBT_DEBUG("Next pair already visited !");
778               break;
779               
780             }else{
781
782               MC_SET_RAW_MEM;
783               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
784               MC_UNSET_RAW_MEM;
785             
786               MC_ddfs(search_cycle);
787
788             }
789             
790           }
791       
792
793         }else{
794       
795           if(is_visited_pair(pair_succ->automaton_state) != -1){
796
797             XBT_DEBUG("Next pair already visited !");
798             break;
799             
800           }else{
801
802             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
803
804               set_acceptance_pair_reached(pair_succ->automaton_state);
805          
806               search_cycle = 1;
807
808               XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
809
810             }
811
812             MC_SET_RAW_MEM;
813             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
814             MC_UNSET_RAW_MEM;
815           
816             MC_ddfs(search_cycle);
817           
818           }
819           
820         }
821
822         /* Restore system before checking others successors */
823         if(cursor != xbt_dynar_length(successors) - 1)
824           MC_replay_liveness(mc_stack_liveness, 1);
825
826       }           
827
828     }
829     
830   }else{
831     
832     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
833     if(MC_state_interleave_size(current_pair->graph_state) > 0){
834       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
835       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
836     }
837     
838   }
839
840   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
841     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
842   }else{
843     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
844   }
845
846   
847   MC_SET_RAW_MEM;
848   pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
849   xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
850   pair_to_remove = NULL;
851   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
852     acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t);
853     acceptance_pair_free(acceptance_pair_to_remove);
854     acceptance_pair_to_remove = NULL;
855   }
856   MC_UNSET_RAW_MEM;
857
858 }