updated doc

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index dae2c6f..1e676d4 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -62,7 +62,7 @@ std::size_t State::count_todo() const
   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_todo() 
 {
     for (auto & [aid, actor] : actors_to_run_) {
 

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index c10ca62..71670d3 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -29,6 +29,9 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   /** Snapshot of system state (if needed) */
   std::shared_ptr<Snapshot> system_state_;
 
+  /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
+   * set. With this information, it is check whether it should be removed from it or not when exploring a new
+   * transition */
   std::map<aid_t, Transition> sleep_set_;
   
 public:
@@ -44,7 +47,7 @@ public:
   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(); 
+  void mark_all_todo();
   bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
   Transition* get_transition() const;
   void set_transition(Transition* t) { transition_.reset(t); }
@@ -57,7 +60,7 @@ public:
   void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
 
   std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
-  void set_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); }
+  void add_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); }
   
   /* Returns the total amount of states created so far (for statistics) */
   static long get_expanded_states() { return expended_states_; }

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 15d30b9..e8bb0b0 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -146,7 +146,7 @@ void DFSExplorer::run()
     XBT_VERB("Sleep set actually containing:");
     for (auto & [aid, transition] : state->get_sleep_set()) {
       
-       XBT_VERB("###<%ld,%s>", aid, transition.to_string().c_str());
+       XBT_VERB("  <%ld,%s>", aid, transition.to_string().c_str());
       
     }
 
@@ -228,9 +228,9 @@ void DFSExplorer::backtrack()
     
     stack_.pop_back();
     
-    XBT_DEBUG("Maarking Transition >>%s<< of process %ld done and adding it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
+    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->set_sleep_set(state->get_transition());
+    state->add_sleep_set(state->get_transition());
 
     if (reduction_mode_ == ReductionMode::dpor) {
       aid_t issuer_id = state->get_transition()->aid_;
@@ -251,7 +251,7 @@ void DFSExplorer::backtrack()
              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);
+             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();
          }
           break;