Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
MC LTL : add statistics
[simgrid.git] / src / mc / mc_dfs.c
1 #include "private.h"
2 #include "unistd.h"
3
4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
5                                 "Logging specific to MC DFS algorithm");
6
7 xbt_dynar_t initial_pairs = NULL;
8 int max_pair = 0;
9 xbt_dynar_t visited_pairs;
10 xbt_dynar_t reached_pairs;
11
12 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
13   mc_pairs_t p = NULL;
14   p = xbt_new0(s_mc_pairs_t, 1);
15   p->system_state = sn;
16    p->automaton_state = st;
17   p->graph_state = sg;
18   p->num = max_pair;
19   max_pair++;
20   return p;
21     
22 }
23
24 void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){
25
26   //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as);
27   MC_SET_RAW_MEM;
28   mc_visited_pairs_t p = NULL;
29   p = xbt_new0(s_mc_visited_pairs_t, 1);
30   p->graph_state = gs;
31   p->automaton_state = as;
32   p->search_cycle = sc;
33   xbt_dynar_push(visited_pairs, &p); 
34   //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
35   MC_UNSET_RAW_MEM;
36
37   //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
38 }
39
40 int reached(mc_state_t gs, xbt_state_t as ){
41
42   mc_reached_pairs_t rp = NULL;
43   unsigned int c= 0;
44   unsigned int i;
45   int different_process;
46
47   MC_SET_RAW_MEM;
48   xbt_dynar_foreach(reached_pairs, c, rp){
49     if(rp->automaton_state == as){
50       different_process=0;
51       for(i=0; i < gs->max_pid; i++){
52         if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){
53           different_process++;
54         }
55       }
56       if(different_process==0){
57         MC_UNSET_RAW_MEM;
58         XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached (graph=%p)!", gs, as, as->id, rp->graph_state);
59         return 1;
60       }
61       /* XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached !", gs, as, as->id); */
62       /* return 1; */
63     }
64   }
65   MC_UNSET_RAW_MEM;
66   return 0;
67 }
68
69 void set_pair_reached(mc_state_t gs, xbt_state_t as){
70
71   //XBT_DEBUG("Set pair (graph=%p, automaton=%p) reached ", gs, as);
72   //if(reached(gs, as) == 0){
73     MC_SET_RAW_MEM;
74     mc_reached_pairs_t p = NULL;
75     p = xbt_new0(s_mc_reached_pairs_t, 1);
76     p->graph_state = gs;
77     p->automaton_state = as;
78     xbt_dynar_push(reached_pairs, &p); 
79     XBT_DEBUG("New reached pair : graph=%p, automaton=%p(%s)", gs, as, as->id);
80     MC_UNSET_RAW_MEM;
81     //}
82
83 }
84
85 int visited(mc_state_t gs, xbt_state_t as, int sc){
86   unsigned int c = 0;
87   mc_visited_pairs_t p = NULL;
88   unsigned int i;
89   int different_process;
90
91   //XBT_DEBUG("Visited pair length : %lu", xbt_dynar_length(visited_pairs));
92
93   MC_SET_RAW_MEM;
94   xbt_dynar_foreach(visited_pairs, c, p){
95     //XBT_DEBUG("Test pair visited");
96     //sleep(1);
97     if((p->automaton_state == as) && (p->search_cycle == sc)){
98       different_process=0;
99       for(i=0; i < gs->max_pid; i++){
100         if(gs->proc_status[i].state != p->graph_state->proc_status[i].state){
101           different_process++;
102         }
103       }
104       if(different_process==0){
105         MC_UNSET_RAW_MEM;
106         return 1;
107       }
108     }
109   }
110   MC_UNSET_RAW_MEM;
111   return 0;
112
113 }
114
115 void MC_dfs_init(xbt_automaton_t a){
116
117    XBT_DEBUG("**************************************************");
118    XBT_DEBUG("DFS init");
119    XBT_DEBUG("**************************************************");
120  
121   mc_pairs_t mc_initial_pair;
122   mc_state_t initial_graph_state;
123   smx_process_t process; 
124   mc_snapshot_t init_snapshot;
125  
126   MC_wait_for_requests();
127
128   MC_SET_RAW_MEM;
129
130   init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
131
132   initial_graph_state = MC_state_pair_new();
133   xbt_swag_foreach(process, simix_global->process_list){
134     if(MC_process_is_enabled(process)){
135       MC_state_interleave_process(initial_graph_state, process);
136     }
137   }
138
139   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL); 
140   reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL); 
141
142   MC_take_snapshot(init_snapshot);
143
144   MC_UNSET_RAW_MEM; 
145
146   /* unsigned int cursor = 0; */
147   /* xbt_state_t state = NULL; */
148   /* int nb_init_state = 0; */
149
150   /* xbt_dynar_foreach(a->states, cursor, state){ */
151   /*   if(state->type == -1){ */
152
153   /*     MC_SET_RAW_MEM; */
154   /*     mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); */
155
156   /*     xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); */
157
158   /*     XBT_DEBUG("**************************************************"); */
159   /*     XBT_DEBUG("Initial state=%p ", mc_initial_pair); */
160
161   /*     MC_UNSET_RAW_MEM; */
162
163   /*     set_pair_visited(mc_initial_pair->graph_state, mc_initial_pair->automaton_state, 0); */
164       
165   /*     if(nb_init_state == 0) */
166   /*    MC_dfs(a, 0, 0); */
167   /*     else */
168   /*    MC_dfs(a, 0, 1); */
169       
170   /*     nb_init_state++; */
171   /*   } */
172   /* } */
173
174   /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
175     -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
176
177   unsigned int cursor = 0;
178   unsigned int cursor2 = 0;
179   xbt_state_t state = NULL;
180   int res;
181   xbt_transition_t transition_succ;
182   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
183   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
184   //  int enabled_transition = 0;
185   mc_pairs_t pair_succ;
186
187   xbt_dynar_foreach(a->states, cursor, state){
188     if(state->type == -1){
189       xbt_dynar_foreach(state->out, cursor2, transition_succ){
190         res = MC_automaton_evaluate_label(a, transition_succ->label);
191         
192         if(res == 1){
193          
194           MC_SET_RAW_MEM;
195
196           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
197           xbt_dynar_push(successors, &mc_initial_pair);
198
199           //XBT_DEBUG("New initial successor");
200
201           MC_UNSET_RAW_MEM;
202
203         }else{
204           if(res == 2){
205
206             MC_SET_RAW_MEM;
207             
208             mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
209             xbt_dynar_push(elses, &mc_initial_pair);
210
211             //XBT_DEBUG("New initial successor");
212
213             MC_UNSET_RAW_MEM;
214           }
215         }
216       }
217     }
218   }
219
220   if(xbt_dynar_length(successors) > 0){
221
222     cursor = 0;
223     xbt_dynar_foreach(successors, cursor, pair_succ){
224       MC_SET_RAW_MEM;
225
226       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
227
228       XBT_DEBUG("**************************************************");
229       XBT_DEBUG("Initial state=%p ", pair_succ);
230
231       MC_UNSET_RAW_MEM;
232
233       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
234
235       if(cursor == 0){
236         MC_dfs(a, 0, 0);
237         if(pair_succ->automaton_state->type == 1){
238           set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
239           MC_dfs(a, 1, 0);
240         }
241       }else{
242         MC_dfs(a, 0, 1);
243         if(pair_succ->automaton_state->type == 1){
244           MC_dfs(a, 1, 1);
245         }
246       }
247
248       /* if(cursor == 0) */
249       /*        MC_dfs(a, 0, 0); */
250       /* else */
251       /*        MC_dfs(a, 0, 1); */
252       
253     }
254
255   }
256
257   if(xbt_dynar_length(elses) > 0){
258     cursor = 0;
259     xbt_dynar_foreach(elses, cursor, pair_succ){
260       MC_SET_RAW_MEM;
261
262       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
263
264       XBT_DEBUG("**************************************************");
265       XBT_DEBUG("Initial state=%p ", pair_succ);
266
267       MC_UNSET_RAW_MEM;
268
269       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
270
271       if(cursor == 0){
272         MC_dfs(a, 0, 0);
273         if(pair_succ->automaton_state->type == 1){
274           set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);
275           MC_dfs(a, 1, 0);
276         }
277       }else{
278         MC_dfs(a, 0, 1);
279         if(pair_succ->automaton_state->type == 1){
280           MC_dfs(a, 1, 1);
281         }
282       }
283
284       /* if(cursor == 0) */
285       /*   MC_dfs(a, 0, 0); */
286       /* else */
287       /*   MC_dfs(a, 0, 1); */
288         
289     
290     }
291   }
292   
293 }
294
295
296 void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
297
298   smx_process_t process = NULL;
299
300
301   if(xbt_fifo_size(mc_snapshot_stack) == 0)
302     return;
303
304   if(restore == 1){
305     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
306     MC_UNSET_RAW_MEM;
307   }
308
309   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs));
310
311   /* Get current state */
312   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
313
314   if(restore==1){
315     xbt_swag_foreach(process, simix_global->process_list){
316       if(MC_process_is_enabled(process)){
317         //XBT_DEBUG("Pid : %lu", process->pid);
318         MC_state_interleave_process(current_pair->graph_state, process);
319       }
320     }
321   }
322
323   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
324   XBT_DEBUG("State : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
325   //XBT_DEBUG("Restore : %d", restore);
326   
327   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
328   
329   //sleep(1);
330
331   mc_stats_pair->visited_pairs++;
332
333   int value;
334   mc_state_t next_graph_state = NULL;
335   smx_req_t req = NULL;
336   char *req_str;
337
338   mc_pairs_t pair_succ;
339   xbt_transition_t transition_succ;
340   unsigned int cursor;
341   int res;
342   //int enabled_transition = 0;
343
344   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
345
346   mc_pairs_t next_pair;
347   mc_snapshot_t next_snapshot;
348   mc_snapshot_t current_snapshot;
349   
350   
351   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
352
353     MC_SET_RAW_MEM;
354     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
355     MC_take_snapshot(current_snapshot);
356     MC_UNSET_RAW_MEM;
357    
358     
359     /* Debug information */
360     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
361       req_str = MC_request_to_string(req, value);
362       XBT_DEBUG("Execute: %s", req_str);
363       xbt_free(req_str);
364     }
365
366     MC_state_set_executed_request(current_pair->graph_state, req, value);
367
368     /* Answer the request */
369     SIMIX_request_pre(req, value);
370
371     /* Wait for requests (schedules processes) */
372     MC_wait_for_requests();
373
374
375     /* Create the new expanded graph_state */
376     MC_SET_RAW_MEM;
377
378     next_graph_state = MC_state_pair_new();
379     
380     /* Get enabled process and insert it in the interleave set of the next graph_state */
381     xbt_swag_foreach(process, simix_global->process_list){
382       if(MC_process_is_enabled(process)){
383         //XBT_DEBUG("Pid : %lu", process->pid);
384         MC_state_interleave_process(next_graph_state, process);
385       }
386     }
387
388     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
389     MC_take_snapshot(next_snapshot);
390       
391     MC_UNSET_RAW_MEM;
392
393     xbt_dynar_reset(successors);
394     
395     cursor = 0;
396     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
397
398       res = MC_automaton_evaluate_label(a, transition_succ->label);
399
400       MC_SET_RAW_MEM;
401       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
402
403       //XBT_DEBUG("Next pair : %p", next_pair);
404         
405       if((res == 1) || (res == 2)){ // enabled transition in automaton
406         xbt_dynar_push(successors, &next_pair);
407         mc_stats_pair->expanded_pairs++;
408       }
409
410       MC_UNSET_RAW_MEM;
411     }
412
413    
414     if(xbt_dynar_length(successors) == 0){
415
416       MC_SET_RAW_MEM;
417       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
418       xbt_dynar_push(successors, &next_pair);
419       mc_stats_pair->expanded_pairs++;
420       MC_UNSET_RAW_MEM;
421         
422     }
423
424     // XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors));
425     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses));
426
427     if(xbt_dynar_length(successors) >0){
428
429       cursor = 0;
430       xbt_dynar_foreach(successors, cursor, pair_succ){
431
432         //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
433
434         if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
435           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
436           XBT_INFO("|             ACCEPTANCE CYCLE            |");
437           XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
438           XBT_INFO("Counter-example that violates formula :");
439           MC_show_snapshot_stack(mc_snapshot_stack);
440           MC_dump_snapshot_stack(mc_snapshot_stack);
441           MC_print_statistics_pairs(mc_stats_pair);
442           exit(0);
443         }
444         
445         if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
446
447           //XBT_DEBUG("Unvisited pair !");
448
449           mc_stats_pair->executed_transitions++;
450  
451           MC_SET_RAW_MEM;
452           xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
453           MC_UNSET_RAW_MEM;
454
455           set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
456           MC_dfs(a, search_cycle, 0);
457
458           if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
459
460             MC_restore_snapshot(current_pair->system_state);
461             MC_UNSET_RAW_MEM;
462  
463             xbt_swag_foreach(process, simix_global->process_list){
464               if(MC_process_is_enabled(process)){
465                 //XBT_DEBUG("Pid : %lu", process->pid);
466                 MC_state_interleave_process(current_pair->graph_state, process);
467               }
468             }
469             
470             set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
471             XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
472             MC_dfs(a, 1, 1);
473
474           }
475         }
476       }
477     
478     }
479
480     
481     if(MC_state_interleave_size(current_pair->graph_state) > 0){
482       MC_restore_snapshot(current_snapshot);
483       MC_UNSET_RAW_MEM;
484       //XBT_DEBUG("Snapshot restored");
485     }
486   }
487
488   
489   MC_SET_RAW_MEM;
490   //remove_pair_reached(current_pair->graph_state);
491   xbt_fifo_shift(mc_snapshot_stack);
492   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
493   MC_UNSET_RAW_MEM;
494
495 }
496
497 void MC_show_snapshot_stack(xbt_fifo_t stack){
498   int value;
499   mc_pairs_t pair;
500   xbt_fifo_item_t item;
501   smx_req_t req;
502   char *req_str = NULL;
503   
504   for (item = xbt_fifo_get_last_item(stack);
505        (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
506         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
507     req = MC_state_get_executed_request(pair->graph_state, &value);
508     if(req){
509       req_str = MC_request_to_string(req, value);
510       XBT_INFO("%s", req_str);
511       xbt_free(req_str);
512     }
513   }
514 }
515
516 void MC_dump_snapshot_stack(xbt_fifo_t stack){
517   mc_pairs_t pair;
518
519   MC_SET_RAW_MEM;
520   while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
521     MC_pair_delete(pair);
522   MC_UNSET_RAW_MEM;
523 }
524
525 void MC_pair_delete(mc_pairs_t pair){
526   xbt_free(pair->graph_state->proc_status);
527   xbt_free(pair->graph_state);
528   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
529   xbt_free(pair);
530 }
531
532
533 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
534   
535   switch(l->type){
536   case 0 : {
537     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
538     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
539     return (left_res || right_res);
540     break;
541   }
542   case 1 : {
543     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
544     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
545     return (left_res && right_res);
546     break;
547   }
548   case 2 : {
549     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
550     return (!res);
551     break;
552   }
553   case 3 : { 
554     unsigned int cursor = 0;
555     xbt_propositional_symbol_t p = NULL;
556     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
557       if(strcmp(p->pred, l->u.predicat) == 0){
558         int (*f)() = p->function;
559         return (*f)();
560       }
561     }
562     return -1;
563     break;
564   }
565   case 4 : {
566     return 2;
567     break;
568   }
569   default : 
570     return -1;
571   }
572 }
573
574 /*void MC_dfs(xbt_automaton_t a, int search_cycle){
575
576   xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
577   xbt_transition_t transition_succ = NULL;
578   xbt_state_t successor = NULL;
579   unsigned int cursor = 0;
580   xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
581   int res;
582
583   //printf("++ current state : %s\n", current_state->id);
584
585   xbt_dynar_foreach(current_state->out, cursor, transition_succ){
586     successor = transition_succ->dst; 
587     res = MC_automaton_evaluate_label(a, transition_succ->label);
588     //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
589     if(res == 1){
590       if(search_cycle == 1 && reached_dfs != NULL){
591         if(strcmp(reached_dfs->id, successor->id) == 0){
592           xbt_dynar_push(state_automaton_visited_dfs, &successor); 
593           printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
594           printf("Visited states : \n");
595           unsigned int cursor2 = 0;
596           xbt_state_t visited_state = NULL;
597           xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
598             printf("State : %s\n", visited_state->id);
599           }
600           exit(1);
601         }
602       }
603       if(successor->visited == 0){
604         successor->visited = 1;
605         xbt_fifo_unshift(stack_automaton_dfs, successor);
606         xbt_dynar_push(state_automaton_visited_dfs, &successor);      
607         MC_dfs(a, search_cycle);
608         if(search_cycle == 0 && successor->type == 1){
609           reached_dfs = successor;
610           MC_dfs(a, 1);
611         }
612       }
613     }else{
614       if(res == 2){
615         xbt_dynar_push(elses,&transition_succ);
616       }
617     }
618   }
619   
620   cursor = 0;
621   xbt_dynar_foreach(elses, cursor, transition_succ){
622    successor = transition_succ->dst; 
623    if(search_cycle == 1 && reached_dfs != NULL){
624      if(strcmp(reached_dfs->id, successor->id) == 0){
625        xbt_dynar_push(state_automaton_visited_dfs, &successor); 
626        printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
627        printf("Visited states : \n");
628        unsigned int cursor2 = 0;
629        xbt_state_t visited_state = NULL;
630        xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
631          printf("State : %s\n", visited_state->id);
632        }
633        exit(1);
634      }
635    }
636    if(successor->visited == 0){
637      successor->visited = 1;
638      xbt_fifo_unshift(stack_automaton_dfs, successor);
639      xbt_dynar_push(state_automaton_visited_dfs, &successor);      
640      MC_dfs(a, search_cycle);
641      if(search_cycle == 0 && successor->type == 1){
642        reached_dfs = successor;
643        MC_dfs(a, 1);
644      }
645    }
646   }
647
648   xbt_fifo_shift(stack_automaton_dfs);
649   }*/
650
651
652 /* void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ */
653
654
655 /*   if(xbt_fifo_size(mc_snapshot_stack) == 0) */
656 /*     return; */
657
658 /*   if(restore == 1){ */
659 /*     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state); */
660 /*     MC_UNSET_RAW_MEM; */
661 /*   } */
662
663
664 /*   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); */
665
666 /*   /\* Get current state *\/ */
667 /*   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
668
669 /*   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); */
670 /*   XBT_DEBUG("State : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); */
671   
672 /*   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); */
673   
674 /*   //sleep(1); */
675
676 /*   smx_process_t process = NULL; */
677 /*   int value; */
678 /*   mc_state_t next_graph_state = NULL; */
679 /*   smx_req_t req = NULL; */
680 /*   char *req_str; */
681
682 /*   mc_pairs_t pair_succ; */
683 /*   xbt_transition_t transition_succ; */
684 /*   unsigned int cursor; */
685 /*   int res; */
686 /*   //int enabled_transition = 0; */
687
688 /*   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); */
689 /*   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);  */
690 /*   xbt_dynar_reset(all_successors); */
691
692 /*   mc_pairs_t next_pair; */
693 /*   mc_snapshot_t next_snapshot; */
694 /*   mc_snapshot_t current_snapshot; */
695   
696 /*   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ */
697
698 /*     //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); */
699 /*     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); */
700
701 /*     MC_SET_RAW_MEM; */
702 /*     current_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
703 /*     MC_take_snapshot(current_snapshot); */
704 /*     MC_UNSET_RAW_MEM; */
705    
706     
707 /*     /\* Debug information *\/ */
708 /*     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){ */
709 /*       req_str = MC_request_to_string(req, value); */
710 /*       XBT_DEBUG("Execute: %s", req_str); */
711 /*       xbt_free(req_str); */
712 /*     } */
713
714 /*     MC_state_set_executed_request(current_pair->graph_state, req, value); */
715 /*     //mc_stats->executed_transitions++; */
716
717 /*     /\* Answer the request *\/ */
718 /*     SIMIX_request_pre(req, value);  */
719
720 /*     /\* Wait for requests (schedules processes) *\/ */
721 /*     MC_wait_for_requests(); */
722
723
724 /*     /\* Create the new expanded graph_state *\/ */
725 /*     MC_SET_RAW_MEM; */
726
727 /*     next_graph_state = MC_state_new(); */
728     
729 /*     /\* Get enabled process and insert it in the interleave set of the next graph_state *\/ */
730 /*     xbt_swag_foreach(process, simix_global->process_list){ */
731 /*       if(MC_process_is_enabled(process)){ */
732 /*      MC_state_interleave_process(next_graph_state, process); */
733 /*       } */
734 /*     } */
735
736 /*     next_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
737 /*     MC_take_snapshot(next_snapshot); */
738       
739 /*     MC_UNSET_RAW_MEM; */
740
741 /*     xbt_dynar_reset(elses); */
742 /*     xbt_dynar_reset(successors); */
743     
744 /*     cursor = 0; */
745 /*     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ */
746
747 /*       res = MC_automaton_evaluate_label(a, transition_succ->label); */
748
749 /*       MC_SET_RAW_MEM; */
750 /*       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); */
751
752 /*       //XBT_DEBUG("Next pair : %p", next_pair); */
753         
754 /*       if(res == 1){ // enabled transition in automaton */
755 /*      xbt_dynar_push(successors, &next_pair);    */
756 /*      //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); */
757 /*       }else{ */
758 /*      if(res == 2){ */
759 /*        xbt_dynar_push(elses, &next_pair); */
760 /*        //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); */
761 /*      } */
762 /*       } */
763
764 /*       MC_UNSET_RAW_MEM; */
765 /*     } */
766
767    
768 /*     if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ */
769
770 /*       MC_SET_RAW_MEM; */
771 /*       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); */
772 /*       xbt_dynar_push(successors, &next_pair); */
773 /*       MC_UNSET_RAW_MEM; */
774         
775 /*     } */
776
777 /*     //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); */
778 /*     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); */
779
780 /*     if(xbt_dynar_length(successors) > 0){ */
781
782 /*       cursor = 0; */
783 /*       xbt_dynar_foreach(successors, cursor, pair_succ){ */
784 /*      MC_SET_RAW_MEM; */
785 /*      xbt_dynar_push(all_successors, &pair_succ); */
786 /*      MC_UNSET_RAW_MEM; */
787 /*       } */
788
789 /*     }else{  */
790
791 /*       cursor = 0; */
792 /*       xbt_dynar_foreach(elses, cursor, pair_succ){ */
793 /*      MC_SET_RAW_MEM; */
794 /*      xbt_dynar_push(all_successors, &pair_succ); */
795 /*      MC_UNSET_RAW_MEM; */
796 /*       } */
797
798 /*     }  */
799
800 /*     MC_restore_snapshot(current_snapshot); */
801 /*     MC_UNSET_RAW_MEM; */
802      
803 /*   }    */
804
805 /*   //XBT_DEBUG("All successors : %lu", xbt_dynar_length(all_successors)); */
806
807 /*   cursor = 0; */
808
809 /*   xbt_dynar_foreach(all_successors, cursor, pair_succ){ */
810
811 /*     if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ */
812 /*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
813 /*       XBT_INFO("|             ACCEPTANCE CYCLE            |"); */
814 /*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
815 /*       XBT_INFO("Counter-example that violates formula :"); */
816 /*       MC_show_snapshot_stack(mc_snapshot_stack); */
817 /*       MC_dump_snapshot_stack(mc_snapshot_stack); */
818 /*       exit(0); */
819 /*     } */
820         
821 /*     if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ */
822
823 /*       //XBT_DEBUG("New pair in stack"); */
824  
825 /*       MC_SET_RAW_MEM; */
826 /*       xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
827 /*       MC_UNSET_RAW_MEM; */
828
829 /*       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); */
830 /*       MC_dfs(a, search_cycle, 1); */
831
832 /*       if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ */
833             
834 /*      set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);  */
835 /*      XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); */
836 /*      MC_dfs(a, 1, 1); */
837
838 /*       } */
839 /*     }  */
840
841 /*   } */
842   
843 /*   MC_SET_RAW_MEM; */
844 /*   //remove_pair_reached(current_pair->graph_state); */
845 /*   xbt_fifo_shift(mc_snapshot_stack); */
846 /*   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); */
847 /*   MC_UNSET_RAW_MEM; */
848
849 /* } */