model-checker : fix DPOR with visited states reduction

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index ab6b9bc..328a69d 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -32,6 +32,8 @@ int _sg_mc_max_depth=1000;
 int _sg_mc_visited=0;
 char *_sg_mc_dot_output_file = NULL;
 
+int user_max_depth_reached = 0;
+
 extern int _sg_init_status;
 void _mc_cfg_cb_reduce(const char *name, int pos) {
   if (_sg_init_status && !_sg_do_model_check) {
@@ -1969,16 +1971,16 @@ void MC_exit(void)
   //xbt_abort();
 }
 
-int SIMIX_pre_mc_random(smx_simcall_t simcall){
+int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
 
   return simcall->mc_value;
 }
 
 
-int MC_random(void)
+int MC_random(int min, int max)
 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/
-  return simcall_mc_random();
+  return simcall_mc_random(min, max);
 }
 
 /**
@@ -2389,8 +2391,8 @@ void MC_assert(int prop)
   }
 }
 
-void MC_max_depth(int max_depth){
-  user_max_depth_reached = max_depth;
+void MC_cut(void){
+  user_max_depth_reached = 1;
 }
 
 void MC_process_clock_add(smx_process_t process, double amount)