[mc] Do not use reduction_mode outside of the safety algorithm

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index b37bf5f..d6a24e1 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -201,7 +201,8 @@ static int modelcheck_safety(void)
               "use --cfg=model-check/reduction:none");
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
-            if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
+            if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none
+                && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
                 XBT_DEBUG("Dependent Transitions:");
                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index d16cd27..7e7d2b1 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -462,7 +462,6 @@ static int MC_modelcheck_comm_determinism_main(void)
 int MC_modelcheck_comm_determinism(void)
 {
   XBT_INFO("Check communication determinism");
-  simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
   mc_model_checker->wait_for_requests();
 
   if (mc_mode == MC_MODE_CLIENT)

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index c9202f5..edf700d 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -373,8 +373,6 @@ static int MC_modelcheck_liveness_main(void)
 
 int modelcheck_liveness(void)
 {
-  if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
-    simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
   MC_automaton_load(_sg_mc_property_file);
   mc_model_checker->wait_for_requests();

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index 91f02cc..1404c21 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -136,9 +136,6 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
 // Those are MC_state_get_internal_request(state)
 bool request_depend(smx_simcall_t r1, smx_simcall_t r2)
 {
-  if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::none)
-    return true;
-
   if (r1->issuer == r2->issuer)
     return false;