1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
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. */
6 #ifndef SIMGRID_MC_BASICSTRATEGY_HPP
7 #define SIMGRID_MC_BASICSTRATEGY_HPP
9 #include "Strategy.hpp"
11 namespace simgrid::mc {
13 /** Basic MC guiding class which corresponds to no guide. When asked for different states
14 * it will follow a depth first search politics to minize the number of opened states. */
15 class BasicStrategy : public Strategy {
16 int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer
19 void copy_from(const Strategy* strategy) override
21 const BasicStrategy* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
22 xbt_assert(cast_strategy != nullptr);
23 depth_ = cast_strategy->depth_ - 1;
24 xbt_assert(depth_ > 0, "The exploration reached a depth greater than %d. We will stop here to prevent weird interaction with DFSExplorer. If you want to change that behaviour, you should augment the size of the search by using --cfg=model-check/max-depth:", _sg_mc_max_depth.get());
26 BasicStrategy() = default;
27 ~BasicStrategy() override = default;
29 std::pair<aid_t, int> best_transition(bool must_be_todo) const override {
30 for (auto const& [aid, actor] : actors_to_run_) {
31 /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
32 if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done()) {
36 return std::make_pair(aid, depth_);
38 return std::make_pair(-1, depth_);
41 void execute_next(aid_t aid, RemoteApp& app) override { return; }
44 } // namespace simgrid::mc