src/mc/api/strategy/BasicStrategy.hpp

   1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #ifndef SIMGRID_MC_BASICSTRATEGY_HPP
   7 #define SIMGRID_MC_BASICSTRATEGY_HPP
   8
   9 #include "Strategy.hpp"
  10 #include "src/mc/explo/Exploration.hpp"
  11
  12 XBT_LOG_EXTERNAL_CATEGORY(mc_dfs);
  13
  14 namespace simgrid::mc {
  15
  16 /** Basic MC guiding class which corresponds to no guide. When asked for different states
  17  *  it will follow a depth first search politics to minize the number of opened states. */
  18 class BasicStrategy : public Strategy {
  19   int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positive value to work with
  20                                  // threshold in DFSExplorer
  21
  22 public:
  23   void copy_from(const Strategy* strategy) override
  24   {
  25     const auto* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
  26     xbt_assert(cast_strategy != nullptr);
  27     depth_ = cast_strategy->depth_ - 1;
  28     if (depth_ <= 0) {
  29       XBT_CERROR(mc_dfs,
  30                  "The exploration reached a depth greater than %d. Change the depth limit with "
  31                  "--cfg=model-check/max-depth. Here are the 100 first trace elements",
  32                  _sg_mc_max_depth.get());
  33       auto trace = Exploration::get_instance()->get_textual_trace(100);
  34       for (auto elm : trace)
  35         XBT_CERROR(mc_dfs, "  %s", elm.c_str());
  36       xbt_die("Aborting now.");
  37     }
  38   }
  39   BasicStrategy()                     = default;
  40   ~BasicStrategy() override           = default;
  41
  42   std::pair<aid_t, int> best_transition(bool must_be_todo) const override {
  43       for (auto const& [aid, actor] : actors_to_run_) {
  44           /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
  45           if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) {
  46         continue;
  47       }
  48
  49       return std::make_pair(aid, depth_);
  50     }
  51     return std::make_pair(-1, depth_);
  52   }
  53
  54   void execute_next(aid_t aid, RemoteApp& app) override { return; }
  55 };
  56
  57 } // namespace simgrid::mc
  58
  59 #endif