From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 4 May 2011 14:18:02 +0000 (+0200)
Subject: model-check : dump stack for acceptance cycle
X-Git-Tag: exp_20120216~133^2~94
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b9890631bde077fb24ee6c401bba8cded1559ae5

model-check : dump stack for acceptance cycle
---

diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c
index 514417ad4d..01d4313e7b 100644
--- a/src/mc/mc_dfs.c
+++ b/src/mc/mc_dfs.c
@@ -386,17 +386,11 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 	  MC_dfs(a, search_cycle, 0);
 
 	  if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){
-
-	    /* mc_pairs_t first_item = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
-	    /* if((first_item->graph_state != pair_succ->graph_state) || (first_item->automaton_state != pair_succ->automaton_state) ){ */
-	    /*   MC_SET_RAW_MEM; */
-	    /*   xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
-	    /*   MC_UNSET_RAW_MEM; */
-	    /* } */
-
+	    
 	    set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); 
 	    XBT_DEBUG("Acceptance state : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
 	    MC_dfs(a, 1, 0);
+
 	  }
 	}else{
 	  //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
@@ -483,7 +477,19 @@ void MC_show_snapshot_stack(xbt_fifo_t stack){
 }
 
 void MC_dump_snapshot_stack(xbt_fifo_t stack){
+  mc_pairs_t pair;
+
+  MC_SET_RAW_MEM;
+  while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
+    MC_pair_delete(pair);
+  MC_UNSET_RAW_MEM;
+}
 
+void MC_pair_delete(mc_pairs_t pair){
+  xbt_free(pair->graph_state->proc_status);
+  xbt_free(pair->graph_state);
+  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
+  xbt_free(pair);
 }
 
 
diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index fa88d39797..8588cb8ad3 100644
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -1,3 +1,5 @@
+
+
 #include "../simix/private.h"
 #include "xbt/fifo.h"
 #include "private.h"
diff --git a/src/mc/private.h b/src/mc/private.h
index 0c151dd4c6..688298ece4 100644
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -201,5 +201,6 @@ int reached(mc_state_t gs, xbt_state_t as);
 void set_pair_reached(mc_state_t gs, xbt_state_t as);
 void MC_show_snapshot_stack(xbt_fifo_t stack);
 void MC_dump_snapshot_stack(xbt_fifo_t stack);
+void MC_pair_delete(mc_pairs_t pair);
 
 #endif