Logo AND Algorithmique Numérique Distribuée

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