Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
7d07e0dda2740a40b6badee71d411ff692e0300e
[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;
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
609   mc_pair_t next_pair = NULL;
610   mc_pair_t pair_succ;
611
612   mc_pair_t pair_to_remove;
613   
614   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
615
616     if(current_pair->requests > 0){
617
618       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
619    
620         /* Debug information */
621        
622         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
623           req_str = MC_request_to_string(req, value);
624           XBT_DEBUG("Execute: %s", req_str);
625           xbt_free(req_str);
626         }
627
628         MC_state_set_executed_request(current_pair->graph_state, req, value);  
629         mc_stats->executed_transitions++;
630
631         /* Answer the request */
632         SIMIX_simcall_pre(req, value);
633
634         /* Wait for requests (schedules processes) */
635         MC_wait_for_requests();
636
637         MC_SET_RAW_MEM;
638
639         /* Create the new expanded graph_state */
640         next_graph_state = MC_state_new();
641
642         /* Get enabled process and insert it in the interleave set of the next graph_state */
643         xbt_swag_foreach(process, simix_global->process_list){
644           if(MC_process_is_enabled(process)){
645             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
646           }
647         }
648
649         xbt_swag_foreach(process, simix_global->process_list){
650           if(MC_process_is_enabled(process)){
651             MC_state_interleave_process(next_graph_state, process);
652           }
653         }
654
655         xbt_dynar_reset(successors);
656
657         MC_UNSET_RAW_MEM;
658
659
660         cursor= 0;
661         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
662
663           res = MC_automaton_evaluate_label(transition_succ->label);
664
665           if(res == 1){ // enabled transition in automaton
666             MC_SET_RAW_MEM;
667             next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
668             xbt_dynar_push(successors, &next_pair);
669             MC_UNSET_RAW_MEM;
670           }
671
672         }
673
674         cursor = 0;
675    
676         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
677       
678           res = MC_automaton_evaluate_label(transition_succ->label);
679   
680           if(res == 2){ // true transition in automaton
681             MC_SET_RAW_MEM;
682             next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));
683             xbt_dynar_push(successors, &next_pair);
684             MC_UNSET_RAW_MEM;
685           }
686
687         }
688
689         cursor = 0; 
690   
691         xbt_dynar_foreach(successors, cursor, pair_succ){
692
693           if(search_cycle == 1){
694
695             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
696           
697               if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
698         
699                 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));
700
701                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
702                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
703                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
704                 XBT_INFO("Counter-example that violates formula :");
705                 MC_show_stack_liveness(mc_stack_liveness);
706                 MC_dump_stack_liveness(mc_stack_liveness);
707                 MC_print_statistics(mc_stats);
708                 xbt_abort();
709
710               }else{
711
712                 if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
713
714                   XBT_DEBUG("Next pair already visited !");
715                   break;
716             
717                 }else{
718
719                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
720
721                   XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
722
723                   MC_SET_RAW_MEM;
724                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
725                   MC_UNSET_RAW_MEM;
726     
727                   MC_ddfs(search_cycle);
728                 
729                 }
730
731               }
732
733             }else{
734
735               if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
736
737                 XBT_DEBUG("Next pair already visited !");
738                 break;
739                 
740               }else{
741
742                 MC_SET_RAW_MEM;
743                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
744                 MC_UNSET_RAW_MEM;
745                 
746                 MC_ddfs(search_cycle);
747               }
748                
749             }
750
751           }else{
752
753             if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
754
755               XBT_DEBUG("Next pair already visited !");
756               break;
757             
758             }else{
759     
760               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
761
762                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
763       
764                 set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state); 
765
766                 search_cycle = 1;
767
768                 XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
769
770               }
771
772               MC_SET_RAW_MEM;
773               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
774               MC_UNSET_RAW_MEM;
775             
776               MC_ddfs(search_cycle);
777
778             }
779            
780           }
781
782           /* Restore system before checking others successors */
783           if(cursor != (xbt_dynar_length(successors) - 1))
784             MC_replay_liveness(mc_stack_liveness, 1);
785             
786         }
787
788         if(MC_state_interleave_size(current_pair->graph_state) > 0){
789           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
790           MC_replay_liveness(mc_stack_liveness, 0);
791         }
792       }
793
794  
795     }else{
796
797       mc_stats->executed_transitions++;
798       
799       XBT_DEBUG("No more request to execute in this state, search evolution in B├╝chi Automaton.");
800
801       MC_SET_RAW_MEM;
802
803       /* Create the new expanded graph_state */
804       next_graph_state = MC_state_new();
805
806       xbt_dynar_reset(successors);
807
808       MC_UNSET_RAW_MEM;
809
810
811       cursor= 0;
812       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
813
814         res = MC_automaton_evaluate_label(transition_succ->label);
815
816         if(res == 1){ // enabled transition in automaton
817           MC_SET_RAW_MEM;
818           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
819           xbt_dynar_push(successors, &next_pair);
820           MC_UNSET_RAW_MEM;
821         }
822
823       }
824
825       cursor = 0;
826    
827       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
828       
829         res = MC_automaton_evaluate_label(transition_succ->label);
830   
831         if(res == 2){ // true transition in automaton
832           MC_SET_RAW_MEM;
833           next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
834           xbt_dynar_push(successors, &next_pair);
835           MC_UNSET_RAW_MEM;
836         }
837
838       }
839
840       cursor = 0; 
841      
842       xbt_dynar_foreach(successors, cursor, pair_succ){
843
844         if(search_cycle == 1){
845
846           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
847
848             if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
849            
850               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
851         
852               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
853               XBT_INFO("|             ACCEPTANCE CYCLE            |");
854               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
855               XBT_INFO("Counter-example that violates formula :");
856               MC_show_stack_liveness(mc_stack_liveness);
857               MC_dump_stack_liveness(mc_stack_liveness);
858               MC_print_statistics(mc_stats);
859               xbt_abort();
860
861             }else{
862
863               if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
864                 
865                 XBT_DEBUG("Next pair already visited !");
866                 break;
867                 
868               }else{
869
870                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
871         
872                 XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
873
874                 MC_SET_RAW_MEM;
875                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
876                 MC_UNSET_RAW_MEM;
877         
878                 MC_ddfs(search_cycle);
879               
880               }
881
882             }
883
884           }else{
885             
886             if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
887               
888               XBT_DEBUG("Next pair already visited !");
889               break;
890               
891             }else{
892
893               MC_SET_RAW_MEM;
894               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
895               MC_UNSET_RAW_MEM;
896             
897               MC_ddfs(search_cycle);
898
899             }
900             
901           }
902       
903
904         }else{
905       
906           if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
907
908             XBT_DEBUG("Next pair already visited !");
909             break;
910             
911           }else{
912
913             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
914
915               set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
916          
917               search_cycle = 1;
918
919               XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
920
921             }
922
923             MC_SET_RAW_MEM;
924             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
925             MC_UNSET_RAW_MEM;
926           
927             MC_ddfs(search_cycle);
928           
929           }
930           
931         }
932
933         /* Restore system before checking others successors */
934         if(cursor != xbt_dynar_length(successors) - 1)
935           MC_replay_liveness(mc_stack_liveness, 1);
936
937       }           
938
939     }
940     
941   }else{
942     
943     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
944     if(MC_state_interleave_size(current_pair->graph_state) > 0){
945       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
946       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
947     }
948     
949   }
950
951   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
952     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
953   }else{
954     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
955   }
956
957   
958   MC_SET_RAW_MEM;
959   pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
960   xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
961   pair_to_remove = NULL;
962   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
963     remove_acceptance_pair(current_pair->num);
964   }
965   MC_UNSET_RAW_MEM;
966
967 }