model-checker : cosmetics reindent

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 145af27..31927b8 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -42,15 +42,15 @@ static void MC_region_restore(mc_mem_region_t reg)
     while(i < maps->mapsize){
       r = maps->regions[i];
       if (maps->regions[i].pathname != NULL){
     while(i < maps->mapsize){
       r = maps->regions[i];
       if (maps->regions[i].pathname != NULL){

-  if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){
-    size_t diff = (char*)reg->start_addr - (char*)r.start_addr;
-    void *segment = malloc(reg->size + diff);
-    XBT_DEBUG("Size of segment : %zu", sizeof(segment));
-    memcpy((char *)segment + diff, reg->data, reg->size);
-    memcpy(r.start_addr, segment, sizeof(segment));
-    XBT_DEBUG("Memcpy region ok");
-    break;
-  }
+        if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){
+          size_t diff = (char*)reg->start_addr - (char*)r.start_addr;
+          void *segment = malloc(reg->size + diff);
+          XBT_DEBUG("Size of segment : %zu", sizeof(segment));
+          memcpy((char *)segment + diff, reg->data, reg->size);
+          memcpy(r.start_addr, segment, sizeof(segment));
+          XBT_DEBUG("Memcpy region ok");
+          break;
+        }

       }
       i++;
     }
       }
       i++;
     }


@@ -134,16 +134,16 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
     if ((reg.prot & PROT_WRITE)){
       if (maps->regions[i].pathname == NULL){
         if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one)
     if ((reg.prot & PROT_WRITE)){
       if (maps->regions[i].pathname == NULL){
         if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one)

-    MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+          MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);

         }
       } else {
         if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
           MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
         } else {
         }
       } else {
         if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
           MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
         } else {

-    if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
-      MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
-    } 
-  }
+          if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
+            MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
+          } 
+        }

       }
     }
     i++;
       }
     }
     i++;

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index d45cf36..6b737a4 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -39,8 +39,8 @@ void MC_dpor_init()
   MC_UNSET_RAW_MEM;
     
   /* FIXME: Update Statistics 
   MC_UNSET_RAW_MEM;
     
   /* FIXME: Update Statistics 

-  mc_stats->state_size +=
-      xbt_setset_set_size(initial_state->enabled_transitions); */
+     mc_stats->state_size +=
+     xbt_setset_set_size(initial_state->enabled_transitions); */

 }
 
 
 }
 
 


@@ -65,8 +65,8 @@ void MC_dpor(void)
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",

-           xbt_fifo_size(mc_stack_safety_stateless), state,
-           MC_state_interleave_size(state));
+              xbt_fifo_size(mc_stack_safety_stateless), state,
+              MC_state_interleave_size(state));

 
     /* Update statistics */
     mc_stats->visited_states++;
 
     /* Update statistics */
     mc_stats->visited_states++;


@@ -107,8 +107,8 @@ void MC_dpor(void)
       MC_UNSET_RAW_MEM;
 
       /* FIXME: Update Statistics
       MC_UNSET_RAW_MEM;
 
       /* FIXME: Update Statistics

-      mc_stats->state_size +=
-          xbt_setset_set_size(next_state->enabled_transitions);*/
+         mc_stats->state_size +=
+         xbt_setset_set_size(next_state->enabled_transitions);*/

 
       /* Let's loop again */
 
 
       /* Let's loop again */
 


@@ -258,10 +258,10 @@ void MC_dpor_stateful(){
 
       /* Debug information */
       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
 
       /* Debug information */
       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){

-  req_str = MC_request_to_string(req, value);
-  //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
-  XBT_DEBUG("Execute: %s",req_str);
-  xbt_free(req_str);
+        req_str = MC_request_to_string(req, value);
+        //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
+        XBT_DEBUG("Execute: %s",req_str);
+        xbt_free(req_str);

       }
 
       MC_state_set_executed_request(current_state->graph_state, req, value);
       }
 
       MC_state_set_executed_request(current_state->graph_state, req, value);


@@ -280,10 +280,10 @@ void MC_dpor_stateful(){
       
       /* Get an enabled process and insert it in the interleave set of the next graph_state */
       xbt_swag_foreach(process, simix_global->process_list){
       
       /* Get an enabled process and insert it in the interleave set of the next graph_state */
       xbt_swag_foreach(process, simix_global->process_list){

-  if(MC_process_is_enabled(process)){
-    MC_state_interleave_process(next_graph_state, process);
-    break;
-  }
+        if(MC_process_is_enabled(process)){
+          MC_state_interleave_process(next_graph_state, process);
+          break;
+        }

       }
 
       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
       }
 
       next_snapshot = xbt_new0(s_mc_snapshot_t, 1);


@@ -310,8 +310,8 @@ void MC_dpor_stateful(){
 
       MC_SET_RAW_MEM;
       while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
 
       MC_SET_RAW_MEM;
       while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){

-  req = MC_state_get_internal_request(current_state->graph_state);
-  xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
+        req = MC_state_get_internal_request(current_state->graph_state);
+        xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {

           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
               XBT_DEBUG("Dependent Transitions:");
           if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
               XBT_DEBUG("Dependent Transitions:");


@@ -328,21 +328,21 @@ void MC_dpor_stateful(){
             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
               MC_state_interleave_process(prev_state->graph_state, req->issuer);
         
             if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
               MC_state_interleave_process(prev_state->graph_state, req->issuer);
         

-      } else {
+            } else {

               XBT_DEBUG("Process %p is in done set", req->issuer);
               XBT_DEBUG("Process %p is in done set", req->issuer);

-      }
+            }

 
             break;
           }
         }
 
 
             break;
           }
         }
 

-  if(MC_state_interleave_size(current_state->graph_state)){
-    MC_restore_snapshot(current_state->system_state);
-    xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
-    XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
-    MC_UNSET_RAW_MEM;
-    break;
-  }
+        if(MC_state_interleave_size(current_state->graph_state)){
+          MC_restore_snapshot(current_state->system_state);
+          xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
+          XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
+          MC_UNSET_RAW_MEM;
+          break;
+        }

       }
 
       MC_UNSET_RAW_MEM;
       }
 
       MC_UNSET_RAW_MEM;

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 62accca..f55b44f 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -80,7 +80,7 @@ void MC_init_safety_stateless(void)
 void MC_init_safety_stateful(void){
 
   
 void MC_init_safety_stateful(void){
 
   

-   /* Check if MC is already initialized */
+  /* Check if MC is already initialized */

   if (initial_snapshot)
     return;
 
   if (initial_snapshot)
     return;
 


@@ -120,7 +120,7 @@ static void MC_init_liveness(xbt_automaton_t a){
 
   XBT_DEBUG("Creating stack");
 
 
   XBT_DEBUG("Creating stack");
 

- /* Create exploration stack */
+  /* Create exploration stack */

   mc_stack_liveness = xbt_fifo_new();
 
   MC_UNSET_RAW_MEM;
   mc_stack_liveness = xbt_fifo_new();
 
   MC_UNSET_RAW_MEM;


@@ -190,7 +190,7 @@ void MC_wait_for_requests(void)
     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
       req = &process->simcall;
       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
       req = &process->simcall;
       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))

-          SIMIX_simcall_pre(req, 0);
+        SIMIX_simcall_pre(req, 0);

     }
   }
 }
     }
   }
 }


@@ -216,7 +216,7 @@ int MC_deadlock_check()
  * \brief Re-executes from the initial state all the transitions indicated by
  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.
  * \brief Re-executes from the initial state all the transitions indicated by
  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.

-*/
+ */

 void MC_replay(xbt_fifo_t stack)
 {
   int value;
 void MC_replay(xbt_fifo_t stack)
 {
   int value;


@@ -293,26 +293,26 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
       if(pair->requests > 0){
    
 
       if(pair->requests > 0){
    

-  saved_req = MC_state_get_executed_request(state, &value);
-  //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+        saved_req = MC_state_get_executed_request(state, &value);
+        //XBT_DEBUG("SavedReq->call %u", saved_req->call);

       
       

-  if(saved_req != NULL){
-    /* because we got a copy of the executed request, we have to fetch the  
-       real one, pointed by the request field of the issuer process */
-    req = &saved_req->issuer->simcall;
-    //XBT_DEBUG("Req->call %u", req->call);
+        if(saved_req != NULL){
+          /* because we got a copy of the executed request, we have to fetch the  
+             real one, pointed by the request field of the issuer process */
+          req = &saved_req->issuer->simcall;
+          //XBT_DEBUG("Req->call %u", req->call);

   
   

-    /* Debug information */
-    if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
-      req_str = MC_request_to_string(req, value);
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-      xbt_free(req_str);
-    }
+          /* Debug information */
+          if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+            req_str = MC_request_to_string(req, value);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }

   
   

-  }
+        }

  
  

-  SIMIX_simcall_pre(req, value);
-  MC_wait_for_requests();
+        SIMIX_simcall_pre(req, value);
+        MC_wait_for_requests();

       }
 
       depth++;
       }
 
       depth++;


@@ -327,34 +327,34 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
     /* Traverse the stack from the initial state and re-execute the transitions */
     for (item = xbt_fifo_get_last_item(stack);
 
     /* Traverse the stack from the initial state and re-execute the transitions */
     for (item = xbt_fifo_get_last_item(stack);

-   item != xbt_fifo_get_first_item(stack);
-   item = xbt_fifo_get_prev_item(item)) {
+         item != xbt_fifo_get_first_item(stack);
+         item = xbt_fifo_get_prev_item(item)) {

 
       pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){
    
 
       pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){
    

-  saved_req = MC_state_get_executed_request(state, &value);
-  //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+        saved_req = MC_state_get_executed_request(state, &value);
+        //XBT_DEBUG("SavedReq->call %u", saved_req->call);

       
       

-  if(saved_req != NULL){
-    /* because we got a copy of the executed request, we have to fetch the  
-       real one, pointed by the request field of the issuer process */
-    req = &saved_req->issuer->simcall;
-    //XBT_DEBUG("Req->call %u", req->call);
+        if(saved_req != NULL){
+          /* because we got a copy of the executed request, we have to fetch the  
+             real one, pointed by the request field of the issuer process */
+          req = &saved_req->issuer->simcall;
+          //XBT_DEBUG("Req->call %u", req->call);

   
   

-    /* Debug information */
-    if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
-      req_str = MC_request_to_string(req, value);
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-      xbt_free(req_str);
-    }
+          /* Debug information */
+          if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+            req_str = MC_request_to_string(req, value);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }

   
   

-  }
+        }

  
  

