From bbc184078a28d2563c177604eb04a2afe923e2fd Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 30 Jul 2022 16:16:17 +0200 Subject: [PATCH] MC: make it clear that we only have the info about the ready-to-run actors in a given mc::State This is very similar to the exploration algorithm in Simix, but that's still counter-intuitive when you try to understand the code. Let's hope that writting it this way will help me not falling into that trap anymore :) --- src/mc/api/State.cpp | 10 +++++----- src/mc/api/State.hpp | 14 +++++++------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 262e0108d6..79213e7cb3 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -23,7 +23,7 @@ State::State(Session& session) : num_(++expended_states_) auto remote_actor = actors[i].copy.get_buffer(); aid_t aid = remote_actor->get_pid(); - actor_states_.insert( + actors_to_run_.insert( std::make_pair(aid, ActorState(aid, session.actor_is_enabled(aid), remote_actor->simcall_.mc_max_consider_))); } @@ -37,7 +37,7 @@ State::State(Session& session) : num_(++expended_states_) std::size_t State::count_todo() const { - return boost::range::count_if(this->actor_states_, [](auto& pair) { return pair.second.is_todo(); }); + return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); } Transition* State::get_transition() const @@ -47,8 +47,8 @@ Transition* State::get_transition() const aid_t State::next_transition() const { - XBT_DEBUG("Search for an actor to run. %zu actors to consider", actor_states_.size()); - for (auto const& [aid, actor] : actor_states_) { + XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size()); + for (auto const& [aid, actor] : actors_to_run_) { /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */ if (not actor.is_todo() || not actor.is_enabled()) continue; @@ -60,7 +60,7 @@ aid_t State::next_transition() const void State::execute_next(aid_t next) { /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */ - const unsigned times_considered = actor_states_.at(next).do_consider(); + const unsigned times_considered = actors_to_run_.at(next).do_consider(); XBT_DEBUG("Let's run actor %ld (times_considered = %u)", next, times_considered); diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 93cb03638c..49317bc119 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -22,8 +22,8 @@ class XBT_PRIVATE State : public xbt::Extendable { /** Sequential state ID (used for debugging) */ long num_ = 0; - /** State's exploration status by process */ - std::map actor_states_; + /** State's exploration status by actor. Not all the actors are there, only the ones that are ready-to-run in this state */ + std::map actors_to_run_; /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; @@ -39,14 +39,14 @@ public: long get_num() const { return num_; } std::size_t count_todo() const; - void mark_todo(aid_t actor) { actor_states_.at(actor).mark_todo(); } - bool is_done(aid_t actor) const { return actor_states_.at(actor).is_done(); } + void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); } + bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); } Transition* get_transition() const; void set_transition(Transition* t) { transition_.reset(t); } - std::map const& get_actors_list() { return actor_states_; } + std::map const& get_actors_list() { return actors_to_run_; } - int get_actor_count() { return actor_states_.size(); } - bool is_actor_enabled(int actor) { return actor_states_.at(actor).is_enabled(); } + int get_actor_count() { return actors_to_run_.size(); } + bool is_actor_enabled(int actor) { return actors_to_run_.at(actor).is_enabled(); } Snapshot* get_system_state() const { return system_state_.get(); } void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } -- 2.20.1