From 7d9763f5619c35b79077e30f5d32de44699824a6 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 5 Apr 2016 10:48:08 +0200 Subject: [PATCH] [mc] Move visitedState as a field of SafetyChecker --- src/mc/SafetyChecker.cpp | 21 ++++++++++----------- src/mc/SafetyChecker.hpp | 1 + 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 02d1304483..68d89d75f3 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -97,7 +97,6 @@ int SafetyChecker::run() int value; smx_simcall_t req = nullptr; - std::unique_ptr visited_state = nullptr; while (!stack_.empty()) { @@ -116,8 +115,8 @@ int SafetyChecker::run() /* If there are processes to interleave and the maximum depth has not been reached then perform one step of the exploration algorithm */ if (stack_.size() <= (std::size_t) _sg_mc_max_depth - && (req = MC_state_get_request(state, &value)) - && visited_state == nullptr) { + && (req = MC_state_get_request(state, &value)) != nullptr + && visitedState_ == nullptr) { char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); XBT_DEBUG("Execute: %s", req_str); @@ -146,7 +145,7 @@ int SafetyChecker::run() } if (_sg_mc_visited == 0 - || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) { + || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) @@ -160,7 +159,7 @@ int SafetyChecker::run() std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); } else if (dot_output != nullptr) - std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); + std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str); stack_.push_back(std::move(next_state)); @@ -173,13 +172,13 @@ int SafetyChecker::run() } else { if (stack_.size() > (std::size_t) _sg_mc_max_depth - || visited_state != nullptr) { - - if (visited_state == nullptr) + || visitedState_ != nullptr) { + if (visitedState_ == nullptr) XBT_WARN("/!\\ Max depth reached ! /!\\ "); else - XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); - + XBT_DEBUG("State already visited (equal to state %d)," + " exploration stopped on this path.", + visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num); } else XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1); @@ -188,7 +187,7 @@ int SafetyChecker::run() XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size()); stack_.pop_back(); - visited_state = nullptr; + visitedState_ = nullptr; /* Check for deadlocks */ if (mc_model_checker->checkDeadlock()) { diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp index c1896eec2e..39b083454a 100644 --- a/src/mc/SafetyChecker.hpp +++ b/src/mc/SafetyChecker.hpp @@ -35,6 +35,7 @@ private: /** Stack representing the position in the exploration graph */ std::list> stack_; simgrid::mc::VisitedStates visitedStates_; + std::unique_ptr visitedState_; }; } -- 2.20.1