-  SIMIX_simcall_pre(req, value);
-  MC_wait_for_requests();
+        SIMIX_simcall_pre(req, value);
+        MC_wait_for_requests();

       }
 
       depth++;
       }
 
       depth++;


@@ -372,7 +372,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
  * \brief Dumps the contents of a model-checker's stack and shows the actual
  *        execution trace
  * \param stack The stack to dump
  * \brief Dumps the contents of a model-checker's stack and shows the actual
  *        execution trace
  * \param stack The stack to dump

-*/
+ */

 void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
 {
   mc_state_t state;
 void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
 {
   mc_state_t state;


@@ -414,8 +414,8 @@ void MC_show_deadlock(smx_simcall_t req)
   XBT_INFO("**************************");
   XBT_INFO("Locked request:");
   /*req_str = MC_request_to_string(req);
   XBT_INFO("**************************");
   XBT_INFO("Locked request:");
   /*req_str = MC_request_to_string(req);

-  XBT_INFO("%s", req_str);
-  xbt_free(req_str);*/
+    XBT_INFO("%s", req_str);
+    xbt_free(req_str);*/

   XBT_INFO("Counter-example execution trace:");
   MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 }
   XBT_INFO("Counter-example execution trace:");
   MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 }


@@ -428,8 +428,8 @@ void MC_show_deadlock_stateful(smx_simcall_t req)
   XBT_INFO("**************************");
   XBT_INFO("Locked request:");
   /*req_str = MC_request_to_string(req);
   XBT_INFO("**************************");
   XBT_INFO("Locked request:");
   /*req_str = MC_request_to_string(req);

-  XBT_INFO("%s", req_str);
-  xbt_free(req_str);*/
+    XBT_INFO("%s", req_str);
+    xbt_free(req_str);*/

   XBT_INFO("Counter-example execution trace:");
   MC_show_stack_safety_stateful(mc_stack_safety_stateful);
 }
   XBT_INFO("Counter-example execution trace:");
   MC_show_stack_safety_stateful(mc_stack_safety_stateful);
 }


@@ -441,7 +441,7 @@ void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
   MC_show_stack_safety_stateful(stack);
 
   /*MC_SET_RAW_MEM;
   MC_show_stack_safety_stateful(stack);
 
   /*MC_SET_RAW_MEM;

-  while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)

     MC_state_delete(state);
     MC_UNSET_RAW_MEM;*/
 }
     MC_state_delete(state);
     MC_UNSET_RAW_MEM;*/
 }


@@ -481,11 +481,11 @@ void MC_show_stack_liveness(xbt_fifo_t stack){
     req = MC_state_get_executed_request(pair->graph_state, &value);
     if(req){
       if(pair->requests>0){
     req = MC_state_get_executed_request(pair->graph_state, &value);
     if(req){
       if(pair->requests>0){

-  req_str = MC_request_to_string(req, value);
-  XBT_INFO("%s", req_str);
-  xbt_free(req_str);
+        req_str = MC_request_to_string(req, value);
+        XBT_INFO("%s", req_str);
+        xbt_free(req_str);

       }else{
       }else{

-  XBT_INFO("End of system requests but evolution in Büchi automaton");
+        XBT_INFO("End of system requests but evolution in Büchi automaton");

       }
     }
   }
       }
     }
   }


@@ -508,9 +508,9 @@ void MC_print_statistics(mc_stats_t stats)
   XBT_INFO("Visited states = %lu", stats->visited_states);
   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
   XBT_INFO("Expanded / Visited = %lf",
   XBT_INFO("Visited states = %lu", stats->visited_states);
   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
   XBT_INFO("Expanded / Visited = %lf",

-        (double) stats->visited_states / stats->expanded_states);
+           (double) stats->visited_states / stats->expanded_states);

   /*XBT_INFO("Exploration coverage = %lf",
   /*XBT_INFO("Exploration coverage = %lf",

-     (double)stats->expanded_states / stats->state_size); */
+    (double)stats->expanded_states / stats->state_size); */

 }
 
 void MC_print_statistics_pairs(mc_stats_pair_t stats)
 }
 
 void MC_print_statistics_pairs(mc_stats_pair_t stats)


@@ -519,9 +519,9 @@ void MC_print_statistics_pairs(mc_stats_pair_t stats)
   XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
   //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
   XBT_INFO("Expanded / Visited = %lf",
   XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
   //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
   XBT_INFO("Expanded / Visited = %lf",

-        (double) stats->visited_pairs / stats->expanded_pairs);
+           (double) stats->visited_pairs / stats->expanded_pairs);

   /*XBT_INFO("Exploration coverage = %lf",
   /*XBT_INFO("Exploration coverage = %lf",

-     (double)stats->expanded_states / stats->state_size); */
+    (double)stats->expanded_states / stats->state_size); */

 }
 
 void MC_assert(int prop)
 }
 
 void MC_assert(int prop)


@@ -610,5 +610,8 @@ void MC_diff(void){
 }
 
 xbt_automaton_t MC_create_automaton(const char *file){
 }
 
 xbt_automaton_t MC_create_automaton(const char *file){

-  return xbt_create_automaton(file);
+  MC_SET_RAW_MEM;
+  xbt_automaton_t a = xbt_create_automaton(file);
+  MC_UNSET_RAW_MEM;
+  return a;

 }
 }

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index b7ad897..a49dbfb 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -79,51 +79,51 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   for(i=0 ; i< s1->num_reg ; i++){
 
     if(s1->regions[i]->type != s2->regions[i]->type){
   for(i=0 ; i< s1->num_reg ; i++){
 
     if(s1->regions[i]->type != s2->regions[i]->type){

-  XBT_INFO("Different type of region");
-  errors++;
+      XBT_INFO("Different type of region");
+      errors++;

     }
 
     switch(s1->regions[i]->type){
     }
 
     switch(s1->regions[i]->type){

-      case 0:
+    case 0:

       if(s1->regions[i]->size != s2->regions[i]->size){
       if(s1->regions[i]->size != s2->regions[i]->size){

-  XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-  errors++;
+        XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+        errors++;

       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){

-  XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-  errors++;
+        XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+        errors++;

       }
       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
       }
       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){

-  XBT_INFO("Different heap (mmalloc_compare)");
-  errors++; 
+        XBT_INFO("Different heap (mmalloc_compare)");
+        errors++; 

       }
       break;
     case 1 :
       if(s1->regions[i]->size != s2->regions[i]->size){
       }
       break;
     case 1 :
       if(s1->regions[i]->size != s2->regions[i]->size){

-  XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-  errors++;
+        XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+        errors++;

       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){

-  XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-  errors++;
+        XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+        errors++;

       }
       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
       }
       if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){

-  XBT_INFO("Different memcmp for data in libsimgrid");
-  errors++;
+        XBT_INFO("Different memcmp for data in libsimgrid");
+        errors++;

       }
       break;
     case 2 :
       if(s1->regions[i]->size != s2->regions[i]->size){
       }
       break;
     case 2 :
       if(s1->regions[i]->size != s2->regions[i]->size){

-  XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
-  errors++;
+        XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
+        errors++;

       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
       }
       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){

-  XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
-  errors++;
+        XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
+        errors++;

       }
       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
       }
       if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){

-  XBT_INFO("Different memcmp for data in program");
-  errors++;
+        XBT_INFO("Different memcmp for data in program");
+        errors++;

       }
       break;
     default:
       }
       break;
     default:


@@ -170,27 +170,27 @@ int reached(xbt_state_t st){
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
       XBT_INFO("Pair reached #%d", pair_test->nb);
       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
       XBT_INFO("Pair reached #%d", pair_test->nb);
       if(automaton_state_compare(pair_test->automaton_state, st) == 0){

-  if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-    //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
-    //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
-    //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
-    if(snapshot_compare(pair_test->system_state, sn) == 0){
+        if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+          //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
+          //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
+          //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
+          if(snapshot_compare(pair_test->system_state, sn) == 0){

      
      

-      MC_free_snapshot(sn);
-      xbt_dynar_reset(prop_ato);
-      xbt_free(prop_ato);
-      MC_UNSET_RAW_MEM;
-      return 1;
-    }
-    /* }
-    }else{
-      XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
-      }*/
-  }else{
-    XBT_INFO("Different values of propositional symbols");
-  }
+            MC_free_snapshot(sn);
+            xbt_dynar_reset(prop_ato);
+            xbt_free(prop_ato);
+            MC_UNSET_RAW_MEM;
+            return 1;
+          }
+          /* }
+             }else{
+             XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
+             }*/
+        }else{
+          XBT_INFO("Different values of propositional symbols");
+        }

       }else{
       }else{

-  XBT_INFO("Different automaton state");
+        XBT_INFO("Different automaton state");

       }
     }
 
       }
     }
 


