Bases for wait distance guide

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 868d8fb..a839b28 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/api/State.hpp"
 #include "src/mc/api/guide/BasicGuide.hpp"
+//#include "src/mc/api/guide/WaitGuide.hpp"
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
 
@@ -16,10 +17,13 @@ namespace simgrid::mc {
 
 long State::expended_states_ = 0;
 
-State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_unique<BasicGuide>())
+State::State(RemoteApp& remote_app) : num_(++expended_states_)
 {
-  remote_app.get_actors_status(guide->actors_to_run_);
-
+  remote_app.get_actors_status(guide_->actors_to_run_);
+  if (_sg_mc_guided == "none")  
+      guide_ = std::make_unique<BasicGuide>();
+  if (_sg_mc_guided == "nb_wait")
+      guide_ = std::make_unique<BasicGuide>();  
   /* Stateful model checking */
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
     system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
@@ -27,11 +31,15 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_), guide(std::make_
 }
 
 State::State(RemoteApp& remote_app, const State* parent_state)
-    : num_(++expended_states_), parent_state_(parent_state), guide(std::make_unique<BasicGuide>())
+    : num_(++expended_states_), parent_state_(parent_state)
 {
-
-  remote_app.get_actors_status(guide->actors_to_run_);
-
+    
+    remote_app.get_actors_status(guide_->actors_to_run_);
+    if (_sg_mc_guided == "none")  
+       guide_ = std::make_unique<BasicGuide>();
+    if (_sg_mc_guided == "nb_wait")
+       guide_ = std::make_unique<BasicGuide>();        
+    
   /* Stateful model checking */
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
     system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
@@ -47,10 +55,10 @@ State::State(RemoteApp& remote_app, const State* parent_state)
       if (not parent_state_->get_transition()->depends(&transition)) {
 
         sleep_set_.emplace(aid, transition);
-        if (guide->actors_to_run_.count(aid) != 0) {
+        if (guide_->actors_to_run_.count(aid) != 0) {
           XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
 
-          guide->actors_to_run_.at(aid).mark_done();
+          guide_->actors_to_run_.at(aid).mark_done();
         }
       } else
         XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
@@ -61,7 +69,7 @@ State::State(RemoteApp& remote_app, const State* parent_state)
 
 std::size_t State::count_todo() const
 {
-  return boost::range::count_if(this->guide->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
+  return boost::range::count_if(this->guide_->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
 }
 
 Transition* State::get_transition() const
@@ -71,8 +79,8 @@ Transition* State::get_transition() const
 
 aid_t State::next_transition() const
 {
-  XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide->actors_to_run_.size());
-  for (auto const& [aid, actor] : guide->actors_to_run_) {
+  XBT_DEBUG("Search for an actor to run. %zu actors to consider", guide_->actors_to_run_.size());
+  for (auto const& [aid, actor] : guide_->actors_to_run_) {
     /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
     if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
 
@@ -95,7 +103,7 @@ aid_t State::next_transition() const
 
 std::pair<aid_t, double> State::next_transition_guided() const
 {
-  return guide->next_transition();
+  return guide_->next_transition();
 }
 
 // This should be done in GuidedState, or at least interact with it
@@ -105,7 +113,7 @@ void State::execute_next(aid_t next, RemoteApp& app)
 
   // 1. Identify the appropriate ActorState to prepare for execution
   // when simcall_handle will be called on it
-  auto& actor_state                        = guide->actors_to_run_.at(next);
+  auto& actor_state                        = guide_->actors_to_run_.at(next);
   const unsigned times_considered          = actor_state.do_consider();
   const auto* expected_executed_transition = actor_state.get_transition(times_considered);
   xbt_assert(expected_executed_transition != nullptr,

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 8626d99..f0994e8 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -43,7 +43,7 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
       and for guided model-checking */
   const State* parent_state_;
 
-  std::unique_ptr<GuidedState> guide;
+  std::unique_ptr<GuidedState> guide_;
 
   /* 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
@@ -67,17 +67,21 @@ public:
   long get_num() const { return num_; }
   std::size_t count_todo() const;
 
-  void consider_one(aid_t aid) { guide->consider_one(aid); }
-  void consider_best() { guide->consider_best(); }
-  void consider_all() { guide->consider_all(); }
+  /* Marking as TODO some actor in this state:
+   *  + consider_one mark aid actor (and assert it is possible)
+   *  + consider_best ensure one actor is marked by eventually marking the best regarding its guiding methode
+   *  + conside_all mark all enabled actor that are not done yet */
+  void consider_one(aid_t aid) { guide_->consider_one(aid); }
+  void consider_best() { guide_->consider_best(); }
+  void consider_all() { guide_->consider_all(); }
 
-  bool is_actor_done(aid_t actor) const { return guide->actors_to_run_.at(actor).is_done(); }
+  bool is_actor_done(aid_t actor) const { return guide_->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 guide->actors_to_run_; }
+  std::map<aid_t, ActorState> const& get_actors_list() const { return guide_->actors_to_run_; }
 
-  unsigned long get_actor_count() const { return guide->actors_to_run_.size(); }
-  bool is_actor_enabled(aid_t actor) { return guide->actors_to_run_.at(actor).is_enabled(); }
+  unsigned long get_actor_count() const { return guide_->actors_to_run_.size(); }
+  bool is_actor_enabled(aid_t actor) { return guide_->actors_to_run_.at(actor).is_enabled(); }
 
   Snapshot* get_system_state() const { return system_state_.get(); }
   void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }

diff --git a/src/mc/api/guide/BasicGuide.hpp b/src/mc/api/guide/BasicGuide.hpp
index daa5733..aaba45a 100644 (file)
--- a/src/mc/api/guide/BasicGuide.hpp
+++ b/src/mc/api/guide/BasicGuide.hpp
@@ -9,9 +9,10 @@
 namespace simgrid::mc {
 
 /** Basic MC guiding class which corresponds to no guide at all (random choice) */
-// Not Yet fully implemented
 class BasicGuide : public GuidedState {
 public:
+  void operator=(const GuidedState&) { return; }
+
   std::pair<aid_t, double> next_transition() const override
   {
 

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index edf1316..e61a250 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -173,7 +173,7 @@ void DFSExplorer::run()
     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->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
-    
+
     /* DPOR persistent set procedure:
      * for each new transition considered, check if it depends on any other previous transition executed before it
      * on another process. If there exists one, find the more recent, and add its process to the interleave set.
@@ -259,7 +259,6 @@ void DFSExplorer::backtrack()
 
     stack_.pop_back();
 
-
     if (state->count_todo() == 0) { // Empty interleaving set: exploration at this level is over
       XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
 

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 3416d5c..663961d 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -60,6 +60,14 @@ simgrid::config::Flag<bool> _sg_mc_sleep_set{
     "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", false,
     [](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }};
 
+simgrid::config::Flag<std::string> _sg_mc_guided{
+    "model-check/guided-mc", "Specify the the kind of heuristic to use for guided model-checking", "none",
+    [](std::string_view value) {
+      if (value != "none" && value != "nb_wait")
+        xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value");
+    }};
+
+
 simgrid::config::Flag<int> _sg_mc_checkpoint{
     "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
                               "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index a900f7c..f411e7c 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -27,5 +27,8 @@ extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;
 extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;
 extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_termination;
 extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sleep_set;
+extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_guided;
+
+
 
 #endif