From ae62510f83c4cd6e7967aa00897bf66671a5923a Mon Sep 17 00:00:00 2001 From: mlaurent Date: Wed, 15 Feb 2023 16:21:20 +0100 Subject: [PATCH] updated doc --- src/mc/api/State.cpp | 2 +- src/mc/api/State.hpp | 7 +++++-- src/mc/explo/DFSExplorer.cpp | 8 ++++---- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index dae2c6f936..1e676d4c7d 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -62,7 +62,7 @@ std::size_t State::count_todo() const return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); } - void State::mark_all_todo() +void State::mark_all_todo() { for (auto & [aid, actor] : actors_to_run_) { diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index c10ca6200f..71670d3449 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -29,6 +29,9 @@ class XBT_PRIVATE State : public xbt::Extendable { /** Snapshot of system state (if needed) */ std::shared_ptr system_state_; + /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep + * set. With this information, it is check whether it should be removed from it or not when exploring a new + * transition */ std::map sleep_set_; public: @@ -44,7 +47,7 @@ public: std::size_t count_todo() const; void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); } void mark_done(aid_t actor) { actors_to_run_.at(actor).mark_done();} - void mark_all_todo(); + void mark_all_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); } @@ -57,7 +60,7 @@ public: void set_system_state(std::shared_ptr state) { system_state_ = std::move(state); } std::map const& get_sleep_set() const { return sleep_set_; } - void set_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); } + void add_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); } /* Returns the total amount of states created so far (for statistics) */ static long get_expanded_states() { return expended_states_; } diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 15d30b99f7..e8bb0b0979 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -146,7 +146,7 @@ void DFSExplorer::run() XBT_VERB("Sleep set actually containing:"); for (auto & [aid, transition] : state->get_sleep_set()) { - XBT_VERB("###<%ld,%s>", aid, transition.to_string().c_str()); + XBT_VERB(" <%ld,%s>", aid, transition.to_string().c_str()); } @@ -228,9 +228,9 @@ void DFSExplorer::backtrack() stack_.pop_back(); - XBT_DEBUG("Maarking Transition >>%s<< of process %ld done and adding it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_); + XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_); state->mark_done(state->get_transition()->aid_); - state->set_sleep_set(state->get_transition()); + state->add_sleep_set(state->get_transition()); if (reduction_mode_ == ReductionMode::dpor) { aid_t issuer_id = state->get_transition()->aid_; @@ -251,7 +251,7 @@ void DFSExplorer::backtrack() else XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id); } else { - XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing, to stay sound, we are marking every enabled transition as todo", issuer_id); + XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled transition as todo", issuer_id); prev_state->mark_all_todo(); } break; -- 2.20.1