@@ -205,162 +205,162 @@ int reached(xbt_state_t st){
 
 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */ 
   
 
 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */ 
   

-   xbt_dict_cursor_t cursor_dict = NULL;
-   char *key;
-   char *data;
-   smx_rdv_t rdv1, rdv2;
-   xbt_fifo_item_t item1, item2;
-   smx_action_t action1, action2;
-   xbt_fifo_item_t item_req1, item_req2;
-   smx_simcall_t req1, req2;
-   int i=0;
-   int j=0;
-
-   xbt_dict_foreach(d1, cursor_dict, key, data){
-     rdv1 = (smx_rdv_t)data;
-     rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
-     if(rdv2 == NULL){
-       XBT_INFO("Rdv point unknown");
-       return 1;
-     }else{
-       if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
-   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) );
-   return 1;
-       }else{
+  xbt_dict_cursor_t cursor_dict = NULL;
+  char *key;
+  char *data;
+  smx_rdv_t rdv1, rdv2;
+  xbt_fifo_item_t item1, item2;
+  smx_action_t action1, action2;
+  xbt_fifo_item_t item_req1, item_req2;
+  smx_simcall_t req1, req2;
+  int i=0;
+  int j=0;
+
+  xbt_dict_foreach(d1, cursor_dict, key, data){
+    rdv1 = (smx_rdv_t)data;
+    rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
+    if(rdv2 == NULL){
+      XBT_INFO("Rdv point unknown");
+      return 1;
+    }else{
+      if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
+        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) );
+        return 1;
+      }else{

    
    

-   XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); 
+        XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); 

    
    

-   item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);  
-   item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
+        item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);  
+        item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);

 
 

-   while(i<xbt_fifo_size(rdv1->comm_fifo)){
-     action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
-     action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
+        while(i<xbt_fifo_size(rdv1->comm_fifo)){
+          action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
+          action2 = (smx_action_t) xbt_fifo_get_item_content(item2);

 
 

-     if(action1->type != action2->type){
-       XBT_INFO("Different type of action");
-       return 1;
-     }
+          if(action1->type != action2->type){
+            XBT_INFO("Different type of action");
+            return 1;
+          }

 
 

-     if(action1->state != action2->state){
-       XBT_INFO("Different state of action");
-       return 1;
-     }
+          if(action1->state != action2->state){
+            XBT_INFO("Different state of action");
+            return 1;
+          }

 
 

-     if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
-       XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
-       return 1;
-     }else{
+          if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
+            XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
+            return 1;
+          }else{

 
 

-       item_req1 = xbt_fifo_get_first_item(action1->simcalls);  
-       item_req2 = xbt_fifo_get_first_item(action2->simcalls);
+            item_req1 = xbt_fifo_get_first_item(action1->simcalls);  
+            item_req2 = xbt_fifo_get_first_item(action2->simcalls);

 
 

-       while(j<xbt_fifo_size(action1->simcalls)){
+            while(j<xbt_fifo_size(action1->simcalls)){

 
 

-         req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
-         req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
+              req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
+              req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);

          
          

-         if(req1->call != req2->call){
-     XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
-     return 1;
-         }
-         if(req1->issuer->pid != req2->issuer->pid){
-     XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
-     return 1;
-         }
-
-         item_req1 = xbt_fifo_get_next_item(item_req1);  
-         item_req2 = xbt_fifo_get_next_item(item_req2);
-         j++;
+              if(req1->call != req2->call){
+                XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
+                return 1;
+              }
+              if(req1->issuer->pid != req2->issuer->pid){
+                XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
+                return 1;
+              }
+
+              item_req1 = xbt_fifo_get_next_item(item_req1);  
+              item_req2 = xbt_fifo_get_next_item(item_req2);
+              j++;

          
          

-       }
-     }
-
-     switch(action1->type){
-     case 0: /* execution */
-     case 1: /* parallel execution */
-       if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
-         return 1;
-       break;
-     case 2: /* comm */
-       if(action1->comm.type != action2->comm.type)
-         return 1;
-       //XBT_INFO("Type of comm : %d", action1->comm.type);
+            }
+          }
+
+          switch(action1->type){
+          case 0: /* execution */
+          case 1: /* parallel execution */
+            if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
+              return 1;
+            break;
+          case 2: /* comm */
+            if(action1->comm.type != action2->comm.type)
+              return 1;
+            //XBT_INFO("Type of comm : %d", action1->comm.type);

        
        

-       switch(action1->comm.type){
-       case 0: /* SEND */
-         if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
-     return 1;
-         if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
-     return 1;
-         break;
-       case 1: /* RECEIVE */
-         if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
-     return 1;
-         if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
-     return 1;
-         break;
-       case 2: /* READY */
-         if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
-     return 1;
-         if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
-     return 1;
-         if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
-     return 1;
-         if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
-     return 1;
-         break;
-       case 3: /* DONE */
-         if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
-     return 1;
-         if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
-     return 1;
-         if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
-     return 1;
-         if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
-     return 1;
-         break;
+            switch(action1->comm.type){
+            case 0: /* SEND */
+              if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
+                return 1;
+              if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
+                return 1;
+              break;
+            case 1: /* RECEIVE */
+              if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
+                return 1;
+              if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
+                return 1;
+              break;
+            case 2: /* READY */
+              if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
+                return 1;
+              if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
+                return 1;
+              if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
+                return 1;
+              if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
+                return 1;
+              break;
+            case 3: /* DONE */
+              if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
+                return 1;
+              if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
+                return 1;
+              if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
+                return 1;
+              if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
+                return 1;
+              break;

          
          

-       } /* end of switch on type of comm */
+            } /* end of switch on type of comm */

        
        

-       if(action1->comm.refcount != action2->comm.refcount)
-         return 1;
-       if(action1->comm.detached != action2->comm.detached)
-         return 1;
-       if(action1->comm.rate != action2->comm.rate)
-         return 1;
-       if(action1->comm.task_size != action2->comm.task_size)
-         return 1;
-       if(action1->comm.src_buff != action2->comm.src_buff)
-         return 1;
-       if(action1->comm.dst_buff != action2->comm.dst_buff)
-         return 1;
-       if(action1->comm.src_data != action2->comm.src_data)
-         return 1;
-       if(action1->comm.dst_data != action2->comm.dst_data)
-         return 1;
+            if(action1->comm.refcount != action2->comm.refcount)
+              return 1;
+            if(action1->comm.detached != action2->comm.detached)
+              return 1;
+            if(action1->comm.rate != action2->comm.rate)
+              return 1;
+            if(action1->comm.task_size != action2->comm.task_size)
+              return 1;
+            if(action1->comm.src_buff != action2->comm.src_buff)
+              return 1;
+            if(action1->comm.dst_buff != action2->comm.dst_buff)
+              return 1;
+            if(action1->comm.src_data != action2->comm.src_data)
+              return 1;
+            if(action1->comm.dst_data != action2->comm.dst_data)
+              return 1;

        
        

-       break;
-     case 3: /* sleep */
-       if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
-         return 1;
-       break;
-     case 4: /* synchro */
+            break;
+          case 3: /* sleep */
+            if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
+              return 1;
+            break;
+          case 4: /* synchro */

        
        

-       break;
-     default:
-       break;
-     }
-
-     item1 = xbt_fifo_get_next_item(item1);  
-     item2 = xbt_fifo_get_next_item(item2);
-     i++;
-   }
-       }
-     }
-   }
-
-   return 0;
+            break;
+          default:
+            break;
+          }
+
+          item1 = xbt_fifo_get_next_item(item1);  
+          item2 = xbt_fifo_get_next_item(item2);
+          i++;
+        }
+      }
+    }
+  }
+
+  return 0;

    
 }
 
    
 }
 


@@ -392,23 +392,23 @@ void set_pair_reached(xbt_state_t st){
 
   /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
 
 
   /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
 

-  xbt_dict_cursor_t cursor_dict = NULL;
-  char *key;
-  char *data;
-  xbt_fifo_item_t item;
-  smx_action_t action;
+    xbt_dict_cursor_t cursor_dict = NULL;
+    char *key;
+    char *data;
+    xbt_fifo_item_t item;
+    smx_action_t action;

 
 

-  xbt_dict_foreach(rdv_points, cursor_dict, key, data){
+    xbt_dict_foreach(rdv_points, cursor_dict, key, data){

     smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
     new_rdv->name = strdup(((smx_rdv_t)data)->name);
     new_rdv->comm_fifo = xbt_fifo_new();
     xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
     smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
     new_rdv->name = strdup(((smx_rdv_t)data)->name);
     new_rdv->comm_fifo = xbt_fifo_new();
     xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {

-      smx_action_t a = xbt_new0(s_smx_action_t, 1);
-      memcpy(a, action, sizeof(s_smx_action_t));
-      xbt_fifo_push(new_rdv->comm_fifo, a);
-      XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
-      if(action->type==2)
-  XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
+    smx_action_t a = xbt_new0(s_smx_action_t, 1);
+    memcpy(a, action, sizeof(s_smx_action_t));
+    xbt_fifo_push(new_rdv->comm_fifo, a);
+    XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
+    if(action->type==2)
+    XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);

     }
     //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
     xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
     }
     //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
     xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);


@@ -464,26 +464,26 @@ int reached_hash(xbt_state_t st){
     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 
       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 
       if(automaton_state_compare(pair_test->automaton_state, st) == 0){

-  if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-    for(j=0 ; j< sn->num_reg ; j++){
-      if(hash_regions[j] != pair_test->hash_regions[j]){
-        region_diff++;
-      }
-    }
-    if(region_diff == 0){
-      MC_free_snapshot(sn);
-      xbt_dynar_reset(prop_ato);
-      xbt_free(prop_ato);
-      MC_UNSET_RAW_MEM;
-      return 1;
-    }else{
-      XBT_INFO("Different snapshot");
-    }
-  }else{
-    XBT_INFO("Different values of propositional symbols");
-  }
+        if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+          for(j=0 ; j< sn->num_reg ; j++){
+            if(hash_regions[j] != pair_test->hash_regions[j]){
+              region_diff++;
+            }
+          }
+          if(region_diff == 0){
+            MC_free_snapshot(sn);
+            xbt_dynar_reset(prop_ato);
+            xbt_free(prop_ato);
+            MC_UNSET_RAW_MEM;
+            return 1;
+          }else{
+            XBT_INFO("Different snapshot");
+          }
+        }else{
+          XBT_INFO("Different values of propositional symbols");
+        }

       }else{
       }else{

-  XBT_INFO("Different automaton state");
+        XBT_INFO("Different automaton state");

       }
 
       region_diff = 0;
       }
 
       region_diff = 0;


