Rename ActorState::consider() and State::add_interleaved_set() as {ActorState,State...

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index eb2d666..7e5b02f 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -321,7 +321,7 @@ void CommunicationDeterminismChecker::prepare()
   auto actors = api::get().get_actors();
   for (auto& actor : actors)
     if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-      initial_state->add_interleaving_set(actor.copy.get_buffer());
+      initial_state->mark_todo(actor.copy.get_buffer());
 
   stack_.push_back(std::move(initial_state));
 }
@@ -422,7 +422,7 @@ void CommunicationDeterminismChecker::real_run()
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG("Exploration depth = %zu (state = %d, interleaved processes = %zu)", stack_.size(), cur_state->num_,
-              cur_state->interleave_size());
+              cur_state->count_todo());
 
     /* Update statistics */
     api::get().mc_inc_visited_states();
@@ -476,7 +476,7 @@ void CommunicationDeterminismChecker::real_run()
         auto actors = api::get().get_actors();
         for (auto& actor : actors)
           if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-            next_state->add_interleaving_set(actor.copy.get_buffer());
+            next_state->mark_todo(actor.copy.get_buffer());
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str());
@@ -512,7 +512,7 @@ void CommunicationDeterminismChecker::real_run()
       while (not stack_.empty()) {
         std::unique_ptr<State> state(std::move(stack_.back()));
         stack_.pop_back();
-        if (state->interleave_size() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
+        if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
           stack_.push_back(std::move(state));

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 3f2030e..705ce85 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -264,8 +264,8 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
   auto actors = api::get().get_actors();
   for (auto& actor : actors)
     if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
-      next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
-  next_pair->requests = next_pair->graph_state->interleave_size();
+      next_pair->graph_state->mark_todo(actor.copy.get_buffer());
+  next_pair->requests = next_pair->graph_state->count_todo();
   /* FIXME : get search_cycle value for each accepting state */
   if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
     next_pair->search_cycle = true;
@@ -326,8 +326,8 @@ void LivenessChecker::run()
 
     XBT_DEBUG(
         "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",
-        current_pair->depth, current_pair->search_cycle, current_pair->graph_state->interleave_size(),
-        current_pair->num, current_pair->requests);
+        current_pair->depth, current_pair->search_cycle, current_pair->graph_state->count_todo(), current_pair->num,
+        current_pair->requests);
 
     if (current_pair->requests == 0) {
       this->backtrack();

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 049d3fb..c1d4620 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -86,7 +86,7 @@ void SafetyChecker::run()
 
     XBT_DEBUG("**************************************************");
     XBT_VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num_,
-             state->interleave_size());
+             state->count_todo());
 
     api::get().mc_inc_visited_states();
 
@@ -151,7 +151,7 @@ void SafetyChecker::run()
       for (auto& remoteActor : actors) {
         auto actor = remoteActor.copy.get_buffer();
         if (api::get().actor_is_enabled(actor->get_pid())) {
-          next_state->add_interleaving_set(actor);
+          next_state->mark_todo(actor);
           if (reductionMode_ == ReductionMode::dpor)
             break; // With DPOR, we take the first enabled transition
         }
@@ -212,7 +212,7 @@ void SafetyChecker::backtrack()
           }
 
           if (not prev_state->actor_states_[issuer->get_pid()].is_done())
-            prev_state->add_interleaving_set(issuer);
+            prev_state->mark_todo(issuer);
           else
             XBT_DEBUG("Process %p is in done set", req->issuer_);
           break;
@@ -229,7 +229,7 @@ void SafetyChecker::backtrack()
       }
     }
 
-    if (state->interleave_size() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
+    if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
       /* We found a back-tracking point, let's loop */
       XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
       stack_.push_back(std::move(state));
@@ -294,7 +294,7 @@ SafetyChecker::SafetyChecker() : Checker()
   auto actors = api::get().get_actors();
   for (auto& actor : actors)
     if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
-      initial_state->add_interleaving_set(actor.copy.get_buffer());
+      initial_state->mark_todo(actor.copy.get_buffer());
       if (reductionMode_ != ReductionMode::none)
         break;
     }

diff --git a/src/mc/mc_pattern.hpp b/src/mc/mc_pattern.hpp
index 7026e56..385224d 100644 (file)
--- a/src/mc/mc_pattern.hpp
+++ b/src/mc/mc_pattern.hpp
@@ -78,7 +78,7 @@ public:
   bool is_done() const { return this->state == InterleavingType::done; }
   bool is_todo() const { return this->state == InterleavingType::todo; }
   /** Mark that we should try executing this process at some point in the future of the checker algorithm */
-  void consider()
+  void mark_todo()
   {
     this->state            = InterleavingType::todo;
     this->times_considered = 0;

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 26901e6..a93afe2 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -31,7 +31,7 @@ State::State(unsigned long state_number) : num_(state_number)
   }
 }
 
-std::size_t State::interleave_size() const
+std::size_t State::count_todo() const
 {
   return boost::range::count_if(this->actor_states_, [](simgrid::mc::ActorState const& a) { return a.is_todo(); });
 }

diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp
index f932313..7b40cd8 100644 (file)
--- a/src/mc/mc_state.hpp
+++ b/src/mc/mc_state.hpp
@@ -46,11 +46,8 @@ public:
 
   explicit State(unsigned long state_number);
 
-  std::size_t interleave_size() const;
-  void add_interleaving_set(const simgrid::kernel::actor::ActorImpl* actor)
-  {
-    this->actor_states_[actor->get_pid()].consider();
-  }
+  std::size_t count_todo() const;
+  void mark_todo(const simgrid::kernel::actor::ActorImpl* actor) { this->actor_states_[actor->get_pid()].mark_todo(); }
   Transition get_transition() const;
 
 private: