From 41887885e1953cb056594145190e30088f9b6d03 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Mon, 7 Feb 2022 10:18:34 +0100 Subject: [PATCH] Make State::transition_ private --- src/mc/Transition.cpp | 10 ++++--- src/mc/Transition.hpp | 4 +-- .../CommunicationDeterminismChecker.cpp | 16 +++++----- src/mc/checker/LivenessChecker.cpp | 16 +++++----- src/mc/checker/SafetyChecker.cpp | 29 ++++++++++--------- src/mc/mc_state.cpp | 4 +-- src/mc/mc_state.hpp | 6 ++-- 7 files changed, 44 insertions(+), 41 deletions(-) diff --git a/src/mc/Transition.cpp b/src/mc/Transition.cpp index 5c6a80eb65..43bb496b82 100644 --- a/src/mc/Transition.cpp +++ b/src/mc/Transition.cpp @@ -16,7 +16,7 @@ namespace simgrid { namespace mc { unsigned long Transition::executed_transitions_ = 0; -std::string Transition::to_string() +std::string Transition::to_string() const { xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); @@ -28,18 +28,20 @@ RemotePtr Transition::execute(simgrid:: kernel::actor::ActorImpl* actor = actors[next].copy.get_buffer(); aid_t aid = actor->get_pid(); + int times_considered; simgrid::mc::ActorState* actor_state = &state->actor_states_[aid]; /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */ if (actor->simcall_.observer_ != nullptr) { - state->transition_.times_considered_ = actor_state->get_times_considered_and_inc(); + times_considered = actor_state->get_times_considered_and_inc(); if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered()) actor_state->set_done(); } else { - state->transition_.times_considered_ = 0; + times_considered = 0; actor_state->set_done(); } + times_considered_ = times_considered; aid_ = aid; state->executed_req_ = actor->simcall_; @@ -48,7 +50,7 @@ RemotePtr Transition::execute(simgrid:: return replay(); } -RemotePtr Transition::replay() +RemotePtr Transition::replay() const { executed_transitions_++; diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp index a51e996db2..90e6976ec6 100644 --- a/src/mc/Transition.hpp +++ b/src/mc/Transition.hpp @@ -40,12 +40,12 @@ public: */ int times_considered_ = 0; - std::string to_string(); + std::string to_string() const; /* Explore a new path */ RemotePtr execute(simgrid::mc::State* state, int next); /* Moves the application toward a path that was already explored, but don't change the current transition */ - RemotePtr replay(); + RemotePtr replay() const; /* Returns the total amount of transitions executed so far (for statistics) */ static unsigned long get_executed_transitions() { return executed_transitions_; } diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 3ac7e22014..47f30895eb 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -262,7 +262,7 @@ RecordTrace CommunicationDeterminismChecker::get_record_trace() // override { RecordTrace res; for (auto const& state : stack_) - res.push_back(state->get_transition()); + res.push_back(*state->get_transition()); return res; } @@ -270,7 +270,7 @@ std::vector CommunicationDeterminismChecker::get_textual_trace() // { std::vector trace; for (auto const& state : stack_) - trace.push_back(state->transition_.to_string()); + trace.push_back(state->get_transition()->to_string()); return trace; } @@ -357,7 +357,7 @@ void CommunicationDeterminismChecker::restoreState() if (state == stack_.back()) break; - int req_num = state->transition_.times_considered_; + int req_num = state->get_transition()->times_considered_; const s_smx_simcall* saved_req = &state->executed_req_; xbt_assert(saved_req); @@ -369,7 +369,7 @@ void CommunicationDeterminismChecker::restoreState() /* TODO : handle test and testany simcalls */ CallType call = MC_get_call_type(req); - state->transition_.replay(); + state->get_transition()->replay(); handle_comm_pattern(call, req, req_num, 1); /* Update statistics */ @@ -423,13 +423,13 @@ void CommunicationDeterminismChecker::real_run() next_transition = cur_state->next_transition(); if (next_transition >= 0 && visited_state == nullptr) { - cur_state->transition_.execute(cur_state, next_transition); + cur_state->get_transition()->execute(cur_state, next_transition); - aid_t aid = cur_state->transition_.aid_; - int req_num = cur_state->transition_.times_considered_; + aid_t aid = cur_state->get_transition()->aid_; + int req_num = cur_state->get_transition()->times_considered_; smx_simcall_t req = &cur_state->executed_req_; - XBT_DEBUG("Execute: %s", cur_state->transition_.to_string().c_str()); + XBT_DEBUG("Execute: %s", cur_state->get_transition()->to_string().c_str()); std::string req_str; if (dot_output != nullptr) diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index e5f59bbd41..df92c7f10d 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -122,8 +122,8 @@ void LivenessChecker::replay() std::shared_ptr state = pair->graph_state; if (pair->exploration_started) { - state->transition_.replay(); - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->transition_.to_string().c_str(), state.get()); + state->get_transition()->replay(); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get()); } /* Update statistics */ @@ -187,7 +187,7 @@ RecordTrace LivenessChecker::get_record_trace() // override { RecordTrace res; for (std::shared_ptr const& pair : exploration_stack_) - res.push_back(pair->graph_state->get_transition()); + res.push_back(*pair->graph_state->get_transition()); return res; } @@ -217,7 +217,7 @@ std::vector LivenessChecker::get_textual_trace() // override for (std::shared_ptr const& pair : exploration_stack_) { smx_simcall_t req = &pair->graph_state->executed_req_; if (req->call_ != simix::Simcall::NONE) - trace.push_back(pair->graph_state->transition_.to_string()); + trace.push_back(pair->graph_state->get_transition()->to_string()); } return trace; } @@ -338,11 +338,11 @@ void LivenessChecker::run() int next = current_pair->graph_state->next_transition(); - current_pair->graph_state->transition_.execute(current_pair->graph_state.get(), next); + current_pair->graph_state->get_transition()->execute(current_pair->graph_state.get(), next); - aid_t aid = current_pair->graph_state->transition_.aid_; - int req_num = current_pair->graph_state->transition_.times_considered_; - XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str()); + aid_t aid = current_pair->graph_state->get_transition()->aid_; + int req_num = current_pair->graph_state->get_transition()->times_considered_; + XBT_DEBUG("Execute: %s", current_pair->graph_state->get_transition()->to_string().c_str()); if (dot_output != nullptr) { if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 9f3a8f74da..7cc9546992 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -52,7 +52,7 @@ RecordTrace SafetyChecker::get_record_trace() // override { RecordTrace res; for (auto const& state : stack_) - res.push_back(state->get_transition()); + res.push_back(*state->get_transition()); return res; } @@ -60,7 +60,7 @@ std::vector SafetyChecker::get_textual_trace() // override { std::vector trace; for (auto const& state : stack_) - trace.push_back(state->transition_.to_string()); + trace.push_back(state->get_transition()->to_string()); return trace; } @@ -124,15 +124,16 @@ void SafetyChecker::run() } /* Actually answer the request: let execute the selected request (MCed does one step) */ - auto remote_observer = state->transition_.execute(state, next); + auto remote_observer = state->get_transition()->execute(state, next); // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. - XBT_DEBUG("Execute: %s", state->transition_.to_string().c_str()); + XBT_DEBUG("Execute: %s", state->get_transition()->to_string().c_str()); std::string req_str; if (dot_output != nullptr) - req_str = api::get().request_get_dot_output(state->transition_.aid_, state->transition_.times_considered_); + req_str = + api::get().request_get_dot_output(state->get_transition()->aid_, state->get_transition()->times_considered_); /* Create the new expanded state (copy the state of MCed into our MCer data) */ ++expanded_states_count_; @@ -189,18 +190,18 @@ void SafetyChecker::backtrack() std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); if (reductionMode_ == ReductionMode::dpor) { - aid_t issuer_id = state->transition_.aid_; + aid_t issuer_id = state->get_transition()->aid_; for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { State* prev_state = i->get(); - if (state->transition_.aid_ == prev_state->transition_.aid_) { - XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->transition_.to_string().c_str(), - prev_state->transition_.to_string().c_str(), issuer_id); + if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) { + XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(), + prev_state->get_transition()->to_string().c_str(), issuer_id); break; } else if (api::get().requests_are_dependent(prev_state->remote_observer_, state->remote_observer_)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); - XBT_DEBUG(" %s (state=%d)", prev_state->transition_.to_string().c_str(), prev_state->num_); - XBT_DEBUG(" %s (state=%d)", state->transition_.to_string().c_str(), state->num_); + XBT_DEBUG(" %s (state=%d)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); + XBT_DEBUG(" %s (state=%d)", state->get_transition()->to_string().c_str(), state->num_); } if (not prev_state->actor_states_[issuer_id].is_done()) @@ -211,8 +212,8 @@ void SafetyChecker::backtrack() } else { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("INDEPENDENT Transitions:"); - XBT_DEBUG(" %s (state=%d)", prev_state->transition_.to_string().c_str(), prev_state->num_); - XBT_DEBUG(" %s (state=%d)", state->transition_.to_string().c_str(), state->num_); + XBT_DEBUG(" %s (state=%d)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); + XBT_DEBUG(" %s (state=%d)", state->get_transition()->to_string().c_str(), state->num_); } } } @@ -246,7 +247,7 @@ void SafetyChecker::restore_state() for (std::unique_ptr const& state : stack_) { if (state == stack_.back()) break; - state->transition_.replay(); + state->get_transition()->replay(); /* Update statistics */ api::get().mc_inc_visited_states(); } diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 154511c32a..6bc1a7d571 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -38,9 +38,9 @@ std::size_t State::count_todo() const return boost::range::count_if(this->actor_states_, [](simgrid::mc::ActorState const& a) { return a.is_todo(); }); } -Transition State::get_transition() const +Transition* State::get_transition() const { - return this->transition_; + return const_cast(&this->transition_); } int State::next_transition() const diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index ae21f24078..dbabb8a1ca 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -15,6 +15,8 @@ namespace mc { /* A node in the exploration graph (kind-of) */ class XBT_PRIVATE State { + Transition transition_; + public: /** Sequential state number (used for debugging) */ int num_ = 0; @@ -22,8 +24,6 @@ public: /** State's exploration status by process */ std::vector actor_states_; - Transition transition_; - /** The simcall which was executed, going out of that state */ s_smx_simcall executed_req_; @@ -44,7 +44,7 @@ public: std::size_t count_todo() const; void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); } - Transition get_transition() const; + Transition* get_transition() const; private: void copy_incomplete_comm_pattern(); -- 2.20.1