@@ -571,28 +571,28 @@ int visited(xbt_state_t st, int sc){
 
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
       if(pair_test->search_cycle == sc) {
 
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
       if(pair_test->search_cycle == sc) {

-  if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-    if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-      if(snapshot_compare(pair_test->system_state, sn) == 0){
+        if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+          if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+            if(snapshot_compare(pair_test->system_state, sn) == 0){

       
       

-        MC_free_snapshot(sn);
-        xbt_dynar_reset(prop_ato);
-        xbt_free(prop_ato);
-        MC_UNSET_RAW_MEM;
+              MC_free_snapshot(sn);
+              xbt_dynar_reset(prop_ato);
+              xbt_free(prop_ato);
+              MC_UNSET_RAW_MEM;

     
     

-        return 1;
+              return 1;

   
   

+            }else{
+              XBT_INFO("Different snapshot");
+            }
+          }else{
+            XBT_INFO("Different values of propositional symbols"); 
+          }
+        }else{
+          XBT_INFO("Different automaton state");
+        }

       }else{
       }else{

-        XBT_INFO("Different snapshot");
-      }
-    }else{
-      XBT_INFO("Different values of propositional symbols"); 
-    }
-  }else{
-    XBT_INFO("Different automaton state");
-  }
-      }else{
-  XBT_INFO("Different value of search_cycle");
+        XBT_INFO("Different value of search_cycle");

       }
     }
 
       }
     }
 


@@ -649,30 +649,30 @@ int visited_hash(xbt_state_t st, int sc){
     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
   
       if(pair_test->search_cycle == sc) {
     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
   
       if(pair_test->search_cycle == sc) {

-  if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-    if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-      for(j=0 ; j< sn->num_reg ; j++){
-        if(hash_regions[j] != pair_test->hash_regions[j]){
-    region_diff++;
+        if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+          if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+            for(j=0 ; j< sn->num_reg ; j++){
+              if(hash_regions[j] != pair_test->hash_regions[j]){
+                region_diff++;
+              }
+            }
+            if(region_diff == 0){
+              MC_free_snapshot(sn);
+              xbt_dynar_reset(prop_ato);
+              xbt_free(prop_ato);
+              MC_UNSET_RAW_MEM;
+              return 1;
+            }else{
+              //XBT_INFO("Different snapshot");
+            }
+          }else{
+            //XBT_INFO("Different values of propositional symbols"); 
+          }
+        }else{
+          //XBT_INFO("Different automaton state");

         }
         }

-      }
-      if(region_diff == 0){
-        MC_free_snapshot(sn);
-        xbt_dynar_reset(prop_ato);
-        xbt_free(prop_ato);
-        MC_UNSET_RAW_MEM;
-        return 1;

       }else{
       }else{

-        //XBT_INFO("Different snapshot");
-      }
-    }else{
-      //XBT_INFO("Different values of propositional symbols"); 
-    }
-  }else{
-    //XBT_INFO("Different automaton state");
-  }
-      }else{
-  //XBT_INFO("Different value of search_cycle");
+        //XBT_INFO("Different value of search_cycle");

       }
       
       region_diff = 0;
       }
       
       region_diff = 0;


@@ -791,8 +791,8 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
     int_f_void_t f;
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
     int_f_void_t f;
     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){

-  f = (int_f_void_t)p->function;
-  return (*f)();
+        f = (int_f_void_t)p->function;
+        return (*f)();

       }
     }
     return -1;
       }
     }
     return -1;


@@ -870,8 +870,8 @@ void MC_ddfs_init(void){
       MC_UNSET_RAW_MEM;
       
       if(cursor != 0){
       MC_UNSET_RAW_MEM;
       
       if(cursor != 0){

-  MC_restore_snapshot(initial_snapshot_liveness);
-  MC_UNSET_RAW_MEM;
+        MC_restore_snapshot(initial_snapshot_liveness);
+        MC_UNSET_RAW_MEM;

       }
 
       MC_ddfs(0);
       }
 
       MC_ddfs(0);


@@ -879,20 +879,20 @@ void MC_ddfs_init(void){
     }else{
       if(state->type == 2){
       
     }else{
       if(state->type == 2){
       

-  MC_SET_RAW_MEM;
-  mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
-  xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
-  MC_UNSET_RAW_MEM;
+        MC_SET_RAW_MEM;
+        mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+        xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
+        MC_UNSET_RAW_MEM;

 
 

-  set_pair_reached(state);
-  //set_pair_reached_hash(state);
+        set_pair_reached(state);
+        //set_pair_reached_hash(state);

 
 

-  if(cursor != 0){
-    MC_restore_snapshot(initial_snapshot_liveness);
-    MC_UNSET_RAW_MEM;
-  }
+        if(cursor != 0){
+          MC_restore_snapshot(initial_snapshot_liveness);
+          MC_UNSET_RAW_MEM;
+        }

   
   

-  MC_ddfs(1);
+        MC_ddfs(1);

   
       }
     }
   
       }
     }


@@ -948,171 +948,171 @@ void MC_ddfs(int search_cycle){
 
       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
    
 
       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
    

-  /* Debug information */
+        /* Debug information */

 
 

-  req_str = MC_request_to_string(req, value);
-  XBT_INFO("Execute: %s", req_str);
-  xbt_free(req_str);
+        req_str = MC_request_to_string(req, value);
+        XBT_INFO("Execute: %s", req_str);
+        xbt_free(req_str);

 
 

-  MC_state_set_executed_request(current_pair->graph_state, req, value);   
+        MC_state_set_executed_request(current_pair->graph_state, req, value);   

 
 

-  /* Answer the request */
-  SIMIX_simcall_pre(req, value);
+        /* Answer the request */
+        SIMIX_simcall_pre(req, value);

 
 

-  /* Wait for requests (schedules processes) */
-  MC_wait_for_requests();
+        /* Wait for requests (schedules processes) */
+        MC_wait_for_requests();

 
 
 
 

-  MC_SET_RAW_MEM;
+        MC_SET_RAW_MEM;

 
 

-  /* Create the new expanded graph_state */
-  next_graph_state = MC_state_pair_new();
+        /* Create the new expanded graph_state */
+        next_graph_state = MC_state_pair_new();

 
 

-  /* Get enabled process and insert it in the interleave set of the next graph_state */
-  xbt_swag_foreach(process, simix_global->process_list){
-    if(MC_process_is_enabled(process)){
-      MC_state_interleave_process(next_graph_state, process);
-    }
-  }
+        /* Get enabled process and insert it in the interleave set of the next graph_state */
+        xbt_swag_foreach(process, simix_global->process_list){
+          if(MC_process_is_enabled(process)){
+            MC_state_interleave_process(next_graph_state, process);
+          }
+        }

 
 

-  xbt_dynar_reset(successors);
+        xbt_dynar_reset(successors);

 
 

-  MC_UNSET_RAW_MEM;
+        MC_UNSET_RAW_MEM;

 
 
 
 

-  cursor= 0;
-  xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+        cursor= 0;
+        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){

 
 

-    res = MC_automaton_evaluate_label(transition_succ->label);
+          res = MC_automaton_evaluate_label(transition_succ->label);

 
 

-    if(res == 1){ // enabled transition in automaton
-      MC_SET_RAW_MEM;
-      next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
-      xbt_dynar_push(successors, &next_pair);
-      MC_UNSET_RAW_MEM;
-    }
+          if(res == 1){ // enabled transition in automaton
+            MC_SET_RAW_MEM;
+            next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+            xbt_dynar_push(successors, &next_pair);
+            MC_UNSET_RAW_MEM;
+          }

 
 

-  }
+        }

 
 

-  cursor = 0;
+        cursor = 0;

    
    

-  xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){

       
       

-    res = MC_automaton_evaluate_label(transition_succ->label);
+          res = MC_automaton_evaluate_label(transition_succ->label);

   
   

-    if(res == 2){ // true transition in automaton
-      MC_SET_RAW_MEM;
-      next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
-      xbt_dynar_push(successors, &next_pair);
-      MC_UNSET_RAW_MEM;
-    }
+          if(res == 2){ // true transition in automaton
+            MC_SET_RAW_MEM;
+            next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+            xbt_dynar_push(successors, &next_pair);
+            MC_UNSET_RAW_MEM;
+          }

 
 

-  }
+        }

 
 

-  cursor = 0; 
+        cursor = 0; 

   
   

-  xbt_dynar_foreach(successors, cursor, pair_succ){
+        xbt_dynar_foreach(successors, cursor, pair_succ){

 
 

-    if(search_cycle == 1){
+          if(search_cycle == 1){

 
 

-      if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+            if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 

           
           

-        if(reached(pair_succ->automaton_state)){
-    //if(reached_hash(pair_succ->automaton_state)){
+              if(reached(pair_succ->automaton_state)){
+                //if(reached_hash(pair_succ->automaton_state)){

         
         

-    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));
+                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));

 
 

-    XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-    XBT_INFO("|             ACCEPTANCE CYCLE            |");
-    XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-    XBT_INFO("Counter-example that violates formula :");
-    MC_show_stack_liveness(mc_stack_liveness);
-    MC_dump_stack_liveness(mc_stack_liveness);
-    MC_print_statistics_pairs(mc_stats_pair);
-    exit(0);
+                XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+                XBT_INFO("|             ACCEPTANCE CYCLE            |");
+                XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+                XBT_INFO("Counter-example that violates formula :");
+                MC_show_stack_liveness(mc_stack_liveness);
+                MC_dump_stack_liveness(mc_stack_liveness);
+                MC_print_statistics_pairs(mc_stats_pair);
+                exit(0);

 
 

-        }else{
+              }else{

 
 

-    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);
+                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);

         
         

