Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
117534f425d7951f0a77c2dc1780244dd1a155ac
[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
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
10                                 "Logging specific to algorithms for liveness properties verification");
11
12 xbt_dynar_t reached_pairs;
13 xbt_dynar_t reached_pairs_hash;
14 xbt_dynar_t visited_pairs;
15 xbt_dynar_t visited_pairs_hash;
16 xbt_dynar_t successors;
17
18 xbt_dynar_t hosts_table;
19
20
21 /* fast implementation of djb2 algorithm */
22 unsigned int hash_region(char *str, int str_len){
23
24   int c;
25   register unsigned int hash = 5381;
26
27   while (str_len--) {
28     c = *str++;
29     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
30   }
31
32   return hash;
33
34 }
35
36 int data_program_region_compare(void *d1, void *d2, size_t size){
37   int distance = 0;
38   int i;
39   char *pointed_address1 = NULL, *pointed_address2 = NULL;
40   
41   for(i=0; i<size; i++){
42     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
43       fprintf(stderr,"Different byte (offset=%d) (%p - %p) in data program region\n", i, (char *)d1 + i, (char *)d2 + i);
44       distance++;
45     }
46   }
47   
48   fprintf(stderr, "Hamming distance between data program regions : %d\n", distance);
49
50   free(pointed_address1);
51   free(pointed_address2);
52
53   return distance;
54 }
55
56 int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
57   int distance = 0;
58   int i;
59   char *pointed_address1 = NULL, *pointed_address2 = NULL;
60   
61   for(i=0; i<size; i++){
62     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
63       fprintf(stderr, "Different byte (offset=%d) (%p - %p) in data libsimgrid region\n", i, (char *)d1 + i, (char *)d2 + i);
64       distance++;
65     }
66   }
67   
68   fprintf(stderr, "Hamming distance between data libsimgrid regions : %d\n", distance);
69
70   free(pointed_address1);
71   free(pointed_address2);
72   
73   return distance;
74 }
75
76 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, void* s_heap, void* r_heap){
77
78   
79   if(s1->num_reg != s2->num_reg){
80     XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
81     return 1;
82   }
83
84   int i;
85   int errors = 0;
86
87   for(i=0 ; i< s1->num_reg ; i++){
88
89     if(s1->regions[i]->type != s2->regions[i]->type){
90         XBT_INFO("Different type of region");
91         errors++;
92     }
93
94     switch(s1->regions[i]->type){
95       case 0:
96       if(s1->regions[i]->size != s2->regions[i]->size){
97         XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
98         errors++;
99       }
100       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
101         XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
102         errors++;
103       }
104       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data, s_heap, r_heap)){
105         XBT_INFO("Different heap (mmalloc_compare)");
106         errors++; 
107       }
108       break;
109     case 1 :
110       if(s1->regions[i]->size != s2->regions[i]->size){
111         XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
112         errors++;
113       }
114       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
115         XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
116         errors++;
117       }
118       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
119         XBT_INFO("Different memcmp for data in libsimgrid");
120         errors++;
121       }
122       break;
123     case 2 :
124       if(s1->regions[i]->size != s2->regions[i]->size){
125         XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
126         errors++;
127       }
128       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
129         XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
130         errors++;
131       }
132       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
133         XBT_INFO("Different memcmp for data in program");
134         errors++;
135       }
136       break;
137     default:
138       break;
139     }
140   }
141
142   return (errors > 0);
143   
144 }
145
146 int reached(xbt_state_t st){
147
148
149   if(xbt_dynar_is_empty(reached_pairs)){
150
151     return 0;
152
153   }else{
154
155     MC_SET_RAW_MEM;
156
157     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
158     MC_take_snapshot_liveness(sn);    
159     
160     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
161     int res;
162     int_f_void_t f;
163
164     /* Get values of propositional symbols */
165     unsigned int cursor = 0;
166     xbt_propositional_symbol_t ps = NULL;
167     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
168       f = (int_f_void_t)ps->function;
169       res = (*f)();
170       xbt_dynar_push_as(prop_ato, int, res);
171     }
172
173     cursor = 0;
174     mc_pair_reached_t pair_test = NULL;
175
176     //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points();
177      
178     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
179       XBT_INFO("Pair reached #%d", pair_test->nb);
180       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
181         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
182           //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
183           //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
184           //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
185           if(snapshot_compare(pair_test->system_state, sn, std_heap, raw_heap) == 0){
186            
187             MC_free_snapshot(sn);
188             xbt_dynar_reset(prop_ato);
189             xbt_free(prop_ato);
190             MC_UNSET_RAW_MEM;
191             return 1;
192           }
193           /* }
194           }else{
195             XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
196             }*/
197         }else{
198           XBT_INFO("Different values of propositional symbols");
199         }
200       }else{
201         XBT_INFO("Different automaton state");
202       }
203     }
204
205     MC_free_snapshot(sn);
206     xbt_dynar_reset(prop_ato);
207     xbt_free(prop_ato);
208     MC_UNSET_RAW_MEM;
209     return 0;
210     
211   }
212 }
213
214 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */ 
215   
216    xbt_dict_cursor_t cursor_dict = NULL;
217    char *key;
218    char *data;
219    smx_rdv_t rdv1, rdv2;
220    xbt_fifo_item_t item1, item2;
221    smx_action_t action1, action2;
222    xbt_fifo_item_t item_req1, item_req2;
223    smx_simcall_t req1, req2;
224    int i=0;
225    int j=0;
226
227    xbt_dict_foreach(d1, cursor_dict, key, data){
228      rdv1 = (smx_rdv_t)data;
229      rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
230      if(rdv2 == NULL){
231        XBT_INFO("Rdv point unknown");
232        return 1;
233      }else{
234        if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
235          XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
236          return 1;
237        }else{
238          
239          XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); 
240          
241          item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);      
242          item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
243
244          while(i<xbt_fifo_size(rdv1->comm_fifo)){
245            action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
246            action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
247
248            if(action1->type != action2->type){
249              XBT_INFO("Different type of action");
250              return 1;
251            }
252
253            if(action1->state != action2->state){
254              XBT_INFO("Different state of action");
255              return 1;
256            }
257
258            if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
259              XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
260              return 1;
261            }else{
262
263              item_req1 = xbt_fifo_get_first_item(action1->simcalls);    
264              item_req2 = xbt_fifo_get_first_item(action2->simcalls);
265
266              while(j<xbt_fifo_size(action1->simcalls)){
267
268                req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
269                req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
270                
271                if(req1->call != req2->call){
272                  XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
273                  return 1;
274                }
275                if(req1->issuer->pid != req2->issuer->pid){
276                  XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
277                  return 1;
278                }
279
280                item_req1 = xbt_fifo_get_next_item(item_req1);   
281                item_req2 = xbt_fifo_get_next_item(item_req2);
282                j++;
283                
284              }
285            }
286
287            switch(action1->type){
288            case 0: /* execution */
289            case 1: /* parallel execution */
290              if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
291                return 1;
292              break;
293            case 2: /* comm */
294              if(action1->comm.type != action2->comm.type)
295                return 1;
296              //XBT_INFO("Type of comm : %d", action1->comm.type);
297              
298              switch(action1->comm.type){
299              case 0: /* SEND */
300                if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
301                  return 1;
302                if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
303                  return 1;
304                break;
305              case 1: /* RECEIVE */
306                if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
307                  return 1;
308                if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
309                  return 1;
310                break;
311              case 2: /* READY */
312                if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
313                  return 1;
314                if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
315                  return 1;
316                if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
317                  return 1;
318                if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
319                  return 1;
320                break;
321              case 3: /* DONE */
322                if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
323                  return 1;
324                if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
325                  return 1;
326                if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
327                  return 1;
328                if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
329                  return 1;
330                break;
331                
332              } /* end of switch on type of comm */
333              
334              if(action1->comm.refcount != action2->comm.refcount)
335                return 1;
336              if(action1->comm.detached != action2->comm.detached)
337                return 1;
338              if(action1->comm.rate != action2->comm.rate)
339                return 1;
340              if(action1->comm.task_size != action2->comm.task_size)
341                return 1;
342              if(action1->comm.src_buff != action2->comm.src_buff)
343                return 1;
344              if(action1->comm.dst_buff != action2->comm.dst_buff)
345                return 1;
346              if(action1->comm.src_data != action2->comm.src_data)
347                return 1;
348              if(action1->comm.dst_data != action2->comm.dst_data)
349                return 1;
350              
351              break;
352            case 3: /* sleep */
353              if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
354                return 1;
355              break;
356            case 4: /* synchro */
357              
358              break;
359            default:
360              break;
361            }
362
363            item1 = xbt_fifo_get_next_item(item1);       
364            item2 = xbt_fifo_get_next_item(item2);
365            i++;
366          }
367        }
368      }
369    }
370
371    return 0;
372    
373 }
374
375 void set_pair_reached(xbt_state_t st){
376
377  
378   MC_SET_RAW_MEM;
379   
380   mc_pair_reached_t pair = NULL;
381   pair = xbt_new0(s_mc_pair_reached_t, 1);
382   pair->nb = xbt_dynar_length(reached_pairs) + 1;
383   pair->automaton_state = st;
384   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
385   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
386   //pair->rdv_points = xbt_dict_new();  
387   MC_take_snapshot_liveness(pair->system_state);
388
389   /* Get values of propositional symbols */
390   unsigned int cursor = 0;
391   xbt_propositional_symbol_t ps = NULL;
392   int res;
393   int_f_void_t f;
394
395   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
396     f = (int_f_void_t)ps->function;
397     res = (*f)();
398     xbt_dynar_push_as(pair->prop_ato, int, res);
399   }
400
401   /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
402
403   xbt_dict_cursor_t cursor_dict = NULL;
404   char *key;
405   char *data;
406   xbt_fifo_item_t item;
407   smx_action_t action;
408
409   xbt_dict_foreach(rdv_points, cursor_dict, key, data){
410     smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
411     new_rdv->name = strdup(((smx_rdv_t)data)->name);
412     new_rdv->comm_fifo = xbt_fifo_new();
413     xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
414       smx_action_t a = xbt_new0(s_smx_action_t, 1);
415       memcpy(a, action, sizeof(s_smx_action_t));
416       xbt_fifo_push(new_rdv->comm_fifo, a);
417       XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
418       if(action->type==2)
419         XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
420     }
421     //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
422     xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
423     }*/
424  
425   xbt_dynar_push(reached_pairs, &pair); 
426
427   MC_UNSET_RAW_MEM;
428   
429 }
430
431
432 int reached_hash(xbt_state_t st){
433
434
435   if(xbt_dynar_is_empty(reached_pairs_hash)){
436
437     return 0;
438
439   }else{
440
441     MC_SET_RAW_MEM;
442
443     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
444     MC_take_snapshot_liveness(sn);
445
446     int j;
447     unsigned int hash_regions[sn->num_reg];
448     for(j=0; j<sn->num_reg; j++){
449       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
450     }
451
452
453     /* Get values of propositional symbols */
454     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
455     unsigned int cursor = 0;
456     xbt_propositional_symbol_t ps = NULL;
457     int res;
458     int_f_void_t f;
459
460     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
461       f = (int_f_void_t)ps->function;
462       res = (*f)();
463       xbt_dynar_push_as(prop_ato, int, res);
464     }
465
466     mc_pair_reached_hash_t pair_test = NULL;
467
468     int region_diff = 0;
469
470     cursor = 0;
471
472     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
473
474       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
475         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
476           for(j=0 ; j< sn->num_reg ; j++){
477             if(hash_regions[j] != pair_test->hash_regions[j]){
478               region_diff++;
479             }
480           }
481           if(region_diff == 0){
482             MC_free_snapshot(sn);
483             xbt_dynar_reset(prop_ato);
484             xbt_free(prop_ato);
485             MC_UNSET_RAW_MEM;
486             return 1;
487           }else{
488             XBT_INFO("Different snapshot");
489           }
490         }else{
491           XBT_INFO("Different values of propositional symbols");
492         }
493       }else{
494         XBT_INFO("Different automaton state");
495       }
496
497       region_diff = 0;
498     }
499     
500     MC_free_snapshot(sn);
501     xbt_dynar_reset(prop_ato);
502     xbt_free(prop_ato);
503     MC_UNSET_RAW_MEM;
504     return 0;
505     
506   }
507 }
508
509 void set_pair_reached_hash(xbt_state_t st){
510  
511   MC_SET_RAW_MEM;
512
513   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
514   MC_take_snapshot_liveness(sn);
515  
516   mc_pair_reached_hash_t pair = NULL;
517   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
518   pair->automaton_state = st;
519   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
520   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
521   
522   int i;
523
524   for(i=0 ; i< sn->num_reg ; i++){
525     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
526   }
527   
528   /* Get values of propositional symbols */
529   unsigned int cursor = 0;
530   xbt_propositional_symbol_t ps = NULL;
531   int res;
532   int_f_void_t f;
533
534   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
535     f = (int_f_void_t)ps->function;
536     res = (*f)();
537     xbt_dynar_push_as(pair->prop_ato, int, res);
538   }
539   
540   xbt_dynar_push(reached_pairs_hash, &pair);
541
542   MC_free_snapshot(sn);
543   
544   MC_UNSET_RAW_MEM;
545     
546 }
547
548
549 int visited(xbt_state_t st, int sc){
550
551
552   if(xbt_dynar_is_empty(visited_pairs)){
553
554     return 0;
555
556   }else{
557
558     MC_SET_RAW_MEM;
559
560     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
561     MC_take_snapshot_liveness(sn);
562
563     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
564
565     /* Get values of propositional symbols */
566     unsigned int cursor = 0;
567     xbt_propositional_symbol_t ps = NULL;
568     int res;
569     int_f_void_t f;
570
571     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
572       f = (int_f_void_t)ps->function;
573       res = (*f)();
574       xbt_dynar_push_as(prop_ato, int, res);
575     }
576
577     cursor = 0;
578     mc_pair_visited_t pair_test = NULL;
579
580     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
581       if(pair_test->search_cycle == sc) {
582         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
583           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
584             if(snapshot_compare(pair_test->system_state, sn, std_heap, raw_heap) == 0){
585             
586               MC_free_snapshot(sn);
587               xbt_dynar_reset(prop_ato);
588               xbt_free(prop_ato);
589               MC_UNSET_RAW_MEM;
590                 
591               return 1;
592         
593             }else{
594               XBT_INFO("Different snapshot");
595             }
596           }else{
597             XBT_INFO("Different values of propositional symbols"); 
598           }
599         }else{
600           XBT_INFO("Different automaton state");
601         }
602       }else{
603         XBT_INFO("Different value of search_cycle");
604       }
605     }
606
607
608     MC_free_snapshot(sn);
609     xbt_dynar_reset(prop_ato);
610     xbt_free(prop_ato);
611     MC_UNSET_RAW_MEM;
612     return 0;
613     
614   }
615 }
616
617
618 int visited_hash(xbt_state_t st, int sc){
619
620
621   if(xbt_dynar_is_empty(visited_pairs_hash)){
622
623     return 0;
624
625   }else{
626
627     MC_SET_RAW_MEM;
628
629     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
630     MC_take_snapshot_liveness(sn);
631
632     int j;
633     unsigned int hash_regions[sn->num_reg];
634     for(j=0; j<sn->num_reg; j++){
635       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
636     }
637
638     
639     /* Get values of propositional symbols */
640     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
641     unsigned int cursor = 0;
642     xbt_propositional_symbol_t ps = NULL;
643     int res;
644     int_f_void_t f;
645
646     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
647       f = (int_f_void_t)ps->function;
648       res = (*f)();
649       xbt_dynar_push_as(prop_ato, int, res);
650     }
651
652     mc_pair_visited_hash_t pair_test = NULL;
653
654     int region_diff = 0;
655     cursor = 0;
656
657     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
658   
659       if(pair_test->search_cycle == sc) {
660         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
661           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
662             for(j=0 ; j< sn->num_reg ; j++){
663               if(hash_regions[j] != pair_test->hash_regions[j]){
664                 region_diff++;
665               }
666             }
667             if(region_diff == 0){
668               MC_free_snapshot(sn);
669               xbt_dynar_reset(prop_ato);
670               xbt_free(prop_ato);
671               MC_UNSET_RAW_MEM;
672               return 1;
673             }else{
674               //XBT_INFO("Different snapshot");
675             }
676           }else{
677             //XBT_INFO("Different values of propositional symbols"); 
678           }
679         }else{
680           //XBT_INFO("Different automaton state");
681         }
682       }else{
683         //XBT_INFO("Different value of search_cycle");
684       }
685       
686       region_diff = 0;
687     }
688     
689     MC_free_snapshot(sn);
690     xbt_dynar_reset(prop_ato);
691     xbt_free(prop_ato);
692     MC_UNSET_RAW_MEM;
693     return 0;
694     
695   }
696 }
697
698 void set_pair_visited_hash(xbt_state_t st, int sc){
699  
700   MC_SET_RAW_MEM;
701
702   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
703   MC_take_snapshot_liveness(sn);
704  
705   mc_pair_visited_hash_t pair = NULL;
706   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
707   pair->automaton_state = st;
708   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
709   pair->search_cycle = sc;
710   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
711   
712   int i;
713
714   for(i=0 ; i< sn->num_reg ; i++){
715     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
716   }
717   
718   /* Get values of propositional symbols */
719   unsigned int cursor = 0;
720   xbt_propositional_symbol_t ps = NULL;
721   int res;
722   int_f_void_t f;
723
724   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
725     f = (int_f_void_t)ps->function;
726     res = (*f)();
727     xbt_dynar_push_as(pair->prop_ato, int, res);
728   }
729   
730   xbt_dynar_push(visited_pairs_hash, &pair);
731
732   MC_free_snapshot(sn);
733   
734   MC_UNSET_RAW_MEM;
735     
736 }
737
738 void set_pair_visited(xbt_state_t st, int sc){
739
740  
741   MC_SET_RAW_MEM;
742  
743   mc_pair_visited_t pair = NULL;
744   pair = xbt_new0(s_mc_pair_visited_t, 1);
745   pair->automaton_state = st;
746   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
747   pair->search_cycle = sc;
748   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
749   MC_take_snapshot_liveness(pair->system_state);
750
751
752   /* Get values of propositional symbols */
753   unsigned int cursor = 0;
754   xbt_propositional_symbol_t ps = NULL;
755   int res;
756   int_f_void_t f;
757
758   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
759     f = (int_f_void_t)ps->function;
760     res = (*f)();
761     xbt_dynar_push_as(pair->prop_ato, int, res);
762   }
763   
764   xbt_dynar_push(visited_pairs, &pair);
765   
766   MC_UNSET_RAW_MEM;
767   
768   
769 }
770
771 void MC_pair_delete(mc_pair_t pair){
772   xbt_free(pair->graph_state->proc_status);
773   xbt_free(pair->graph_state);
774   xbt_free(pair);
775 }
776
777
778
779 int MC_automaton_evaluate_label(xbt_exp_label_t l){
780   
781   switch(l->type){
782   case 0 : {
783     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
784     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
785     return (left_res || right_res);
786   }
787   case 1 : {
788     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
789     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
790     return (left_res && right_res);
791   }
792   case 2 : {
793     int res = MC_automaton_evaluate_label(l->u.exp_not);
794     return (!res);
795   }
796   case 3 : { 
797     unsigned int cursor = 0;
798     xbt_propositional_symbol_t p = NULL;
799     int_f_void_t f;
800     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
801       if(strcmp(p->pred, l->u.predicat) == 0){
802         f = (int_f_void_t)p->function;
803         return (*f)();
804       }
805     }
806     return -1;
807   }
808   case 4 : {
809     return 2;
810   }
811   default : 
812     return -1;
813   }
814 }
815
816
817 /********************* Double-DFS stateless *******************/
818
819 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
820   xbt_free(pair->graph_state->proc_status);
821   xbt_free(pair->graph_state);
822   xbt_free(pair);
823 }
824
825 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
826   mc_pair_stateless_t p = NULL;
827   p = xbt_new0(s_mc_pair_stateless_t, 1);
828   p->automaton_state = st;
829   p->graph_state = sg;
830   p->requests = r;
831   mc_stats_pair->expanded_pairs++;
832   return p;
833 }
834
835 void MC_ddfs_init(void){
836
837   XBT_INFO("**************************************************");
838   XBT_INFO("Double-DFS init");
839   XBT_INFO("**************************************************");
840
841   mc_pair_stateless_t mc_initial_pair = NULL;
842   mc_state_t initial_graph_state = NULL;
843   smx_process_t process; 
844
845  
846   MC_wait_for_requests();
847
848   MC_SET_RAW_MEM;
849
850   initial_graph_state = MC_state_pair_new();
851   xbt_swag_foreach(process, simix_global->process_list){
852     if(MC_process_is_enabled(process)){
853       MC_state_interleave_process(initial_graph_state, process);
854     }
855   }
856
857   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
858   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
859   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
860   visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
861   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
862
863   /* Save the initial state */
864   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
865   MC_take_snapshot_liveness(initial_snapshot_liveness);
866
867   MC_UNSET_RAW_MEM; 
868
869   unsigned int cursor = 0;
870   xbt_state_t state;
871
872   xbt_dynar_foreach(automaton->states, cursor, state){
873     if(state->type == -1){
874       
875       MC_SET_RAW_MEM;
876       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
877       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
878       MC_UNSET_RAW_MEM;
879       
880       if(cursor != 0){
881         MC_restore_snapshot(initial_snapshot_liveness);
882         MC_UNSET_RAW_MEM;
883       }
884
885       MC_ddfs(0);
886
887     }else{
888       if(state->type == 2){
889       
890         MC_SET_RAW_MEM;
891         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
892         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
893         MC_UNSET_RAW_MEM;
894
895         set_pair_reached(state);
896         //set_pair_reached_hash(state);
897
898         if(cursor != 0){
899           MC_restore_snapshot(initial_snapshot_liveness);
900           MC_UNSET_RAW_MEM;
901         }
902         
903         MC_ddfs(1);
904         
905       }
906     }
907   } 
908
909 }
910
911
912 void MC_ddfs(int search_cycle){
913
914   smx_process_t process;
915   mc_pair_stateless_t current_pair = NULL;
916
917   if(xbt_fifo_size(mc_stack_liveness) == 0)
918     return;
919
920
921   /* Get current pair */
922   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
923
924   /* Update current state in buchi automaton */
925   automaton->current_state = current_pair->automaton_state;
926
927  
928   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
929   XBT_INFO("Pair : 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));
930  
931   mc_stats_pair->visited_pairs++;
932
933   //sleep(1);
934
935   int value;
936   mc_state_t next_graph_state = NULL;
937   smx_simcall_t req = NULL;
938   char *req_str;
939
940   xbt_transition_t transition_succ;
941   unsigned int cursor = 0;
942   int res;
943
944   mc_pair_stateless_t next_pair = NULL;
945   mc_pair_stateless_t pair_succ;
946   
947   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
948
949     //set_pair_visited(current_pair->automaton_state, search_cycle);
950     set_pair_visited_hash(current_pair->automaton_state, search_cycle);
951
952     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
953     XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
954
955     if(current_pair->requests > 0){
956
957       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
958    
959         /* Debug information */
960
961         req_str = MC_request_to_string(req, value);
962         XBT_INFO("Execute: %s", req_str);
963         xbt_free(req_str);
964
965         MC_state_set_executed_request(current_pair->graph_state, req, value);   
966
967         /* Answer the request */
968         SIMIX_simcall_pre(req, value);
969
970         /* Wait for requests (schedules processes) */
971         MC_wait_for_requests();
972
973
974         MC_SET_RAW_MEM;
975
976         /* Create the new expanded graph_state */
977         next_graph_state = MC_state_pair_new();
978
979         /* Get enabled process and insert it in the interleave set of the next graph_state */
980         xbt_swag_foreach(process, simix_global->process_list){
981           if(MC_process_is_enabled(process)){
982             MC_state_interleave_process(next_graph_state, process);
983           }
984         }
985
986         xbt_dynar_reset(successors);
987
988         MC_UNSET_RAW_MEM;
989
990
991         cursor= 0;
992         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
993
994           res = MC_automaton_evaluate_label(transition_succ->label);
995
996           if(res == 1){ // enabled transition in automaton
997             MC_SET_RAW_MEM;
998             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
999             xbt_dynar_push(successors, &next_pair);
1000             MC_UNSET_RAW_MEM;
1001           }
1002
1003         }
1004
1005         cursor = 0;
1006    
1007         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1008       
1009           res = MC_automaton_evaluate_label(transition_succ->label);
1010         
1011           if(res == 2){ // true transition in automaton
1012             MC_SET_RAW_MEM;
1013             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1014             xbt_dynar_push(successors, &next_pair);
1015             MC_UNSET_RAW_MEM;
1016           }
1017
1018         }
1019
1020         cursor = 0; 
1021         
1022         xbt_dynar_foreach(successors, cursor, pair_succ){
1023
1024           if(search_cycle == 1){
1025
1026             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
1027                       
1028               if(reached(pair_succ->automaton_state)){
1029                 //if(reached_hash(pair_succ->automaton_state)){
1030               
1031                 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));
1032
1033                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1034                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
1035                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1036                 XBT_INFO("Counter-example that violates formula :");
1037                 MC_show_stack_liveness(mc_stack_liveness);
1038                 MC_dump_stack_liveness(mc_stack_liveness);
1039                 MC_print_statistics_pairs(mc_stats_pair);
1040                 exit(0);
1041
1042               }else{
1043
1044                 XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1045               
1046                 set_pair_reached(pair_succ->automaton_state);
1047                 //set_pair_reached_hash(pair_succ->automaton_state);
1048
1049                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1050                 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1051
1052                 MC_SET_RAW_MEM;
1053                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1054                 MC_UNSET_RAW_MEM;
1055                 
1056                 MC_ddfs(search_cycle);
1057
1058               }
1059
1060             }else{
1061
1062               if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1063                 //if(!visited(pair_succ->automaton_state, search_cycle)){
1064                 
1065                 MC_SET_RAW_MEM;
1066                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1067                 MC_UNSET_RAW_MEM;
1068                 
1069                 MC_ddfs(search_cycle);
1070                 
1071               }else{
1072
1073                 XBT_INFO("Next pair already visited ! ");
1074
1075               }
1076               
1077             }
1078
1079           }else{
1080           
1081             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1082
1083               XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1084             
1085               set_pair_reached(pair_succ->automaton_state); 
1086               //set_pair_reached_hash(pair_succ->automaton_state);
1087
1088               search_cycle = 1;
1089
1090               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1091               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1092
1093             }
1094
1095             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1096               //if(!visited(pair_succ->automaton_state, search_cycle)){
1097               
1098               MC_SET_RAW_MEM;
1099               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1100               MC_UNSET_RAW_MEM;
1101               
1102               MC_ddfs(search_cycle);
1103               
1104             }else{
1105
1106               XBT_INFO("Next pair already visited ! ");
1107
1108             }
1109
1110           }
1111
1112          
1113           /* Restore system before checking others successors */
1114           if(cursor != (xbt_dynar_length(successors) - 1))
1115             MC_replay_liveness(mc_stack_liveness, 1);
1116         
1117           
1118         }
1119
1120         if(MC_state_interleave_size(current_pair->graph_state) > 0){
1121           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
1122           MC_replay_liveness(mc_stack_liveness, 0);
1123         }
1124       }
1125
1126  
1127     }else{  /*No request to execute, search evolution in B├╝chi automaton */
1128
1129       MC_SET_RAW_MEM;
1130
1131       /* Create the new expanded graph_state */
1132       next_graph_state = MC_state_pair_new();
1133
1134       xbt_dynar_reset(successors);
1135
1136       MC_UNSET_RAW_MEM;
1137
1138
1139       cursor= 0;
1140       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1141
1142         res = MC_automaton_evaluate_label(transition_succ->label);
1143
1144         if(res == 1){ // enabled transition in automaton
1145           MC_SET_RAW_MEM;
1146           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1147           xbt_dynar_push(successors, &next_pair);
1148           MC_UNSET_RAW_MEM;
1149         }
1150
1151       }
1152
1153       cursor = 0;
1154    
1155       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1156       
1157         res = MC_automaton_evaluate_label(transition_succ->label);
1158         
1159         if(res == 2){ // true transition in automaton
1160           MC_SET_RAW_MEM;
1161           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1162           xbt_dynar_push(successors, &next_pair);
1163           MC_UNSET_RAW_MEM;
1164         }
1165
1166       }
1167
1168       cursor = 0; 
1169      
1170       xbt_dynar_foreach(successors, cursor, pair_succ){
1171
1172         if(search_cycle == 1){
1173
1174           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
1175
1176             if(reached(pair_succ->automaton_state)){
1177               //if(reached_hash(pair_succ->automaton_state)){
1178
1179               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1180               
1181               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1182               XBT_INFO("|             ACCEPTANCE CYCLE            |");
1183               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1184               XBT_INFO("Counter-example that violates formula :");
1185               MC_show_stack_liveness(mc_stack_liveness);
1186               MC_dump_stack_liveness(mc_stack_liveness);
1187               MC_print_statistics_pairs(mc_stats_pair);
1188               exit(0);
1189
1190             }else{
1191
1192               XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1193               
1194               set_pair_reached(pair_succ->automaton_state);
1195               //set_pair_reached_hash(pair_succ->automaton_state);
1196                 
1197               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1198               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1199
1200               MC_SET_RAW_MEM;
1201               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1202               MC_UNSET_RAW_MEM;
1203               
1204               MC_ddfs(search_cycle);
1205
1206             }
1207
1208           }else{
1209
1210             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1211               //if(!visited(pair_succ->automaton_state, search_cycle)){
1212
1213               MC_SET_RAW_MEM;
1214               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1215               MC_UNSET_RAW_MEM;
1216               
1217               MC_ddfs(search_cycle);
1218               
1219             }else{
1220
1221               XBT_INFO("Next pair already visited ! ");
1222
1223             }
1224           }
1225             
1226
1227         }else{
1228             
1229           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1230
1231             set_pair_reached(pair_succ->automaton_state);
1232             //set_pair_reached_hash(pair_succ->automaton_state);
1233                     
1234             search_cycle = 1;
1235
1236             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1237             //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1238
1239           }
1240
1241           if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1242             //if(!visited(pair_succ->automaton_state, search_cycle)){
1243
1244             MC_SET_RAW_MEM;
1245             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1246             MC_UNSET_RAW_MEM;
1247             
1248             MC_ddfs(search_cycle);
1249             
1250           }else{
1251
1252             XBT_INFO("Next pair already visited ! ");
1253
1254           }
1255
1256         }
1257
1258         /* Restore system before checking others successors */
1259         if(cursor != xbt_dynar_length(successors) - 1)
1260           MC_replay_liveness(mc_stack_liveness, 1);
1261
1262          
1263       }
1264            
1265     }
1266     
1267   }else{
1268     
1269     XBT_INFO("Max depth reached");
1270
1271   }
1272
1273   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1274     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1275   }else{
1276     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1277   }
1278
1279   
1280   MC_SET_RAW_MEM;
1281   xbt_fifo_shift(mc_stack_liveness);
1282   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1283     xbt_dynar_pop(reached_pairs, NULL);
1284     //xbt_dynar_pop(reached_pairs_hash, NULL);
1285   }
1286   MC_UNSET_RAW_MEM;
1287   
1288   
1289
1290 }