X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/02a0b077329593921105001a7f27463ba2d82ced..201605b6315d5474e458c655eb4fb9952151b732:/src/mc/api/ActorState.hpp diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp index 16232ff53a..ed40454646 100644 --- a/src/mc/api/ActorState.hpp +++ b/src/mc/api/ActorState.hpp @@ -9,6 +9,7 @@ #include "src/kernel/activity/CommImpl.hpp" #include "src/mc/remote/RemotePtr.hpp" +#include #include #include @@ -26,7 +27,6 @@ namespace simgrid::mc { * is important in cases */ class ActorState { - /** * @brief The transitions that the actor is allowed to execute from this * state, viz. those that are enabled for this actor @@ -41,7 +41,7 @@ class ActorState { * such transitions such that `pending_transitions_[i]` represents * the variation of the transition with `times_considered = i`. * - * TODO: If only a subset of transitions of an actor that can + * @note: If only a subset of transitions of an actor that can * take multiple transitions in some state are truly enabled, * we would instead need to map `times_considered` to a transition, * as the map is currently implicit in the ordering of the transitions @@ -54,7 +54,7 @@ class ActorState { * This means there may be a way to store the list once and apply differences * rather than repeating elements frequently. */ - std::vector> pending_transitions_; + std::vector> pending_transitions_; /* Possible exploration status of an actor transition in a state. * Either the checker did not consider the transition, or it was considered and still to do, or considered and @@ -87,18 +87,21 @@ class ActorState { public: ActorState(aid_t aid, bool enabled, unsigned int max_consider) : ActorState(aid, enabled, max_consider, {}) {} - ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector> transitions) - : aid_(aid), max_consider_(max_consider), enabled_(enabled), pending_transitions_(std::move(transitions)) + ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector> transitions) + : pending_transitions_(std::move(transitions)), aid_(aid), max_consider_(max_consider), enabled_(enabled) { } unsigned int do_consider() { if (max_consider_ <= times_considered_ + 1) - set_done(); + mark_done(); return times_considered_++; } + unsigned int get_max_considered() const { return max_consider_; } unsigned int get_times_considered() const { return times_considered_; } + unsigned int get_times_not_considered() const { return max_consider_ - times_considered_; } + bool has_more_to_consider() const { return get_times_not_considered() > 0; } aid_t get_aid() const { return aid_; } /* returns whether the actor is marked as enabled in the application side */ @@ -113,25 +116,57 @@ public: this->state_ = InterleavingType::todo; this->times_considered_ = 0; } - void set_done() { this->state_ = InterleavingType::done; } + void mark_done() { this->state_ = InterleavingType::done; } - inline Transition* get_transition(unsigned times_considered) + /** + * @brief Retrieves the transition that we should consider for execution by + * this actor from the State instance with respect to which this ActorState object + * is considered + */ + std::shared_ptr get_transition() const + { + // The rationale for this selection is as follows: + // + // 1. For transitions with only one possibility of execution, + // we always wish to select action `0` even if we've + // marked the transition already as considered (which + // we'll do if we explore a trace following that transition). + // + // 2. For transitions that can be considered multiple + // times, we want to be sure to select the most up-to-date + // action. In general, this means selecting that which is + // now being considered at this state. If, however, we've + // executed the + // + // The formula satisfies both of the above conditions: + // + // > std::clamp(times_considered_, 0u, max_consider_ - 1) + return get_transition(std::clamp(times_considered_, 0u, max_consider_ - 1)); + } + + std::shared_ptr get_transition(unsigned times_considered) const { xbt_assert(times_considered < this->pending_transitions_.size(), - "Actor %lu does not have a state available transition with `times_considered = %d`,\n" + "Actor %ld does not have a state available transition with `times_considered = %u`,\n" "yet one was asked for", aid_, times_considered); - return this->pending_transitions_[times_considered].get(); + return this->pending_transitions_[times_considered]; } - inline void set_transition(std::unique_ptr t, unsigned times_considered) + void set_transition(std::shared_ptr t, unsigned times_considered) { xbt_assert(times_considered < this->pending_transitions_.size(), - "Actor %lu does not have a state available transition with `times_considered = %d`, " + "Actor %ld does not have a state available transition with `times_considered = %u`, " "yet one was attempted to be set", aid_, times_considered); this->pending_transitions_[times_considered] = std::move(t); } + + const std::vector>& get_enabled_transitions() const + { + static const auto no_enabled_transitions = std::vector>(); + return this->is_enabled() ? this->pending_transitions_ : no_enabled_transitions; + }; }; } // namespace simgrid::mc