-    set_pair_reached(pair_succ->automaton_state);
-    //set_pair_reached_hash(pair_succ->automaton_state);
+                set_pair_reached(pair_succ->automaton_state);
+                //set_pair_reached_hash(pair_succ->automaton_state);

 
 

-    XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-    //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+                XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));

 
 

-    MC_SET_RAW_MEM;
-    xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-    MC_UNSET_RAW_MEM;
+                MC_SET_RAW_MEM;
+                xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+                MC_UNSET_RAW_MEM;

     
     

-    MC_ddfs(search_cycle);
+                MC_ddfs(search_cycle);

 
 

-        }
+              }

 
 

-      }else{
+            }else{

 
 

-        if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-    //if(!visited(pair_succ->automaton_state, search_cycle)){
+              if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+                //if(!visited(pair_succ->automaton_state, search_cycle)){

     
     

-    MC_SET_RAW_MEM;
-    xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-    MC_UNSET_RAW_MEM;
+                MC_SET_RAW_MEM;
+                xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+                MC_UNSET_RAW_MEM;

     
     

-    MC_ddfs(search_cycle);
+                MC_ddfs(search_cycle);

     
     

-        }else{
+              }else{

 
 

-    XBT_INFO("Next pair already visited ! ");
+                XBT_INFO("Next pair already visited ! ");

 
 

-        }
+              }

         
         

-      }
+            }

 
 

-    }else{
+          }else{

     
     

-      if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+            if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){

 
 

-        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);
+              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);

       
       

-        set_pair_reached(pair_succ->automaton_state); 
-        //set_pair_reached_hash(pair_succ->automaton_state);
+              set_pair_reached(pair_succ->automaton_state); 
+              //set_pair_reached_hash(pair_succ->automaton_state);

 
 

-        search_cycle = 1;
+              search_cycle = 1;

 
 

-        XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-        //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));

 
 

-      }
+            }

 
 

-      if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-        //if(!visited(pair_succ->automaton_state, search_cycle)){
+            if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+              //if(!visited(pair_succ->automaton_state, search_cycle)){

         
         

-        MC_SET_RAW_MEM;
-        xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-        MC_UNSET_RAW_MEM;
+              MC_SET_RAW_MEM;
+              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+              MC_UNSET_RAW_MEM;

         
         

-        MC_ddfs(search_cycle);
+              MC_ddfs(search_cycle);

         
         

-      }else{
+            }else{

 
 

-        XBT_INFO("Next pair already visited ! ");
+              XBT_INFO("Next pair already visited ! ");

 
 

-      }
+            }

 
 

-    }
+          }

 
    
 
    

-    /* Restore system before checking others successors */
-    if(cursor != (xbt_dynar_length(successors) - 1))
-      MC_replay_liveness(mc_stack_liveness, 1);
+          /* Restore system before checking others successors */
+          if(cursor != (xbt_dynar_length(successors) - 1))
+            MC_replay_liveness(mc_stack_liveness, 1);

   
     
   
     

-  }
+        }

 
 

-  if(MC_state_interleave_size(current_pair->graph_state) > 0){
-    XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
-    MC_replay_liveness(mc_stack_liveness, 0);
-  }
+        if(MC_state_interleave_size(current_pair->graph_state) > 0){
+          XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
+          MC_replay_liveness(mc_stack_liveness, 0);
+        }

       }
 
  
       }
 
  


@@ -1131,14 +1131,14 @@ void MC_ddfs(int search_cycle){
       cursor= 0;
       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       cursor= 0;
       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 

-  res = MC_automaton_evaluate_label(transition_succ->label);
+        res = MC_automaton_evaluate_label(transition_succ->label);

 
 

-  if(res == 1){ // enabled transition in automaton
-    MC_SET_RAW_MEM;
-    next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
-    xbt_dynar_push(successors, &next_pair);
-    MC_UNSET_RAW_MEM;
-  }
+        if(res == 1){ // enabled transition in automaton
+          MC_SET_RAW_MEM;
+          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+          xbt_dynar_push(successors, &next_pair);
+          MC_UNSET_RAW_MEM;
+        }

 
       }
 
 
       }
 


@@ -1146,14 +1146,14 @@ void MC_ddfs(int search_cycle){
    
       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
       
    
       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
       

-  res = MC_automaton_evaluate_label(transition_succ->label);
+        res = MC_automaton_evaluate_label(transition_succ->label);

   
   

-  if(res == 2){ // true transition in automaton
-    MC_SET_RAW_MEM;
-    next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
-    xbt_dynar_push(successors, &next_pair);
-    MC_UNSET_RAW_MEM;
-  }
+        if(res == 2){ // true transition in automaton
+          MC_SET_RAW_MEM;
+          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+          xbt_dynar_push(successors, &next_pair);
+          MC_UNSET_RAW_MEM;
+        }

 
       }
 
 
       }
 


@@ -1161,95 +1161,95 @@ void MC_ddfs(int search_cycle){
      
       xbt_dynar_foreach(successors, cursor, pair_succ){
 
      
       xbt_dynar_foreach(successors, cursor, pair_succ){
 

-  if(search_cycle == 1){
+        if(search_cycle == 1){

 
 

-    if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+          if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 

 
 

-      if(reached(pair_succ->automaton_state)){
-        //if(reached_hash(pair_succ->automaton_state)){
+            if(reached(pair_succ->automaton_state)){
+              //if(reached_hash(pair_succ->automaton_state)){

 
 

-        XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
+              XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);

         
         

-        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-        XBT_INFO("|             ACCEPTANCE CYCLE            |");
-        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-        XBT_INFO("Counter-example that violates formula :");
-        MC_show_stack_liveness(mc_stack_liveness);
-        MC_dump_stack_liveness(mc_stack_liveness);
-        MC_print_statistics_pairs(mc_stats_pair);
-        exit(0);
-
-      }else{
-
-        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);
+              XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+              XBT_INFO("|             ACCEPTANCE CYCLE            |");
+              XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+              XBT_INFO("Counter-example that violates formula :");
+              MC_show_stack_liveness(mc_stack_liveness);
+              MC_dump_stack_liveness(mc_stack_liveness);
+              MC_print_statistics_pairs(mc_stats_pair);
+              exit(0);
+
+            }else{
+
+              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);

         
         

-        set_pair_reached(pair_succ->automaton_state);
-        //set_pair_reached_hash(pair_succ->automaton_state);
+              set_pair_reached(pair_succ->automaton_state);
+              //set_pair_reached_hash(pair_succ->automaton_state);

     
     

-        XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-        //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));

 
 

-        MC_SET_RAW_MEM;
-        xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-        MC_UNSET_RAW_MEM;
+              MC_SET_RAW_MEM;
+              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+              MC_UNSET_RAW_MEM;

         
         

-        MC_ddfs(search_cycle);
+              MC_ddfs(search_cycle);

 
 

-      }
+            }

 
 

-    }else{
+          }else{

 
 

-      if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-        //if(!visited(pair_succ->automaton_state, search_cycle)){
+            if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+              //if(!visited(pair_succ->automaton_state, search_cycle)){

 
 

-        MC_SET_RAW_MEM;
-        xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-        MC_UNSET_RAW_MEM;
+              MC_SET_RAW_MEM;
+              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+              MC_UNSET_RAW_MEM;

         
         

-        MC_ddfs(search_cycle);
+              MC_ddfs(search_cycle);

         
         

-      }else{
+            }else{

 
 

-        XBT_INFO("Next pair already visited ! ");
+              XBT_INFO("Next pair already visited ! ");

 
 

-      }
-    }
+            }
+          }

       
 
       
 

-  }else{
+        }else{

       
       

-    if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+          if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){

 
 

-      set_pair_reached(pair_succ->automaton_state);
-      //set_pair_reached_hash(pair_succ->automaton_state);
+            set_pair_reached(pair_succ->automaton_state);
+            //set_pair_reached_hash(pair_succ->automaton_state);

             
             

-      search_cycle = 1;
+            search_cycle = 1;

 
 

-      XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-      //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+            XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+            //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));

 
 

-    }
+          }

 
 

-    if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-      //if(!visited(pair_succ->automaton_state, search_cycle)){
+          if(!visited_hash(pair_succ->automaton_state, search_cycle)){
+            //if(!visited(pair_succ->automaton_state, search_cycle)){

 
 

-      MC_SET_RAW_MEM;
-      xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-      MC_UNSET_RAW_MEM;
+            MC_SET_RAW_MEM;
+            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+            MC_UNSET_RAW_MEM;

       
       

-      MC_ddfs(search_cycle);
+            MC_ddfs(search_cycle);

       
       

-    }else{
+          }else{

 
 

-      XBT_INFO("Next pair already visited ! ");
+            XBT_INFO("Next pair already visited ! ");

 
 

-    }
+          }

 
 

-  }
+        }

 
 

-  /* Restore system before checking others successors */
-  if(cursor != xbt_dynar_length(successors) - 1)
-    MC_replay_liveness(mc_stack_liveness, 1);
+        /* Restore system before checking others successors */
+        if(cursor != xbt_dynar_length(successors) - 1)
+          MC_replay_liveness(mc_stack_liveness, 1);

 
    
       }
 
    
       }

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 9a5f74a..3d89d84 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -27,7 +27,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
     return FALSE;
 
   if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
     return FALSE;
 
   if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)

-       &&  r2->call == SIMCALL_COMM_WAIT){
+        &&  r2->call == SIMCALL_COMM_WAIT){

 
     if(r2->comm_wait.comm->comm.rdv == NULL)
       return FALSE;
 
     if(r2->comm_wait.comm->comm.rdv == NULL)
       return FALSE;


@@ -45,7 +45,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
   }
 
   if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
   }
 
   if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)

