From: mlaurent Date: Sat, 18 Mar 2023 13:46:53 +0000 (+0100) Subject: Replace todo direct access with consider methods; guided or not X-Git-Tag: v3.34~240^2~19 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/639c6962daa378323864a53174e0e7fe2fcaef1e?ds=sidebyside Replace todo direct access with consider methods; guided or not --- diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp index 008a8443a4..868d8fbe6d 100644 --- a/src/mc/api/State.cpp +++ b/src/mc/api/State.cpp @@ -64,15 +64,6 @@ std::size_t State::count_todo() const return boost::range::count_if(this->guide->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); }); } -void State::mark_all_enabled_todo() -{ - for (auto const& [aid, _] : this->get_actors_list()) { - if (this->is_actor_enabled(aid) and not is_actor_done(aid)) { - this->mark_todo(aid); - } - } -} - Transition* State::get_transition() const { return transition_; diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index 5415ac809a..8626d9978c 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -54,7 +54,8 @@ public: explicit State(RemoteApp& remote_app); explicit State(RemoteApp& remote_app, const State* parent_state); /* Returns a positive number if there is another transition to pick, or -1 if not */ - aid_t next_transition() const; + aid_t next_transition() const; // this function should disapear as it is redundant with the next one + /* Same as next_transition, but choice is now guided, and a double corresponding to the internal cost of the transition is returned */ std::pair next_transition_guided() const; @@ -65,8 +66,11 @@ public: long get_num() const { return num_; } std::size_t count_todo() const; - void mark_todo(aid_t actor) { guide->actors_to_run_.at(actor).mark_todo(); } - void mark_all_enabled_todo(); + + void consider_one(aid_t aid) { guide->consider_one(aid); } + void consider_best() { guide->consider_best(); } + void consider_all() { guide->consider_all(); } + bool is_actor_done(aid_t actor) const { return guide->actors_to_run_.at(actor).is_done(); } Transition* get_transition() const; void set_transition(Transition* t) { transition_ = t; } diff --git a/src/mc/api/guide/BasicGuide.hpp b/src/mc/api/guide/BasicGuide.hpp index 4fcd9f61ae..daa573329c 100644 --- a/src/mc/api/guide/BasicGuide.hpp +++ b/src/mc/api/guide/BasicGuide.hpp @@ -26,6 +26,18 @@ public: return std::make_pair(-1, 0.0); } void execute_next(aid_t aid, RemoteApp& app) override { return; } + + void consider_best() override + { + for (auto& [_, actor] : actors_to_run_) { + if (actor.is_todo()) + return; + if (actor.is_enabled() and not actor.is_done()) { + actor.mark_todo(); + return; + } + } + } }; } // namespace simgrid::mc diff --git a/src/mc/api/guide/GuidedState.hpp b/src/mc/api/guide/GuidedState.hpp index 6eb3a96afa..aab6531239 100644 --- a/src/mc/api/guide/GuidedState.hpp +++ b/src/mc/api/guide/GuidedState.hpp @@ -3,6 +3,8 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include "xbt/asserts.h" + #ifndef SIMGRID_MC_GUIDEDSTATE_HPP #define SIMGRID_MC_GUIDEDSTATE_HPP @@ -17,6 +19,24 @@ protected: public: virtual std::pair next_transition() const = 0; virtual void execute_next(aid_t aid, RemoteApp& app) = 0; + virtual void consider_best() = 0; + + // Mark the first enabled and not yet done transition as todo + // If there's already a transition marked as todo, does nothing + void consider_one(aid_t aid) + { + xbt_assert(actors_to_run_.at(aid).is_enabled() and not actors_to_run_.at(aid).is_done(), + "Tried to mark as TODO actor %ld but it is either not enabled or already done", aid); + actors_to_run_.at(aid).mark_todo(); + } + // Matk as todo all actors enabled that are not done yet + void consider_all() + { + for (auto& [_, actor] : actors_to_run_) + if (actor.is_enabled() and not actor.is_done()) + actor.mark_todo(); + } + friend class State; }; diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index ad1bd08250..64972274f5 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -177,13 +177,10 @@ void DFSExplorer::run() /* If this is a new state (or if we don't care about state-equality reduction) */ if (visited_state_ == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ - for (auto const& [aid, _] : next_state->get_actors_list()) { - if (next_state->is_actor_enabled(aid) and not next_state->is_actor_done(aid)) { - next_state->mark_todo(aid); - if (reduction_mode_ == ReductionMode::dpor) - break; // With DPOR, we take the first enabled transition - } - } + if (reduction_mode_ == ReductionMode::dpor) + next_state->consider_best(); // Take only one transition if DPOR: others may be considered later if required + else + next_state->consider_all(); dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(), state->get_transition()->dot_string().c_str()); @@ -240,14 +237,14 @@ void DFSExplorer::backtrack() if (prev_state->is_actor_enabled(issuer_id)) { if (not prev_state->is_actor_done(issuer_id)) - prev_state->mark_todo(issuer_id); + prev_state->consider_one(issuer_id); 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); - prev_state->mark_all_enabled_todo(); + prev_state->consider_all(); } break; } else { @@ -317,16 +314,11 @@ DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Explo /* Get an enabled actor and insert it in the interleave set of the initial state */ XBT_DEBUG("Initial state. %lu actors to consider", initial_state->get_actor_count()); - for (auto const& [aid, _] : initial_state->get_actors_list()) { - if (initial_state->is_actor_enabled(aid)) { - initial_state->mark_todo(aid); - if (reduction_mode_ == ReductionMode::dpor) { - XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid); - break; - } - XBT_DEBUG("Actor %ld is TODO", aid); - } - } + if (reduction_mode_ == ReductionMode::dpor) + initial_state->consider_best(); + else + initial_state->consider_all(); + stack_.push_back(std::move(initial_state)); } diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 370a146d0b..bd332375fb 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -307,7 +307,7 @@ std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt /* Add all enabled actors to the interleave set of the initial state */ for (auto const& [aid, _] : next_pair->app_state_->get_actors_list()) if (next_pair->app_state_->is_actor_enabled(aid)) - next_pair->app_state_->mark_todo(aid); + next_pair->app_state_->consider_one(aid); next_pair->requests = next_pair->app_state_->count_todo(); /* FIXME : get search_cycle value for each accepting state */ diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 4863807268..1506a16cdd 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -208,7 +208,7 @@ std::unique_ptr UdporChecker::record_current_state() auto next_state = this->get_current_state(); // In UDPOR, we care about all enabled transitions in a given state - next_state->mark_all_enabled_todo(); + next_state->consider_all(); return next_state; }