From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 2 Nov 2011 13:35:31 +0000 (+0100)
Subject: model-checker : change variable successors (local->global) in dfs algorithm
X-Git-Tag: exp_20120216~133^2~54
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/646a169d229d00d57d0dfcd7ea030e186871ac7c

model-checker : change variable successors (local->global) in dfs algorithm
---

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 513f1732b4..c431568e16 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -7,6 +7,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
 xbt_dynar_t initial_pairs = NULL;
 xbt_dynar_t reached_pairs;
 mc_snapshot_t snapshot = NULL;
+xbt_dynar_t successors = NULL;
 extern mc_snapshot_t initial_snapshot;
 
 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
@@ -226,9 +227,10 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){
   }
 
   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
+  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  snapshot = xbt_new0(s_mc_snapshot_t, 1);
 
   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-  snapshot = xbt_new0(s_mc_snapshot_t, 1);
   MC_take_snapshot(initial_snapshot);
 
   MC_UNSET_RAW_MEM; 
@@ -317,12 +319,6 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
   mc_pair_stateless_t next_pair = NULL;
   mc_pair_stateless_t pair_succ;
   //mc_snapshot_t next_snapshot = NULL;
-  
-  xbt_dynar_t successors = NULL;
-  
-  MC_SET_RAW_MEM;
-  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
-  MC_UNSET_RAW_MEM;
 
   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){