A few spelling mistakes and many replacements: [Ss]imgrid -> SimGrid.

[simgrid.git] / src / mc / api / State.cpp

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 1f8786d1a57d55d3690a43976ed07d2ccc69f8c8..0b6fc023444ec37a69a67fe4900a92f888629d0c 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -5,9 +5,12 @@
 
 #include "src/mc/api/State.hpp"
 #include "src/mc/api/strategy/BasicStrategy.hpp"
-#include "src/mc/api/strategy/WaitStrategy.hpp"
+#include "src/mc/api/strategy/MaxMatchComm.hpp"
+#include "src/mc/api/strategy/MinMatchComm.hpp"
+#include "src/mc/api/strategy/UniformStrategy.hpp"
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
+#include "xbt/random.hpp"
 
 #include <algorithm>
 #include <boost/range/algorithm.hpp>
@@ -21,10 +24,18 @@ long State::expended_states_ = 0;
 State::State(RemoteApp& remote_app) : num_(++expended_states_)
 {
   XBT_VERB("Creating a guide for the state");
+
+  
   if (_sg_mc_strategy == "none")
     strategy_ = std::make_shared<BasicStrategy>();
-  else if (_sg_mc_strategy == "nb_wait")
-    strategy_ = std::make_shared<WaitStrategy>();
+  else if (_sg_mc_strategy == "max_match_comm")
+    strategy_ = std::make_shared<MaxMatchComm>();
+  else if (_sg_mc_strategy == "min_match_comm")
+    strategy_ = std::make_shared<MinMatchComm>();
+  else if (_sg_mc_strategy == "uniform") {
+    xbt::random::set_mersenne_seed(_sg_mc_random_seed);  
+    strategy_ = std::make_shared<UniformStrategy>();
+  }
   else
     THROW_IMPOSSIBLE;
 
@@ -41,13 +52,18 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
 State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
     : incoming_transition_(parent_state->get_transition_out()), num_(++expended_states_), parent_state_(parent_state)
 {
-  if (_sg_mc_strategy == "none")
+    
+   if (_sg_mc_strategy == "none")
     strategy_ = std::make_shared<BasicStrategy>();
-  else if (_sg_mc_strategy == "nb_wait")
-    strategy_ = std::make_shared<WaitStrategy>();
+  else if (_sg_mc_strategy == "max_match_comm")
+    strategy_ = std::make_shared<MaxMatchComm>();
+  else if (_sg_mc_strategy == "min_match_comm")
+    strategy_ = std::make_shared<MinMatchComm>();
+  else if (_sg_mc_strategy == "uniform") 
+    strategy_ = std::make_shared<UniformStrategy>();
   else
     THROW_IMPOSSIBLE;
-  *strategy_ = *(parent_state->strategy_);
+  strategy_->copy_from(parent_state_->strategy_.get());
 
   remote_app.get_actors_status(strategy_->actors_to_run_);
 
@@ -62,7 +78,7 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
     /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
      * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
      * it is not explored*/
-    for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
+    for (const auto& [aid, transition] : parent_state_->get_sleep_set()) {
       if (not incoming_transition_->depends(transition.get())) {
         sleep_set_.try_emplace(aid, transition);
         if (strategy_->actors_to_run_.count(aid) != 0) {
@@ -213,9 +229,7 @@ void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
       if (actor.is_enabled()) {
         // For each variant of the transition, we want
         // to insert the action into the tree. This ensures
-        // that all variants are searched?
-        //
-        // TODO: How do we modify sleep sets then?
+        // that all variants are searched
         for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
           wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
         }
@@ -273,7 +287,15 @@ void State::do_odpor_unwind()
 {
   if (auto out_transition = get_transition_out(); out_transition != nullptr) {
     remove_subtree_using_current_out_transition();
-    add_sleep_set(std::move(out_transition));
+
+    // Only when we've exhausted all variants of the transition which
+    // can be chosen from this state do we finally add the actor to the
+    // sleep set. This ensures that the current logic handling sleep sets
+    // works with ODPOR in the way we intend it to work. There is not a
+    // good way to perform transition equality in SimGrid; instead, we
+    // effectively simply check for the presence of an actor in the sleep set.
+    if (!get_actors_list().at(out_transition->aid_).has_more_to_consider())
+      add_sleep_set(std::move(out_transition));
   }
 }