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_enabled_todo()
{
- for (auto& [aid, actor] : actors_to_run_) {
-
- if (actor.is_enabled() and not actor.is_done() and not actor.is_todo())
- actor.mark_todo();
+ for (auto const& [aid, _] : this->get_actors_list()) {
- if (this->is_actor_enabled(aid)) {
++ if (this->is_actor_enabled(aid) and not is_actor_done(aid)) {
+ this->mark_todo(aid);
+ }
}
}
long get_num() const { return num_; }
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();
- bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
+ void mark_all_enabled_todo();
- bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
++ bool is_actor_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
std::map<aid_t, ActorState> const& get_actors_list() const { return actors_to_run_; }
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_done(aid)) {
- if (next_state->is_actor_enabled(aid)) {
++ 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
XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
- if (not prev_state->is_done(issuer_id))
- prev_state->mark_todo(issuer_id);
- else
- XBT_DEBUG("Actor %ld is in done set", issuer_id);
+ if (prev_state->is_actor_enabled(issuer_id)){
- if (not prev_state->is_done(issuer_id))
++ if (not prev_state->is_actor_done(issuer_id))
+ prev_state->mark_todo(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_todo();
++ prev_state->mark_all_enabled_todo();
+ }
break;
} else {
XBT_VERB("INDEPENDENT Transitions:");