Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of https://framagit.org/simgrid/simgrid
authormlaurent <mathieu.laurent@ens-rennes.fr>
Fri, 24 Feb 2023 14:42:51 +0000 (15:42 +0100)
committermlaurent <mathieu.laurent@ens-rennes.fr>
Fri, 24 Feb 2023 14:42:51 +0000 (15:42 +0100)
1  2 
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/explo/DFSExplorer.cpp

Simple merge
@@@ -61,12 -29,12 +61,12 @@@ std::size_t State::count_todo() cons
    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);
+     }
    }
  }
  
@@@ -59,9 -54,8 +59,8 @@@ public
    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_; }
@@@ -184,7 -165,7 +184,7 @@@ void DFSExplorer::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
@@@ -244,15 -216,10 +244,15 @@@ void DFSExplorer::backtrack(
            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:");