Logo AND Algorithmique Numérique Distribuée

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