Logo AND Algorithmique Numérique Distribuée

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