From 873fe7743b2a9f2eddc53ed3383bdd74bb3fe226 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 21 Mar 2016 16:45:52 +0100 Subject: [PATCH 1/1] [mc] Do not use reduction_mode outside of the safety algorithm --- src/mc/SafetyChecker.cpp | 3 ++- src/mc/mc_comm_determinism.cpp | 1 - src/mc/mc_liveness.cpp | 2 -- src/mc/mc_request.cpp | 3 --- 4 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index b37bf5f341..d6a24e1f47 100644 --- 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 d16cd27dcf..7e7d2b1814 100644 --- 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 c9202f5c9a..edf700d15d 100644 --- 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 91f02ccbf2..1404c21e6f 100644 --- 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; -- 2.20.1