-       &&  r1->call == SIMCALL_COMM_WAIT){
+        &&  r1->call == SIMCALL_COMM_WAIT){

 
     if(r1->comm_wait.comm->comm.rdv != NULL)
       return FALSE;
 
     if(r1->comm_wait.comm->comm.rdv != NULL)
       return FALSE;


@@ -66,22 +66,22 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
    * isend/irecv call is not stored in a buffer used in the
    * test call. */
   if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
    * isend/irecv call is not stored in a buffer used in the
    * test call. */
   if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)

-     &&  r2->call == SIMCALL_COMM_TEST)
+        &&  r2->call == SIMCALL_COMM_TEST)

     return FALSE;
 
   /* FIXME: the following rule assumes that the result of the
    * isend/irecv call is not stored in a buffer used in the
    * test call.*/
   if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
     return FALSE;
 
   /* FIXME: the following rule assumes that the result of the
    * isend/irecv call is not stored in a buffer used in the
    * test call.*/
   if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)

-     && r1->call == SIMCALL_COMM_TEST)
+        && r1->call == SIMCALL_COMM_TEST)

     return FALSE;
 
   if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND

-      && r1->comm_isend.rdv != r2->comm_isend.rdv)
+     && r1->comm_isend.rdv != r2->comm_isend.rdv)

     return FALSE;
 
   if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV

-      && r1->comm_irecv.rdv != r2->comm_irecv.rdv)
+     && r1->comm_irecv.rdv != r2->comm_irecv.rdv)

     return FALSE;
 
   if(r1->call == SIMCALL_COMM_WAIT && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_WAIT && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)


@@ -95,8 +95,8 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT

-      && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
-      && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
+     && r1->comm_wait.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
+     && r1->comm_wait.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)

     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT


@@ -110,46 +110,46 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_TEST &&
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_TEST &&

-      (r1->comm_test.comm == NULL
-       || r1->comm_test.comm->comm.src_buff == NULL
-       || r1->comm_test.comm->comm.dst_buff == NULL))
+     (r1->comm_test.comm == NULL
+      || r1->comm_test.comm->comm.src_buff == NULL
+      || r1->comm_test.comm->comm.dst_buff == NULL))

     return FALSE;
 
   if(r2->call == SIMCALL_COMM_TEST &&
     return FALSE;
 
   if(r2->call == SIMCALL_COMM_TEST &&

-      (r2->comm_test.comm == NULL
-       || r2->comm_test.comm->comm.src_buff == NULL
-       || r2->comm_test.comm->comm.dst_buff == NULL))
+     (r2->comm_test.comm == NULL
+      || r2->comm_test.comm->comm.src_buff == NULL
+      || r2->comm_test.comm->comm.dst_buff == NULL))

     return FALSE;
 
   if(r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT

-      && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
-      && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)
+     && r1->comm_test.comm->comm.src_buff == r2->comm_wait.comm->comm.src_buff
+     && r1->comm_test.comm->comm.dst_buff == r2->comm_wait.comm->comm.dst_buff)

     return FALSE;
 
   if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
     return FALSE;
 
   if(r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST

-      && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
-      && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)
+     && r1->comm_wait.comm->comm.src_buff == r2->comm_test.comm->comm.src_buff
+     && r1->comm_wait.comm->comm.dst_buff == r2->comm_test.comm->comm.dst_buff)

     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST

-        && r1->comm_wait.comm->comm.src_buff != NULL
-        && r1->comm_wait.comm->comm.dst_buff != NULL
-        && r2->comm_test.comm->comm.src_buff != NULL
-        && r2->comm_test.comm->comm.dst_buff != NULL
-        && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
-        && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
-        && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)
+      && r1->comm_wait.comm->comm.src_buff != NULL
+      && r1->comm_wait.comm->comm.dst_buff != NULL
+      && r2->comm_test.comm->comm.src_buff != NULL
+      && r2->comm_test.comm->comm.dst_buff != NULL
+      && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.src_buff
+      && r1->comm_wait.comm->comm.dst_buff != r2->comm_test.comm->comm.dst_buff
+      && r2->comm_test.comm->comm.dst_buff != r1->comm_wait.comm->comm.src_buff)

     return FALSE;
 
   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT

-          && r1->comm_test.comm->comm.src_buff != NULL
-          && r1->comm_test.comm->comm.dst_buff != NULL
-          && r2->comm_wait.comm->comm.src_buff != NULL
-          && r2->comm_wait.comm->comm.dst_buff != NULL
-          && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
-          && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
-          && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
-      return FALSE;
+      && r1->comm_test.comm->comm.src_buff != NULL
+      && r1->comm_test.comm->comm.dst_buff != NULL
+      && r2->comm_wait.comm->comm.src_buff != NULL
+      && r2->comm_wait.comm->comm.dst_buff != NULL
+      && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.src_buff
+      && r1->comm_test.comm->comm.dst_buff != r2->comm_wait.comm->comm.dst_buff
+      && r2->comm_wait.comm->comm.dst_buff != r1->comm_test.comm->comm.src_buff)
+    return FALSE;

 
 
   return TRUE;
 
 
   return TRUE;


@@ -179,69 +179,69 @@ char *MC_request_to_string(smx_simcall_t req, int value)
   size_t size = 0;
 
   switch(req->call){
   size_t size = 0;
 
   switch(req->call){

-    case SIMCALL_COMM_ISEND:
-      type = xbt_strdup("iSend");
-      p = pointer_to_string(req->comm_isend.src_buff);
-      bs = buff_size_to_string(req->comm_isend.src_buff_size);
-      args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs);
-      break;
-    case SIMCALL_COMM_IRECV:
-      size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
-      type = xbt_strdup("iRecv");
-      p = pointer_to_string(req->comm_irecv.dst_buff); 
-      bs = buff_size_to_string(size);
-      args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs);
-      break;
-    case SIMCALL_COMM_WAIT:
-      act = req->comm_wait.comm;
-      if(value == -1){
-        type = xbt_strdup("WaitTimeout");
-  p = pointer_to_string(act);
-  args = bprintf("comm=%p", p);
-      }else{
-        type = xbt_strdup("Wait");
-  p = pointer_to_string(act);
-  args  = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
-                        act->comm.src_proc ? act->comm.src_proc->pid : 0,
-                        act->comm.src_proc ? act->comm.src_proc->name : "",
-                        act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
-                        act->comm.dst_proc ? act->comm.dst_proc->name : "");
-      }
-      break;
-    case SIMCALL_COMM_TEST:
-      act = req->comm_test.comm;
-      if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){
-        type = xbt_strdup("Test FALSE");
-  p = pointer_to_string(act);
-        args = bprintf("comm=%s", p);
-      }else{
-        type = xbt_strdup("Test TRUE");
-  p = pointer_to_string(act);
-        args  = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
-                        act->comm.src_proc->pid, act->comm.src_proc->name,
-                        act->comm.dst_proc->pid, act->comm.dst_proc->name);
-      }
-      break;
-
-    case SIMCALL_COMM_WAITANY:
-      type = xbt_strdup("WaitAny");
-      p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t));
-      args = bprintf("comm=%s (%d of %lu)", p,
-                     value+1, xbt_dynar_length(req->comm_waitany.comms));
-      break;
-
-    case SIMCALL_COMM_TESTANY:
-      if(value == -1){
-        type = xbt_strdup("TestAny FALSE");
-        args = xbt_strdup("-");
-      }else{
-        type = xbt_strdup("TestAny");
-        args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
-      }
-      break;
-
-    default:
-      THROW_UNIMPLEMENTED;
+  case SIMCALL_COMM_ISEND:
+    type = xbt_strdup("iSend");
+    p = pointer_to_string(req->comm_isend.src_buff);
+    bs = buff_size_to_string(req->comm_isend.src_buff_size);
+    args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs);
+    break;
+  case SIMCALL_COMM_IRECV:
+    size = req->comm_irecv.dst_buff_size ? *req->comm_irecv.dst_buff_size : 0;
+    type = xbt_strdup("iRecv");
+    p = pointer_to_string(req->comm_irecv.dst_buff); 
+    bs = buff_size_to_string(size);
+    args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs);
+    break;
+  case SIMCALL_COMM_WAIT:
+    act = req->comm_wait.comm;
+    if(value == -1){
+      type = xbt_strdup("WaitTimeout");
+      p = pointer_to_string(act);
+      args = bprintf("comm=%p", p);
+    }else{
+      type = xbt_strdup("Wait");
+      p = pointer_to_string(act);
+      args  = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
+                      act->comm.src_proc ? act->comm.src_proc->pid : 0,
+                      act->comm.src_proc ? act->comm.src_proc->name : "",
+                      act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
+                      act->comm.dst_proc ? act->comm.dst_proc->name : "");
+    }
+    break;
+  case SIMCALL_COMM_TEST:
+    act = req->comm_test.comm;
+    if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL){
+      type = xbt_strdup("Test FALSE");
+      p = pointer_to_string(act);
+      args = bprintf("comm=%s", p);
+    }else{
+      type = xbt_strdup("Test TRUE");
+      p = pointer_to_string(act);
+      args  = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p,
+                      act->comm.src_proc->pid, act->comm.src_proc->name,
+                      act->comm.dst_proc->pid, act->comm.dst_proc->name);
+    }
+    break;
+
+  case SIMCALL_COMM_WAITANY:
+    type = xbt_strdup("WaitAny");
+    p = pointer_to_string(xbt_dynar_get_as(req->comm_waitany.comms, value, smx_action_t));
+    args = bprintf("comm=%s (%d of %lu)", p,
+                   value+1, xbt_dynar_length(req->comm_waitany.comms));
+    break;
+
+  case SIMCALL_COMM_TESTANY:
+    if(value == -1){
+      type = xbt_strdup("TestAny FALSE");
+      args = xbt_strdup("-");
+    }else{
+      type = xbt_strdup("TestAny");
+      args = bprintf("(%d of %lu)", value+1, xbt_dynar_length(req->comm_testany.comms));
+    }
+    break;
+
+  default:
+    THROW_UNIMPLEMENTED;

   }
 
   str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);
   }
 
   str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args);


