X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/199b029b33b5b9fbe1eacb50828914f3b38bde2f..f53ee0c4bdeaffa3c7a781f45f640e5f32cbb480:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 97e3e2a235..e924d16857 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -11,6 +11,7 @@ mc_snapshot_t initial_snapshot = NULL;
 xbt_fifo_t mc_stack = NULL;
 xbt_setset_t mc_setset = NULL;
 mc_stats_t mc_stats = NULL;
+mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 
 /**
@@ -54,7 +55,8 @@ void MC_init(int method)
   MC_UNSET_RAW_MEM;
 }
 
-void MC_modelcheck(int method){
+void MC_modelcheck(int method)
+{
 
   MC_init(method);
 
@@ -68,8 +70,42 @@ void MC_modelcheck(int method){
     default:
       break;
   }
+
+  MC_exit(method);
 }
 
+void MC_exit(int method)
+{
+  mc_state_t state;
+  
+  switch(method){
+    case 0:
+      //MC_dfs_exit();
+      break;
+    case 1:
+      //MC_dpor_exit();
+      break;
+    default:
+      break;
+  }
+   
+  /* Destroy MC data structures (in RAW memory) */
+  MC_SET_RAW_MEM;
+  xbt_free(mc_stats);
+
+  while( (state = (mc_state_t)xbt_fifo_pop(mc_stack)) != NULL )
+    MC_state_delete(state);
+  
+  xbt_fifo_free(mc_stack);
+  xbt_setset_destroy(mc_setset);
+  MC_UNSET_RAW_MEM;
+}
+
+int MC_random(int min, int max)
+{
+  MC_trans_intercept_random(min, max);
+  return mc_current_state->executed_transition->random.value;
+}
 
 /**
  * \brief Re-executes from the initial state all the transitions indicated by
@@ -79,7 +115,6 @@ void MC_modelcheck(int method){
 void MC_replay(xbt_fifo_t stack)
 {
   xbt_fifo_item_t item;
-  mc_state_t state;
   mc_transition_t trans;
 
   DEBUG0("**** Begin Replay ****");
@@ -96,8 +131,8 @@ void MC_replay(xbt_fifo_t stack)
       item != xbt_fifo_get_first_item(stack);
       item = xbt_fifo_get_prev_item(item)){
 
-    state = (mc_state_t) xbt_fifo_get_item_content(item);
-    trans = state->executed_transition;
+    mc_current_state = (mc_state_t) xbt_fifo_get_item_content(item);
+    trans = mc_current_state->executed_transition;
 
     /* Update statistics */
     mc_stats->visited_states++;
@@ -124,16 +159,12 @@ void MC_replay(xbt_fifo_t stack)
 void MC_dump_stack(xbt_fifo_t stack)
 {
   mc_state_t state;
-  mc_transition_t trans;
 
+  MC_show_stack(stack);
+  
   MC_SET_RAW_MEM;
-  while( (state = (mc_state_t)xbt_fifo_pop(stack)) != NULL ){
-    trans = state->executed_transition;
-    if(trans)
-      INFO1("%s", trans->name);
-    
+  while( (state = (mc_state_t)xbt_fifo_pop(stack)) != NULL )
     MC_state_delete(state);
-  }
   MC_UNSET_RAW_MEM;
 }
 
@@ -143,9 +174,8 @@ void MC_show_stack(xbt_fifo_t stack)
   mc_transition_t trans;
   xbt_fifo_item_t item;
 
-  INFO0("===========================");
   for(item=xbt_fifo_get_last_item(stack);
-     (item?(state=(mc_state_t)(xbt_fifo_get_item_content(item))):(NULL));             \
+     (item?(state=(mc_state_t)(xbt_fifo_get_item_content(item))):(NULL));
       item=xbt_fifo_get_prev_item(item)){
     trans = state->executed_transition;
     if(trans){      
@@ -154,7 +184,6 @@ void MC_show_stack(xbt_fifo_t stack)
   }
 }
 
-
 /**
  * \brief Schedules all the process that are ready to run
  *        As a side effect it performs some clean-up required by SIMIX 
@@ -182,6 +211,7 @@ mc_state_t MC_state_new(void)
   mc_state_t state = NULL; 
   
   state = xbt_new0(s_mc_state_t, 1);
+  state->created_transitions = xbt_setset_new_set(mc_setset);
   state->transitions = xbt_setset_new_set(mc_setset);
   state->enabled_transitions = xbt_setset_new_set(mc_setset);
   state->interleave = xbt_setset_new_set(mc_setset);
@@ -198,8 +228,15 @@ mc_state_t MC_state_new(void)
  */
 void MC_state_delete(mc_state_t state)
 {
-  /*if(state->executed_transition)
-    MC_transition_delete(state->executed_transition);*/
+  xbt_setset_cursor_t cursor;
+  mc_transition_t trans;  
+  
+  xbt_setset_foreach(state->created_transitions, cursor, trans){
+    xbt_setset_elm_remove(mc_setset, trans);
+    MC_transition_delete(trans);
+  }
+
+  xbt_setset_destroy_set(state->created_transitions);
   xbt_setset_destroy_set(state->transitions);
   xbt_setset_destroy_set(state->enabled_transitions);
   xbt_setset_destroy_set(state->interleave);
@@ -234,12 +271,7 @@ void MC_execute_surf_actions(void)
         DEBUG5("Resource [%s] (%d): Executing RUNNING action \"%s\" (%p) MaxDuration %lf", 
           model->name, xbt_swag_size(model->states.running_action_set),
           smx_action->name, smx_action, action->max_duration);
-
-        /* Copy the transfered data of the completed network actions */              
-        /* FIXME: be carefull it might not be an action of the network model */
-        if(smx_action && smx_action->data != NULL)
-          SIMIX_network_copy_data((smx_comm_t)smx_action->data);
-
+        
         if(smx_action)
           SIMIX_action_signal_all(smx_action);
       }