Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Doxygen mc_dpor.c (and some mc_liveness.c)
[simgrid.git] / src / mc / mc_liveness.c
1 /* Copyright (c) 2011-2013. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7 #include "mc_private.h"
8 #include <unistd.h>
9 #include <sys/wait.h>
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
12                                 "Logging specific to algorithms for liveness properties verification");
13
14 /********* Global variables *********/
15
16 xbt_dynar_t acceptance_pairs;
17 xbt_dynar_t visited_pairs;
18 xbt_dynar_t successors;
19 xbt_parmap_t parmap;
20
21 /********* Static functions *********/
22
23 static xbt_dynar_t get_atomic_propositions_values(){
24   int res;
25   int_f_void_t f;
26   unsigned int cursor = 0;
27   xbt_automaton_propositional_symbol_t ps = NULL;
28   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
29
30   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
31     f = (int_f_void_t)ps->function;
32     res = f();
33     xbt_dynar_push_as(values, int, res);
34   }
35
36   return values;
37 }
38
39 /** \brief Find a suitable subrange of candidate duplicates for a given state
40  *
41  *  See mc_dpor.c with a similar (same?) function.
42  */
43 static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
44
45   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
46
47   MC_SET_RAW_MEM;
48
49   int cursor = 0, previous_cursor, next_cursor;
50   mc_visited_pair_t pair_test;
51   int start = 0;
52   int end = xbt_dynar_length(all_pairs) - 1;
53   
54   while(start <= end){
55     cursor = (start + end) / 2;
56     pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_visited_pair_t);
57     if(pair_test->nb_processes < pair->nb_processes){
58       start = cursor + 1;
59     }else if(pair_test->nb_processes > pair->nb_processes){
60       end = cursor - 1;
61     }else{
62       if(pair_test->heap_bytes_used < pair->heap_bytes_used){
63         start = cursor +1;
64       }else if(pair_test->heap_bytes_used > pair->heap_bytes_used){
65         end = cursor - 1;
66       }else{
67         *min = *max = cursor;
68         previous_cursor = cursor - 1;
69         while(previous_cursor >= 0){
70           pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_visited_pair_t);
71           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
72             break;
73           *min = previous_cursor;
74           previous_cursor--;
75         }
76         next_cursor = cursor + 1;
77         while(next_cursor < xbt_dynar_length(all_pairs)){
78           pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_visited_pair_t);
79           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
80             break;
81           *max = next_cursor;
82           next_cursor++;
83         }
84         if(!raw_mem_set)
85           MC_UNSET_RAW_MEM;
86         return -1;
87       }
88      }
89   }
90
91   if(!raw_mem_set)
92     MC_UNSET_RAW_MEM;
93
94   return cursor;
95 }
96
97 static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
98
99   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
100
101   MC_SET_RAW_MEM;
102   
103   mc_visited_pair_t pair = NULL;
104   pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
105   pair->acceptance_pair = 1;
106   
107   if(xbt_dynar_is_empty(acceptance_pairs)){
108
109     xbt_dynar_push(acceptance_pairs, &pair); 
110
111   }else{
112
113     int min = -1, max = -1, index;
114     //int res;
115     mc_visited_pair_t pair_test;
116     int cursor;
117
118     index = get_search_interval(acceptance_pairs, pair, &min, &max);
119
120     if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists
121
122       // Parallell implementation
123       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
124       if(res != -1){
125         if(!raw_mem_set)
126           MC_UNSET_RAW_MEM;
127         return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
128         }*/
129
130       cursor = min;
131       while(cursor <= max){
132         pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
133         if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
134           if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
135             if(snapshot_compare(pair_test, pair) == 0){
136               XBT_INFO("Pair %d already reached (equal to pair %d) !", pair->num, pair_test->num);
137               
138               xbt_fifo_shift(mc_stack_liveness);
139               if(dot_output != NULL)
140                 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, pair_test->num, initial_state_liveness->prev_req);
141
142               if(!raw_mem_set)
143                 MC_UNSET_RAW_MEM;
144
145               return NULL;
146             }
147           }
148         }
149         cursor++;
150       }
151       xbt_dynar_insert_at(acceptance_pairs, min, &pair);
152     }else{
153       pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
154       if(pair_test->nb_processes < pair->nb_processes){
155         xbt_dynar_insert_at(acceptance_pairs, index+1, &pair);
156       }else{
157         if(pair_test->heap_bytes_used < pair->heap_bytes_used)
158           xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
159         else
160           xbt_dynar_insert_at(acceptance_pairs, index, &pair);
161       }
162     }
163     
164   }
165
166   if(!raw_mem_set)
167     MC_UNSET_RAW_MEM;
168
169   return pair;
170  
171 }
172
173 static void remove_acceptance_pair(int pair_num){
174
175   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
176
177   MC_SET_RAW_MEM;
178
179   unsigned int cursor = 0;
180   mc_visited_pair_t pair_test = NULL;
181
182   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
183     if(pair_test->num == pair_num){
184       break;
185     }
186   }
187
188   xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
189   
190   pair_test->acceptance_removed = 1;
191
192   if(_sg_mc_visited == 0){
193     MC_visited_pair_delete(pair_test);
194   }else if(pair_test->visited_removed == 1){
195     MC_visited_pair_delete(pair_test);
196   }
197
198   if(!raw_mem_set)
199     MC_UNSET_RAW_MEM;
200 }
201
202 /** \brief Checks whether a given state has already been visited by the algorithm.
203  *
204  */
205 static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
206
207   if(_sg_mc_visited == 0)
208     return -1;
209
210   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
211
212   MC_SET_RAW_MEM;
213
214   mc_visited_pair_t new_pair = NULL;
215
216   if(pair == NULL){
217     new_pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
218   }else{
219     new_pair = pair;
220   }
221
222   if(xbt_dynar_is_empty(visited_pairs)){
223
224     xbt_dynar_push(visited_pairs, &new_pair); 
225
226   }else{
227
228     int min = -1, max = -1, index;
229     //int res;
230     mc_visited_pair_t pair_test;
231     int cursor;
232
233     index = get_search_interval(visited_pairs, new_pair, &min, &max);
234
235     if(min != -1 && max != -1){ // Visited pair with same number of processes and same heap bytes used exists
236       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
237       if(res != -1){
238         pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
239         if(pair_test->other_num == -1)
240           pair->other_num = pair_test->num;
241         else
242           pair->other_num = pair_test->other_num;
243         if(dot_output == NULL)
244           XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
245         else
246           XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
247         xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
248         xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
249         pair_test->visited_removed = 1;
250         if(pair_test->stack_removed && pair_test->visited_removed){
251           if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
252             if(pair_test->acceptance_removed){
253               MC_pair_delete(pair_test);
254             }
255           }else{
256             MC_pair_delete(pair_test);
257           }
258         }
259         if(!raw_mem_set)
260           MC_UNSET_RAW_MEM;
261         return pair->other_num;
262         }*/
263       cursor = min;
264       while(cursor <= max){
265         pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
266         //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
267           if(xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0){
268             if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0){
269               if(snapshot_compare(pair_test, new_pair) == 0){
270                 if(pair_test->other_num == -1)
271                   new_pair->other_num = pair_test->num;
272                 else
273                   new_pair->other_num = pair_test->other_num;
274                 if(dot_output == NULL)
275                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
276                 else
277                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
278                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
279                 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
280                 pair_test->visited_removed = 1;
281                 if(pair_test->acceptance_pair){
282                   if(pair_test->acceptance_removed == 1)
283                     MC_visited_pair_delete(pair_test);
284                 }else{
285                   MC_visited_pair_delete(pair_test);
286                 }
287                 if(!raw_mem_set)
288                   MC_UNSET_RAW_MEM;
289                 return new_pair->other_num;
290               }
291             }
292             //}
293         }
294         cursor++;
295       }
296       xbt_dynar_insert_at(visited_pairs, min, &new_pair);
297     }else{
298       pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
299       if(pair_test->nb_processes < new_pair->nb_processes){
300         xbt_dynar_insert_at(visited_pairs, index+1, &new_pair);
301       }else{
302         if(pair_test->heap_bytes_used < new_pair->heap_bytes_used)
303           xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
304         else
305           xbt_dynar_insert_at(visited_pairs, index, &new_pair);
306       }
307     }
308
309     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
310       int min2 = mc_stats->expanded_pairs;
311       unsigned int cursor2 = 0;
312       unsigned int index2 = 0;
313       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
314         if(pair_test->num < min2){
315           index2 = cursor2;
316           min2 = pair_test->num;
317         }
318       }
319       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
320       pair_test->visited_removed = 1;
321       if(pair_test->acceptance_pair){
322         if(pair_test->acceptance_removed)
323           MC_visited_pair_delete(pair_test);
324       }else{
325         MC_visited_pair_delete(pair_test);
326       }
327     }
328
329   }
330
331   if(!raw_mem_set)
332     MC_UNSET_RAW_MEM;
333   
334   return -1;
335 }
336
337 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
338   
339   switch(l->type){
340   case 0 : {
341     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
342     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
343     return (left_res || right_res);
344   }
345   case 1 : {
346     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values);
347     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values);
348     return (left_res && right_res);
349   }
350   case 2 : {
351     int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
352     return (!res);
353   }
354   case 3 : { 
355     unsigned int cursor = 0;
356     xbt_automaton_propositional_symbol_t p = NULL;
357     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
358       if(strcmp(p->pred, l->u.predicat) == 0)
359         return (int)xbt_dynar_get_as(atomic_propositions_values, cursor, int);
360     }
361     return -1;
362   }
363   case 4 : {
364     return 2;
365   }
366   default : 
367     return -1;
368   }
369 }
370
371
372 /********* DDFS Algorithm *********/
373
374
375 void MC_ddfs_init(void){
376
377   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
378
379   XBT_DEBUG("**************************************************");
380   XBT_DEBUG("Double-DFS init");
381   XBT_DEBUG("**************************************************");
382
383   mc_pair_t initial_pair = NULL;
384   smx_process_t process; 
385
386   MC_wait_for_requests();
387
388   MC_ignore_heap(simix_global->process_to_run->data, 0);
389   MC_ignore_heap(simix_global->process_that_ran->data, 0);
390
391   MC_SET_RAW_MEM;
392
393   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
394   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
395   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
396
397   initial_state_liveness->snapshot = MC_take_snapshot(0);
398   initial_state_liveness->prev_pair = 0;
399
400   MC_UNSET_RAW_MEM; 
401   
402   unsigned int cursor = 0;
403   xbt_automaton_state_t automaton_state;
404
405   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
406     if(automaton_state->type == -1){ /* Initial automaton state */
407       
408       MC_SET_RAW_MEM;
409
410       initial_pair = MC_pair_new();
411       initial_pair->automaton_state = automaton_state;
412       initial_pair->graph_state = MC_state_new();
413       initial_pair->atomic_propositions = get_atomic_propositions_values();
414
415       /* Get enabled process and insert it in the interleave set of the graph_state */
416       xbt_swag_foreach(process, simix_global->process_list){
417         if(MC_process_is_enabled(process)){
418           MC_state_interleave_process(initial_pair->graph_state, process);
419         }
420       }
421
422       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
423       initial_pair->search_cycle = 0;
424
425       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
426
427       MC_UNSET_RAW_MEM;
428       
429       MC_ddfs();
430       
431       if(cursor != 0){
432         MC_restore_snapshot(initial_state_liveness->snapshot);
433         MC_UNSET_RAW_MEM;
434       } 
435     }
436   }
437
438   if(initial_state_liveness->raw_mem_set)
439     MC_SET_RAW_MEM;
440   else
441     MC_UNSET_RAW_MEM;
442   
443
444 }
445
446
447 void MC_ddfs(){
448
449   smx_process_t process;
450   mc_pair_t current_pair = NULL;
451
452   if(xbt_fifo_size(mc_stack_liveness) == 0)
453     return;
454
455   /* Get current pair */
456   current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
457
458   /* Update current state in buchi automaton */
459   _mc_property_automaton->current_state = current_pair->automaton_state;
460
461   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state), current_pair->num);
462  
463   mc_stats->visited_pairs++;
464
465   int value;
466   smx_simcall_t req = NULL;
467   char *req_str;
468
469   xbt_automaton_transition_t transition_succ;
470   unsigned int cursor = 0;
471   int res;
472   int visited_num;
473
474   mc_pair_t next_pair = NULL;
475   xbt_dynar_t prop_values = NULL;
476   mc_visited_pair_t reached_pair = NULL;
477   int counter_example_depth = 0;
478   
479   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
480
481     if(current_pair->requests > 0){
482
483       if(current_pair->search_cycle){
484
485         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ 
486           if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
487
488             counter_example_depth = xbt_fifo_size(mc_stack_liveness);
489             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
490             XBT_INFO("|             ACCEPTANCE CYCLE            |");
491             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
492             XBT_INFO("Counter-example that violates formula :");
493             MC_show_stack_liveness(mc_stack_liveness);
494             MC_dump_stack_liveness(mc_stack_liveness);
495             MC_print_statistics(mc_stats);
496             XBT_INFO("Counter-example depth : %d", counter_example_depth);
497             xbt_abort();
498
499           }
500         }
501       }
502
503       if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
504
505         MC_SET_RAW_MEM;
506         if(dot_output != NULL)
507           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
508         MC_UNSET_RAW_MEM;
509               
510       }else{  
511
512         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
513
514           MC_SET_RAW_MEM;
515           if(dot_output != NULL){
516             if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
517               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
518               xbt_free(initial_state_liveness->prev_req);
519             }
520             initial_state_liveness->prev_pair = current_pair->num;
521           }
522           MC_UNSET_RAW_MEM;
523
524           /* Debug information */
525           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
526             req_str = MC_request_to_string(req, value);
527             XBT_DEBUG("Execute: %s", req_str);
528             xbt_free(req_str);
529           }
530
531           MC_SET_RAW_MEM;
532           if(dot_output != NULL){
533             initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
534             if(current_pair->search_cycle)
535               fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
536           }
537           MC_UNSET_RAW_MEM; 
538           
539           MC_state_set_executed_request(current_pair->graph_state, req, value);  
540           mc_stats->executed_transitions++;
541
542           /* Answer the request */
543           SIMIX_simcall_pre(req, value);
544           
545           /* Wait for requests (schedules processes) */
546           MC_wait_for_requests();
547
548           MC_SET_RAW_MEM;
549           prop_values = get_atomic_propositions_values();
550           MC_UNSET_RAW_MEM;
551
552           int new_pair = 0;
553          
554           /* Evaluate enabled transition according to atomic propositions values */
555           cursor= 0;
556           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
557
558             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
559
560             if(res == 1){ // enabled transition in automaton
561
562               if(new_pair)
563                 MC_replay_liveness(mc_stack_liveness, 1); 
564
565               MC_SET_RAW_MEM;
566
567               next_pair = MC_pair_new();
568               next_pair->graph_state = MC_state_new();
569               next_pair->automaton_state = transition_succ->dst;
570               next_pair->atomic_propositions = get_atomic_propositions_values();
571
572               /* Get enabled process and insert it in the interleave set of the next graph_state */
573               xbt_swag_foreach(process, simix_global->process_list){
574                 if(MC_process_is_enabled(process)){
575                   MC_state_interleave_process(next_pair->graph_state, process);
576                 }
577               }
578
579               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
580               
581               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
582                 next_pair->search_cycle = 1;
583             
584               xbt_fifo_unshift(mc_stack_liveness, next_pair);
585
586               if(mc_stats->expanded_pairs%1000000 == 0)
587                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
588
589               MC_UNSET_RAW_MEM;
590
591               new_pair = 1;
592
593               MC_ddfs();
594
595             }
596
597           }
598
599           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
600           cursor = 0;   
601           xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
602       
603             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
604   
605             if(res == 2){ // true transition in automaton
606
607               if(new_pair)
608                 MC_replay_liveness(mc_stack_liveness, 1); 
609             
610               MC_SET_RAW_MEM;
611             
612               next_pair = MC_pair_new();
613               next_pair->graph_state = MC_state_new();
614               next_pair->automaton_state = transition_succ->dst;
615               next_pair->atomic_propositions = get_atomic_propositions_values();
616
617               /* Get enabled process and insert it in the interleave set of the next graph_state */
618               xbt_swag_foreach(process, simix_global->process_list){
619                 if(MC_process_is_enabled(process)){
620                   MC_state_interleave_process(next_pair->graph_state, process);
621                 }
622               }
623
624               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
625             
626               if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
627                 next_pair->search_cycle = 1;
628
629               xbt_fifo_unshift(mc_stack_liveness, next_pair);
630
631               if(mc_stats->expanded_pairs%1000000 == 0)
632                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
633             
634               MC_UNSET_RAW_MEM;
635
636               new_pair = 1;
637
638               MC_ddfs();
639
640             }
641
642           }
643
644           if(MC_state_interleave_size(current_pair->graph_state) > 0){
645             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
646             MC_replay_liveness(mc_stack_liveness, 0);
647           }
648         
649         }
650
651       }
652  
653     }
654     
655   }else{
656     
657     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
658     if(MC_state_interleave_size(current_pair->graph_state) > 0){
659       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
660       if(_sg_mc_max_depth == 1000)
661         XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
662     }
663     
664   }
665
666   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
667     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
668   }else{
669     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num, xbt_fifo_size(mc_stack_liveness) );
670   }
671
672   
673   MC_SET_RAW_MEM;
674   xbt_dynar_free(&prop_values);
675   current_pair = xbt_fifo_shift(mc_stack_liveness);
676   if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
677     remove_acceptance_pair(current_pair->num);
678   }
679   MC_pair_delete(current_pair);
680
681   MC_UNSET_RAW_MEM;
682
683 }