@@ -268,11 +268,11 @@ unsigned int MC_request_testany_fail(smx_simcall_t req)
 int MC_request_is_visible(smx_simcall_t req)
 {
   return req->call == SIMCALL_COMM_ISEND
 int MC_request_is_visible(smx_simcall_t req)
 {
   return req->call == SIMCALL_COMM_ISEND

-     || req->call == SIMCALL_COMM_IRECV
-     || req->call == SIMCALL_COMM_WAIT
-     || req->call == SIMCALL_COMM_WAITANY
-     || req->call == SIMCALL_COMM_TEST
-     || req->call == SIMCALL_COMM_TESTANY;
+    || req->call == SIMCALL_COMM_IRECV
+    || req->call == SIMCALL_COMM_WAIT
+    || req->call == SIMCALL_COMM_WAITANY
+    || req->call == SIMCALL_COMM_TEST
+    || req->call == SIMCALL_COMM_TESTANY;

 }
 
 int MC_request_is_enabled(smx_simcall_t req)
 }
 
 int MC_request_is_enabled(smx_simcall_t req)


@@ -282,33 +282,33 @@ int MC_request_is_enabled(smx_simcall_t req)
 
   switch (req->call) {
 
 
   switch (req->call) {
 

-    case SIMCALL_COMM_WAIT:
-      /* FIXME: check also that src and dst processes are not suspended */
+  case SIMCALL_COMM_WAIT:
+    /* FIXME: check also that src and dst processes are not suspended */
+
+    /* If it has a timeout it will be always be enabled, because even if the
+     * communication is not ready, it can timeout and won't block.
+     * On the other hand if it hasn't a timeout, check if the comm is ready.*/
+    if(req->comm_wait.timeout >= 0){
+      return TRUE;
+    }else{
+      act = req->comm_wait.comm;
+      return (act->comm.src_proc && act->comm.dst_proc);
+    }
+    break;

 
 

-      /* If it has a timeout it will be always be enabled, because even if the
-       * communication is not ready, it can timeout and won't block.
-       * On the other hand if it hasn't a timeout, check if the comm is ready.*/
-      if(req->comm_wait.timeout >= 0){
+  case SIMCALL_COMM_WAITANY:
+    /* Check if it has at least one communication ready */
+    xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
+      if (act->comm.src_proc && act->comm.dst_proc){

         return TRUE;
         return TRUE;

-      }else{
-        act = req->comm_wait.comm;
-        return (act->comm.src_proc && act->comm.dst_proc);

       }
       }

-      break;
-
-    case SIMCALL_COMM_WAITANY:
-      /* Check if it has at least one communication ready */
-      xbt_dynar_foreach(req->comm_waitany.comms, index, act) {
-        if (act->comm.src_proc && act->comm.dst_proc){
-          return TRUE;
-        }
-      }
-      return FALSE;
-      break;
+    }
+    return FALSE;
+    break;

 
 

-    default:
-      /* The rest of the request are always enabled */
-      return TRUE;
+  default:
+    /* The rest of the request are always enabled */
+    return TRUE;

   }
 }
 
   }
 }
 


@@ -318,24 +318,24 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 
   switch (req->call) {
 
 
   switch (req->call) {
 

-    case SIMCALL_COMM_WAIT:
-      /* FIXME: check also that src and dst processes are not suspended */
-      act = req->comm_wait.comm;
-      return (act->comm.src_proc && act->comm.dst_proc);
-      break;
+  case SIMCALL_COMM_WAIT:
+    /* FIXME: check also that src and dst processes are not suspended */
+    act = req->comm_wait.comm;
+    return (act->comm.src_proc && act->comm.dst_proc);
+    break;

 
 

-    case SIMCALL_COMM_WAITANY:
-      act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
-      return (act->comm.src_proc && act->comm.dst_proc);
-      break;
+  case SIMCALL_COMM_WAITANY:
+    act = xbt_dynar_get_as(req->comm_waitany.comms, idx, smx_action_t);
+    return (act->comm.src_proc && act->comm.dst_proc);
+    break;

 
 

-    case SIMCALL_COMM_TESTANY:
-      act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
-      return (act->comm.src_proc && act->comm.dst_proc);
-      break;
+  case SIMCALL_COMM_TESTANY:
+    act = xbt_dynar_get_as(req->comm_testany.comms, idx, smx_action_t);
+    return (act->comm.src_proc && act->comm.dst_proc);
+    break;

 
 

-    default:
-      return TRUE;
+  default:
+    return TRUE;

   }
 }
 
   }
 }
 

diff --git a/src/xbt/mmalloc/mm_module.c b/src/xbt/mmalloc/mm_module.c
index b0b2d5d..1272d4d 100644 (file)
--- a/src/xbt/mmalloc/mm_module.c
+++ b/src/xbt/mmalloc/mm_module.c
@@ -3,22 +3,22 @@
 
    Contributed by Fred Fish at Cygnus Support.   fnf@cygnus.com
 
 
    Contributed by Fred Fish at Cygnus Support.   fnf@cygnus.com
 

-This file is part of the GNU C Library.
+   This file is part of the GNU C Library.

 
 

-The GNU C Library is free software; you can redistribute it and/or
-modify it under the terms of the GNU Library General Public License as
-published by the Free Software Foundation; either version 2 of the
-License, or (at your option) any later version.
+   The GNU C Library is free software; you can redistribute it and/or
+   modify it under the terms of the GNU Library General Public License as
+   published by the Free Software Foundation; either version 2 of the
+   License, or (at your option) any later version.

 
 

-The GNU C Library is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-Library General Public License for more details.
+   The GNU C Library is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+   Library General Public License for more details.

 
 

-You should have received a copy of the GNU Library General Public
-License along with the GNU C Library; see the file COPYING.LIB.  If
-not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
-Boston, MA 02111-1307, USA.  */
+   You should have received a copy of the GNU Library General Public
+   License along with the GNU C Library; see the file COPYING.LIB.  If
+   not, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
+   Boston, MA 02111-1307, USA.  */

 
 #include <sys/types.h>
 #include <fcntl.h>              /* After sys/types.h, at least for dpx/2.  */
 
 #include <sys/types.h>
 #include <fcntl.h>              /* After sys/types.h, at least for dpx/2.  */


@@ -84,56 +84,56 @@ xbt_mheap_t xbt_mheap_new(int fd, void *baseaddr)
 
     else if (sbuf.st_size > 0) {
       /* We were given an valid file descriptor on an open file, so try to remap
 
     else if (sbuf.st_size > 0) {
       /* We were given an valid file descriptor on an open file, so try to remap

-   it into the current process at the same address to which it was previously
-   mapped. It naturally have to pass some sanity checks for that.
+         it into the current process at the same address to which it was previously
+         mapped. It naturally have to pass some sanity checks for that.

 
 

-   Note that we have to update the file descriptor number in the malloc-
-   descriptor read from the file to match the current valid one, before
-   trying to map the file in, and again after a successful mapping and
-   after we've switched over to using the mapped in malloc descriptor
-   rather than the temporary one on the stack.
+         Note that we have to update the file descriptor number in the malloc-
+         descriptor read from the file to match the current valid one, before
+         trying to map the file in, and again after a successful mapping and
+         after we've switched over to using the mapped in malloc descriptor
+         rather than the temporary one on the stack.

 
 

-   Once we've switched over to using the mapped in malloc descriptor, we
-   have to update the pointer to the morecore function, since it almost
-   certainly will be at a different address if the process reusing the
-   mapped region is from a different executable.
+         Once we've switched over to using the mapped in malloc descriptor, we
+         have to update the pointer to the morecore function, since it almost
+         certainly will be at a different address if the process reusing the
+         mapped region is from a different executable.

 
 

-   Also note that if the heap being remapped previously used the mmcheckf()
-   routines, we need to update the hooks since their target functions
-   will have certainly moved if the executable has changed in any way.
-   We do this by calling mmcheckf() internally.
+         Also note that if the heap being remapped previously used the mmcheckf()
+         routines, we need to update the hooks since their target functions
+         will have certainly moved if the executable has changed in any way.
+         We do this by calling mmcheckf() internally.

 
 

-   Returns a pointer to the malloc descriptor if successful, or NULL if
-   unsuccessful for some reason. */
+         Returns a pointer to the malloc descriptor if successful, or NULL if
+         unsuccessful for some reason. */

 
       struct mdesc newmd;
       struct mdesc *mdptr = NULL, *mdptemp = NULL;
 
       if (lseek(fd, 0L, SEEK_SET) != 0)
 
       struct mdesc newmd;
       struct mdesc *mdptr = NULL, *mdptemp = NULL;
 
       if (lseek(fd, 0L, SEEK_SET) != 0)

-  return NULL;
+        return NULL;

       if (read(fd, (char *) &newmd, sizeof(newmd)) != sizeof(newmd))
       if (read(fd, (char *) &newmd, sizeof(newmd)) != sizeof(newmd))

-  return NULL;
+        return NULL;

       if (newmd.headersize != sizeof(newmd))
       if (newmd.headersize != sizeof(newmd))

-  return NULL;
+        return NULL;

       if (strcmp(newmd.magic, MMALLOC_MAGIC) != 0)
       if (strcmp(newmd.magic, MMALLOC_MAGIC) != 0)

-  return NULL;
+        return NULL;

       if (newmd.version > MMALLOC_VERSION)
       if (newmd.version > MMALLOC_VERSION)

-  return NULL;
+        return NULL;

 
       newmd.fd = fd;
       if (__mmalloc_remap_core(&newmd) == newmd.base) {
 
       newmd.fd = fd;
       if (__mmalloc_remap_core(&newmd) == newmd.base) {

-  mdptr = (struct mdesc *) newmd.base;
-  mdptr->fd = fd;
-  if(!mdptr->refcount){
-    sem_init(&mdptr->sem, 0, 1);
-    mdptr->refcount++;
-  }
+        mdptr = (struct mdesc *) newmd.base;
+        mdptr->fd = fd;
+        if(!mdptr->refcount){
+          sem_init(&mdptr->sem, 0, 1);
+          mdptr->refcount++;
+        }

       }
 
       /* Add the new heap to the linked list of heaps attached by mmalloc */
       mdptemp = __mmalloc_default_mdp;
       while(mdptemp->next_mdesc)
       }
 
       /* Add the new heap to the linked list of heaps attached by mmalloc */
       mdptemp = __mmalloc_default_mdp;
       while(mdptemp->next_mdesc)

-  mdptemp = mdptemp->next_mdesc;
+        mdptemp = mdptemp->next_mdesc;

 
       LOCK(mdptemp);
       mdptemp->next_mdesc = mdptr;
 
       LOCK(mdptemp);
       mdptemp->next_mdesc = mdptr;


@@ -193,7 +193,7 @@ xbt_mheap_t xbt_mheap_new(int fd, void *baseaddr)
       mdp = mdp->next_mdesc;
 
     LOCK(mdp);
       mdp = mdp->next_mdesc;
 
     LOCK(mdp);

-      mdp->next_mdesc = (struct mdesc *)mbase;
+    mdp->next_mdesc = (struct mdesc *)mbase;

     UNLOCK(mdp);
   }
 
     UNLOCK(mdp);
   }
 


