From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Thu, 3 Jan 2013 11:13:12 +0000 (+0100)
Subject: model-checker : update list of visited states during the exploration with the newest... 
X-Git-Tag: v3_9_rc1~86^2~43
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e621aad76114ee574a0e26966992408db9c5ec27

model-checker : update list of visited states during the exploration with the newest states
---

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 9576aada9d..c10eef5d98 100644
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -81,6 +81,8 @@ static int is_visited_state(){
       if(chunks_used_test == current_chunks_used){
         same_chunks_not_found = 0;
         if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
+          xbt_dynar_remove_at(visited_states, cursor, NULL);
+          xbt_dynar_insert_at(visited_states, cursor, &new_state);
           if(raw_mem_set)
             MC_SET_RAW_MEM;
           else
@@ -95,6 +97,8 @@ static int is_visited_state(){
             if(chunks_used_test != current_chunks_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
+              xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
+              xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
               if(raw_mem_set)
                 MC_SET_RAW_MEM;
               else
@@ -110,6 +114,8 @@ static int is_visited_state(){
             if(chunks_used_test != current_chunks_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
+              xbt_dynar_remove_at(visited_states, next_cursor, NULL);
+              xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
               if(raw_mem_set)
                 MC_SET_RAW_MEM;
               else