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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index acbaabfe63..9cd6c7f6db 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -4,7 +4,7 @@
 #include "private.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
-				"Logging specific to MC (global)");
+                                "Logging specific to MC (global)");
 
 /* MC global data structures */
 mc_snapshot_t initial_snapshot = NULL;
@@ -18,39 +18,39 @@ char mc_replay_mode = FALSE;
  *  \brief Initialize the model-checker data structures
  */
 void MC_init(int method)
-{   
+{
   /* Check if MC is already initialized */
-  if(initial_snapshot)
+  if (initial_snapshot)
     return;
-   
+
   /* 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;
-  
+
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
   /* Create the container for the sets */
   mc_setset = xbt_setset_new(20);
-  
-  switch(method){
-    case 0:
-      MC_dfs_init();
-      break;
-    case 1:
-      MC_dpor_init();
-      break;
-    default:
-      break;
+
+  switch (method) {
+  case 0:
+    MC_dfs_init();
+    break;
+  case 1:
+    MC_dpor_init();
+    break;
+  default:
+    break;
   }
-  
+
   /* Save the initial state */
   MC_SET_RAW_MEM;
-  initial_snapshot = xbt_new(s_mc_snapshot_t,1);	
+  initial_snapshot = xbt_new(s_mc_snapshot_t, 1);
   MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 }
@@ -60,15 +60,15 @@ void MC_modelcheck(int method)
 
   MC_init(method);
 
-  switch(method){
-    case 0:
-      MC_dfs();
-      break;
-    case 1:
-      MC_dpor();
-      break;
-    default:
-      break;
+  switch (method) {
+  case 0:
+    MC_dfs();
+    break;
+  case 1:
+    MC_dpor();
+    break;
+  default:
+    break;
   }
 
   MC_exit(method);
@@ -77,25 +77,25 @@ void MC_modelcheck(int 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;
+
+  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 )
+  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;
@@ -103,13 +103,8 @@ void MC_exit(int method)
 
 int MC_random(int min, int max)
 {
-  MC_random_create(min,max);
-  SIMIX_process_yield();
-
-  if(!mc_replay_mode)
-    return mc_current_state->executed_transition->current_value;
-  else
-    return mc_current_state->executed_transition->current_value - 1;
+  MC_trans_intercept_random(min, max);
+  return mc_current_state->executed_transition->random.value;
 }
 
 /**
@@ -128,13 +123,13 @@ void MC_replay(xbt_fifo_t stack)
   MC_restore_snapshot(initial_snapshot);
 
   mc_replay_mode = TRUE;
-  
+
   MC_UNSET_RAW_MEM;
 
   /* Traverse the stack from the initial state and re-execute the transitions */
-  for(item = xbt_fifo_get_last_item(stack);
-      item != xbt_fifo_get_first_item(stack);
-      item = xbt_fifo_get_prev_item(item)){
+  for (item = xbt_fifo_get_last_item(stack);
+       item != xbt_fifo_get_first_item(stack);
+       item = xbt_fifo_get_prev_item(item)) {
 
     mc_current_state = (mc_state_t) xbt_fifo_get_item_content(item);
     trans = mc_current_state->executed_transition;
@@ -166,9 +161,9 @@ void MC_dump_stack(xbt_fifo_t stack)
   mc_state_t state;
 
   MC_show_stack(stack);
-  
+
   MC_SET_RAW_MEM;
-  while( (state = (mc_state_t)xbt_fifo_pop(stack)) != NULL )
+  while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
     MC_state_delete(state);
   MC_UNSET_RAW_MEM;
 }
@@ -179,12 +174,12 @@ void MC_show_stack(xbt_fifo_t stack)
   mc_transition_t trans;
   xbt_fifo_item_t item;
 
-  for(item=xbt_fifo_get_last_item(stack);
-     (item?(state=(mc_state_t)(xbt_fifo_get_item_content(item))):(NULL));
-      item=xbt_fifo_get_prev_item(item)){
+  for (item = xbt_fifo_get_last_item(stack);
+       (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){      
-      INFO1("%s", trans->name);  
+    if (trans) {
+      INFO1("%s", trans->name);
     }
   }
 }
@@ -213,8 +208,8 @@ void MC_schedule_enabled_processes(void)
  */
 mc_state_t MC_state_new(void)
 {
-  mc_state_t state = NULL; 
-  
+  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);
@@ -224,9 +219,10 @@ mc_state_t MC_state_new(void)
   state->executed_transition = NULL;
 
   mc_stats->expanded_states++;
-  
+
   return state;
 }
+
 /**
  * \brief Deletes a state data structure
  * \param trans The state to be deleted
@@ -234,9 +230,10 @@ mc_state_t MC_state_new(void)
 void MC_state_delete(mc_state_t state)
 {
   xbt_setset_cursor_t cursor;
-  mc_transition_t trans;  
-  
-  xbt_setset_foreach(state->created_transitions, cursor, trans){
+  mc_transition_t trans;
+
+  xbt_setset_foreach(state->created_transitions, cursor, trans) {
+    xbt_setset_elm_remove(mc_setset, trans);
     MC_transition_delete(trans);
   }
 
@@ -266,32 +263,33 @@ void MC_execute_surf_actions(void)
   smx_action_t smx_action = NULL;
 
   /* Execute all the actions in every model */
-  xbt_dynar_foreach(model_list, iter, model){
-    while ((action = xbt_swag_extract(model->states.running_action_set))){
+  xbt_dynar_foreach(model_list, iter, model) {
+    while ((action = xbt_swag_extract(model->states.running_action_set))) {
       /* FIXME: timeouts are not calculated correctly */
-      if(NOW >= action->max_duration){ 
+      if (NOW >= action->max_duration) {
         surf_action_state_set(action, SURF_ACTION_DONE);
         smx_action = action->data;
-        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);
-        
-        if(smx_action)
+        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);
+
+        if (smx_action)
           SIMIX_action_signal_all(smx_action);
       }
     }
     /*FIXME: check if this is always empty or not */
     while ((action = xbt_swag_extract(model->states.failed_action_set))) {
       smx_action = action->data;
-      DEBUG4("Resource [%s] (%d): Executing FAILED action \"%s\" (%p)", 
-        model->name, xbt_swag_size(model->states.running_action_set),
-        smx_action->name, smx_action);
+      DEBUG4("Resource [%s] (%d): Executing FAILED action \"%s\" (%p)",
+             model->name, xbt_swag_size(model->states.running_action_set),
+             smx_action->name, smx_action);
       if (smx_action)
-       SIMIX_action_signal_all(smx_action);
+        SIMIX_action_signal_all(smx_action);
     }
   }
   /* That's it, now go one step deeper into the model-checking process! */
-  NOW += 0.5;  /* FIXME: Check time increases*/
+  NOW += 0.5;                   /* FIXME: Check time increases */
 }
 
 /****************************** Statistics ************************************/
@@ -302,15 +300,15 @@ void MC_print_statistics(mc_stats_t stats)
   INFO1("Visited states = %lu", stats->visited_states);
   INFO1("Executed transitions = %lu", stats->executed_transitions);
   INFO1("Expanded / Visited = %lf",
-    (double)stats->visited_states / stats->expanded_states);
+        (double) stats->visited_states / stats->expanded_states);
   /*INFO1("Exploration coverage = %lf", 
-    (double)stats->expanded_states / stats->state_size);*/
+     (double)stats->expanded_states / stats->state_size); */
 }
 
 /************************* Assertion Checking *********************************/
 void MC_assert(int prop)
 {
-  if(!prop){
+  if (!prop) {
     INFO0("**************************");
     INFO0("*** PROPERTY NOT VALID ***");
     INFO0("**************************");
@@ -320,4 +318,3 @@ void MC_assert(int prop)
     xbt_abort();
   }
 }
-