@@ -218,18 +218,18 @@ void xbt_mheap_destroy_no_free(xbt_mheap_t md)
 }
 
 /** Terminate access to a mmalloc managed region by unmapping all memory pages
 }
 
 /** Terminate access to a mmalloc managed region by unmapping all memory pages

-   associated with the region, and closing the file descriptor if it is one
-   that we opened.
+    associated with the region, and closing the file descriptor if it is one
+    that we opened.

 
 

-   Returns NULL on success.
+    Returns NULL on success.

 
 

-   Returns the malloc descriptor on failure, which can subsequently be used
-   for further action, such as obtaining more information about the nature of
-   the failure.
+    Returns the malloc descriptor on failure, which can subsequently be used
+    for further action, such as obtaining more information about the nature of
+    the failure.

 
 

-   Note that the malloc descriptor that we are using is currently located in
-   region we are about to unmap, so we first make a local copy of it on the
-   stack and use the copy. */
+    Note that the malloc descriptor that we are using is currently located in
+    region we are about to unmap, so we first make a local copy of it on the
+    stack and use the copy. */

 
 void *xbt_mheap_destroy(xbt_mheap_t mdp)
 {
 
 void *xbt_mheap_destroy(xbt_mheap_t mdp)
 {


@@ -324,7 +324,7 @@ void *mmalloc_preinit(void)
     __mmalloc_default_mdp = xbt_mheap_new(-1, addr);
     /* Fixme? only the default mdp in protected against forks */
     res = xbt_os_thread_atfork(mmalloc_fork_prepare,
     __mmalloc_default_mdp = xbt_mheap_new(-1, addr);
     /* Fixme? only the default mdp in protected against forks */
     res = xbt_os_thread_atfork(mmalloc_fork_prepare,

-             mmalloc_fork_parent, mmalloc_fork_child);
+                               mmalloc_fork_parent, mmalloc_fork_child);

     if (res != 0)
       THROWF(system_error,0,"xbt_os_thread_atfork() failed: return value %d",res);
   }
     if (res != 0)
       THROWF(system_error,0,"xbt_os_thread_atfork() failed: return value %d",res);
   }

diff --git a/src/xbt/mmalloc/mmorecore.c b/src/xbt/mmalloc/mmorecore.c
index 339b72c..d374c7e 100644 (file)
--- a/src/xbt/mmalloc/mmorecore.c
+++ b/src/xbt/mmalloc/mmorecore.c
@@ -30,23 +30,23 @@
 static size_t pagesize;
 
 #define PAGE_ALIGN(addr) (void*) (((long)(addr) + pagesize - 1) & \
 static size_t pagesize;
 
 #define PAGE_ALIGN(addr) (void*) (((long)(addr) + pagesize - 1) & \

-            ~(pagesize - 1))
+                                  ~(pagesize - 1))

 
 /* Return MAP_PRIVATE if MDP represents /dev/zero.  Otherwise, return
    MAP_SHARED.  */
 #define MAP_PRIVATE_OR_SHARED(MDP) (( MDP -> flags & MMALLOC_ANONYMOUS) \
 
 /* Return MAP_PRIVATE if MDP represents /dev/zero.  Otherwise, return
    MAP_SHARED.  */
 #define MAP_PRIVATE_OR_SHARED(MDP) (( MDP -> flags & MMALLOC_ANONYMOUS) \

-                                    ? MAP_PRIVATE \
+                                    ? MAP_PRIVATE                       \

                                     : MAP_SHARED)
 
 /* Return MAP_ANONYMOUS if MDP uses anonymous mapping. Otherwise, return 0 */
 #define MAP_IS_ANONYMOUS(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \
                                     : MAP_SHARED)
 
 /* Return MAP_ANONYMOUS if MDP uses anonymous mapping. Otherwise, return 0 */
 #define MAP_IS_ANONYMOUS(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \

-                              ? MAP_ANONYMOUS \
-                              : 0)
+                               ? MAP_ANONYMOUS                      \
+                               : 0)

 
 /* Return -1 if MDP uses anonymous mapping. Otherwise, return MDP->FD */
 #define MAP_ANON_OR_FD(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \
 
 /* Return -1 if MDP uses anonymous mapping. Otherwise, return MDP->FD */
 #define MAP_ANON_OR_FD(MDP) (((MDP) -> flags & MMALLOC_ANONYMOUS) \

-                              ? -1 \
-                              : (MDP) -> fd)
+                             ? -1                                 \
+                             : (MDP) -> fd)

 
 /*  Get core for the memory region specified by MDP, using SIZE as the
     amount to either add to or subtract from the existing region.  Works
 
 /*  Get core for the memory region specified by MDP, using SIZE as the
     amount to either add to or subtract from the existing region.  Works

diff --git a/src/xbt/mmalloc/mmprivate.h b/src/xbt/mmalloc/mmprivate.h
index b68eb49..ccc667d 100644 (file)
--- a/src/xbt/mmalloc/mmprivate.h
+++ b/src/xbt/mmalloc/mmprivate.h
@@ -134,8 +134,8 @@ struct mstats
  */
 typedef struct {
   int type; /*  0: busy large block
  */
 typedef struct {
   int type; /*  0: busy large block

-    >0: busy fragmented (fragments of size 2^type bytes)
-    <0: free block */
+                >0: busy fragmented (fragments of size 2^type bytes)
+                <0: free block */

   union {
     /* Heap information for a busy block.  */
     struct {
   union {
     /* Heap information for a busy block.  */
     struct {

diff --git a/src/xbt/mmalloc/mrealloc.c b/src/xbt/mmalloc/mrealloc.c
index 7b803fe..23d0a1c 100644 (file)
--- a/src/xbt/mmalloc/mrealloc.c
+++ b/src/xbt/mmalloc/mrealloc.c
@@ -1,6 +1,6 @@
 /* Change the size of a block allocated by `mmalloc'.
    Copyright 1990, 1991 Free Software Foundation
 /* Change the size of a block allocated by `mmalloc'.
    Copyright 1990, 1991 Free Software Foundation

-      Written May 1989 by Mike Haertel. */
+   Written May 1989 by Mike Haertel. */

 
 /* Copyright (c) 2010. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* Copyright (c) 2010. The SimGrid Team.
  * All rights reserved.                                                     */


@@ -38,7 +38,7 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
 
   if ((char *) ptr < (char *) mdp->heapbase || BLOCK(ptr) > mdp->heapsize) {
     printf
 
   if ((char *) ptr < (char *) mdp->heapbase || BLOCK(ptr) > mdp->heapsize) {
     printf

-        ("FIXME. Ouch, this pointer is not mine, refusing to proceed (another solution would be to malloc it instead of reallocing it, see source code)\n");
+      ("FIXME. Ouch, this pointer is not mine, refusing to proceed (another solution would be to malloc it instead of reallocing it, see source code)\n");

     result = mmalloc(mdp, size);
     abort();
     return result;
     result = mmalloc(mdp, size);
     abort();
     return result;


@@ -83,10 +83,10 @@ void *mrealloc(xbt_mheap_t mdp, void *ptr, size_t size)
       /* The new size is smaller; return excess memory to the free list. */
       //printf("(%s) return excess memory...",xbt_thread_self_name());
       for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++)
       /* The new size is smaller; return excess memory to the free list. */
       //printf("(%s) return excess memory...",xbt_thread_self_name());
       for (it= block+blocks; it< mdp->heapinfo[block].busy_block.size ; it++)

-  mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here
+        mdp->heapinfo[it].type = 0; // FIXME that should be useless, type should already be 0 here

 
       mdp->heapinfo[block + blocks].busy_block.size
 
       mdp->heapinfo[block + blocks].busy_block.size

-          = mdp->heapinfo[block].busy_block.size - blocks;
+        = mdp->heapinfo[block].busy_block.size - blocks;

       mfree(mdp, ADDRESS(block + blocks));
 
       mdp->heapinfo[block].busy_block.size = blocks;
       mfree(mdp, ADDRESS(block + blocks));
 
       mdp->heapinfo[block].busy_block.size = blocks;