détection de cycle d'acceptation ok mais boucle infinie en cas d'absence de cycle

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 48b6872..203b7aa 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -18,6 +18,8 @@ mc_stats_t mc_stats = NULL;
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
+xbt_fifo_t mc_snapshot_stack = NULL;
+
 /**
  *  \brief Initialize the model-checker data structures
  */
@@ -51,6 +53,29 @@ void MC_init(void)
   MC_UNSET_RAW_MEM;
 }
 
+void MC_init_with_automaton(xbt_automaton_t a){
+  
+  mc_time = xbt_new0(double, simix_process_maxpid);
+
+  /* Initialize the data structures that must be persistent across every
+     iteration of the model-checker (in RAW memory) */
+  MC_SET_RAW_MEM;
+
+  /* Initialize statistics */
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  mc_stats->state_size = 1;
+
+  XBT_DEBUG("Creating snapshot_stack");
+
+ /* Create exploration stack */
+  mc_snapshot_stack = xbt_fifo_new();
+
+  MC_UNSET_RAW_MEM;
+
+  MC_dfs_init(a);
+}
+
+
 void MC_modelcheck(void)
 {
   MC_init();
@@ -58,6 +83,11 @@ void MC_modelcheck(void)
   MC_exit();
 }
 
+void MC_modelcheck_with_automaton(xbt_automaton_t a){
+  MC_init_with_automaton(a);
+  MC_exit();
+}
+
 void MC_exit(void)
 {
   MC_print_statistics(mc_stats);
@@ -76,15 +106,18 @@ int MC_random(int min, int max)
  */
 void MC_wait_for_requests(void)
 {
-  smx_req_t req = NULL;
-
-  do {
-    SIMIX_context_runall(simix_global->process_to_run);
-    while((req = SIMIX_request_pop())){
-      if(!MC_request_is_visible(req))
-        SIMIX_request_pre(req, 0);
+  smx_process_t process;
+  smx_req_t req;
+  unsigned int iter;
+
+  while (xbt_dynar_length(simix_global->process_to_run)) {
+    SIMIX_process_runall();
+    xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
+      req = &process->request;
+      if (req->call != REQ_NO_REQ && !MC_request_is_visible(req))
+          SIMIX_request_pre(req, 0);
     }
-  } while (xbt_dynar_length(simix_global->process_to_run));
+  }
 }
 
 int MC_deadlock_check()