model-checker : fix dichotomic search and insertion for visited states

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index c10eef5..017b0d0 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -9,7 +9,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
                                 "Logging specific to MC DPOR exploration");
 
 xbt_dynar_t visited_states;
                                 "Logging specific to MC DPOR exploration");
 
 xbt_dynar_t visited_states;

-int nb_visited_states = 0;

 
 static int is_visited_state(void);
 static void visited_state_free(mc_safety_visited_state_t state);
 
 static int is_visited_state(void);
 static void visited_state_free(mc_safety_visited_state_t state);


@@ -28,8 +27,6 @@ static void visited_state_free_voidp(void *s){
 
 static int is_visited_state(){
 
 
 static int is_visited_state(){
 

-  nb_visited_states++;
-

   if(_sg_mc_visited == 0)
     return 0;
 
   if(_sg_mc_visited == 0)
     return 0;
 


@@ -40,7 +37,7 @@ static int is_visited_state(){
   mc_safety_visited_state_t new_state = NULL;
   new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
   new_state->system_state = MC_take_snapshot();
   mc_safety_visited_state_t new_state = NULL;
   new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
   new_state->system_state = MC_take_snapshot();

-  new_state->num = nb_visited_states;
+  new_state->num = mc_stats->expanded_states;

 
   MC_UNSET_RAW_MEM;
   
 
   MC_UNSET_RAW_MEM;
   


@@ -127,11 +124,19 @@ static int is_visited_state(){
         }   
       }
     }
         }   
       }
     }

- 
-    if(xbt_dynar_length(visited_states) == _sg_mc_visited){
-      int min = nb_visited_states;
+
+    state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
+    chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
+
+    if(chunks_used_test < current_chunks_used)
+      xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
+    else
+      xbt_dynar_insert_at(visited_states, cursor, &new_state);
+
+    if(xbt_dynar_length(visited_states) > _sg_mc_visited){
+      int min = mc_stats->expanded_states;

       unsigned int cursor2 = 0;
       unsigned int cursor2 = 0;

-      unsigned int index;
+      unsigned int index = 0;

       xbt_dynar_foreach(visited_states, cursor2, state_test){
         if(state_test->num < min){
           index = cursor2;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
         if(state_test->num < min){
           index = cursor2;


@@ -140,14 +145,6 @@ static int is_visited_state(){
       }
       xbt_dynar_remove_at(visited_states, index, NULL);
     }
       }
       xbt_dynar_remove_at(visited_states, index, NULL);
     }

-
-    if(cursor > 0)
-      cursor--;
-
-    if(chunks_used_test < current_chunks_used)
-      xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
-    else
-      xbt_dynar_insert_at(visited_states, cursor, &new_state);

     
     MC_UNSET_RAW_MEM;
 
     
     MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 5ebe09e..cdc4cd1 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -180,8 +180,7 @@ void MC_init(){
   get_binary_plt_section();
 
   MC_ignore_data_bss(&end_raw_heap, sizeof(end_raw_heap));
   get_binary_plt_section();
 
   MC_ignore_data_bss(&end_raw_heap, sizeof(end_raw_heap));

-  MC_ignore_data_bss(&nb_visited_states, sizeof(nb_visited_states));
-
+ 

   /* Get global variables */
   MC_get_global_variables(xbt_binary_name);
   MC_get_global_variables(libsimgrid_path);
   /* Get global variables */
   MC_get_global_variables(xbt_binary_name);
   MC_get_global_variables(libsimgrid_path);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index ac17191..84af06d 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -230,8 +230,6 @@ typedef struct s_mc_safety_visited_state{
   int num;
 }s_mc_safety_visited_state_t, *mc_safety_visited_state_t;
 
   int num;
 }s_mc_safety_visited_state_t, *mc_safety_visited_state_t;
 

-extern int nb_visited_states;
-

 
 /********************************** Double-DFS for liveness property**************************************/
 
 
 /********************************** Double-DFS for liveness property**************************************/