Use boost::iterator_facade for History::Iterator

[simgrid.git] / src / mc / explo / DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index a3e0c38..43dd7ce 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -143,13 +143,14 @@ void DFSExplorer::run()
       continue;
     }
 
-    XBT_VERB("Sleep set actually containing:");
-    for (auto & [aid, transition] : state->get_sleep_set()) {
-      
-       XBT_VERB("  <%ld,%s>", aid, transition.to_string().c_str());
+    if (_sg_mc_sleep_set) {
+       XBT_VERB("Sleep set actually containing:");
+       for (auto & [aid, transition] : state->get_sleep_set()) {
+   
+           XBT_VERB("  <%ld,%s>", aid, transition.to_string().c_str());
       
+       }
     }
-
     /* Actually answer the request: let's execute the selected request (MCed does one step) */
     state->execute_next(next);
     on_transition_execute_signal(state->get_transition(), get_remote_app());
@@ -164,7 +165,7 @@ void DFSExplorer::run()
 
     /* If we want sleep set reduction, pass the old state to the new state so it can
      * both copy the sleep set and eventually removes things from it locally */
-    if (sleep_set_reduction_)
+    if (_sg_mc_sleep_set)
        next_state = std::make_unique<State>(get_remote_app(), state); 
     else
        next_state = std::make_unique<State>(get_remote_app());
@@ -183,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) 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
@@ -228,8 +229,7 @@ void DFSExplorer::backtrack()
     stack_.pop_back();
     
     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->add_sleep_set(state->get_transition());
+    state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
 
     if (reduction_mode_ == ReductionMode::dpor) {
       aid_t issuer_id = state->get_transition()->aid_;
@@ -245,13 +245,13 @@ void DFSExplorer::backtrack()
           XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
 
          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 {
@@ -305,8 +305,6 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Explo
   else
     reduction_mode_ = ReductionMode::none;
 
-  sleep_set_reduction_ = _sg_mc_sleep_set;
-  
   if (_sg_mc_termination) {
     if (with_dpor) {
       XBT_INFO("Check non progressive cycles (turning DPOR off)");