src/mc/explo/DFSExplorer.hpp

   1 /* Copyright (c) 2008-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_SAFETY_CHECKER_HPP
   7 #define SIMGRID_MC_SAFETY_CHECKER_HPP
   8
   9 #include "src/mc/VisitedState.hpp"
  10 #include "src/mc/explo/Exploration.hpp"
  11
  12 #include <list>
  13 #include <memory>
  14 #include <string>
  15 #include <vector>
  16
  17 namespace simgrid::mc {
  18
  19 typedef std::list<std::shared_ptr<State>> stack_t;
  20
  21 /* Used to compare two stacks and decide which one is better to backtrack,
  22  * regarding the chosen guide in the last state. */
  23 class OpenedStatesCompare {
  24 public:
  25   bool operator()(std::shared_ptr<State> const& lhs, std::shared_ptr<State> const& rhs)
  26   {
  27     return lhs->next_transition_guided().second < rhs->next_transition_guided().second;
  28   }
  29 };
  30
  31 class XBT_PRIVATE DFSExplorer : public Exploration {
  32
  33   XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor);
  34
  35   ReductionMode reduction_mode_;
  36   unsigned long backtrack_count_      = 0; // for statistics
  37   unsigned long visited_states_count_ = 0; // for statistics
  38
  39   static xbt::signal<void(RemoteApp&)> on_exploration_start_signal;
  40   static xbt::signal<void(RemoteApp&)> on_backtracking_signal;
  41
  42   static xbt::signal<void(State*, RemoteApp&)> on_state_creation_signal;
  43
  44   static xbt::signal<void(State*, RemoteApp&)> on_restore_system_state_signal;
  45   static xbt::signal<void(RemoteApp&)> on_restore_initial_state_signal;
  46   static xbt::signal<void(Transition*, RemoteApp&)> on_transition_replay_signal;
  47   static xbt::signal<void(Transition*, RemoteApp&)> on_transition_execute_signal;
  48
  49   static xbt::signal<void(RemoteApp&)> on_log_state_signal;
  50
  51 public:
  52   explicit DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info = false);
  53   void run() override;
  54   RecordTrace get_record_trace() override;
  55   std::vector<std::string> get_textual_trace() override;
  56   void log_state() override;
  57
  58   /** Called once when the exploration starts */
  59   static void on_exploration_start(std::function<void(RemoteApp& remote_app)> const& f)
  60   {
  61     on_exploration_start_signal.connect(f);
  62   }
  63   /** Called each time that the exploration backtracks from a exploration end */
  64   static void on_backtracking(std::function<void(RemoteApp& remote_app)> const& f)
  65   {
  66     on_backtracking_signal.connect(f);
  67   }
  68   /** Called each time that a new state is create */
  69   static void on_state_creation(std::function<void(State*, RemoteApp& remote_app)> const& f)
  70   {
  71     on_state_creation_signal.connect(f);
  72   }
  73   /** Called when rollbacking directly onto a previously checkpointed state */
  74   static void on_restore_system_state(std::function<void(State*, RemoteApp& remote_app)> const& f)
  75   {
  76     on_restore_system_state_signal.connect(f);
  77   }
  78   /** Called when the state to which we backtrack was not checkpointed state, forcing us to restore the initial state
  79    * before replaying some transitions */
  80   static void on_restore_initial_state(std::function<void(RemoteApp& remote_app)> const& f)
  81   {
  82     on_restore_initial_state_signal.connect(f);
  83   }
  84   /** Called when replaying a transition that was previously executed, to reach a backtracked state */
  85   static void on_transition_replay(std::function<void(Transition*, RemoteApp& remote_app)> const& f)
  86   {
  87     on_transition_replay_signal.connect(f);
  88   }
  89   /** Called when executing a new transition */
  90   static void on_transition_execute(std::function<void(Transition*, RemoteApp& remote_app)> const& f)
  91   {
  92     on_transition_execute_signal.connect(f);
  93   }
  94   /** Called when displaying the statistics at the end of the exploration */
  95   static void on_log_state(std::function<void(RemoteApp&)> const& f) { on_log_state_signal.connect(f); }
  96
  97 private:
  98   void check_non_termination(const State* current_state);
  99   void backtrack();
 100
 101   /** Stack representing the position in the exploration graph */
 102   stack_t stack_;
 103   VisitedStates visited_states_;
 104   std::unique_ptr<VisitedState> visited_state_;
 105
 106   /** Opened states are states that still contains todo actors.
 107    *  When backtracking, we pick a state from it*/
 108
 109   std::priority_queue<std::shared_ptr<State>, std::vector<std::shared_ptr<State>>, OpenedStatesCompare> opened_states_;
 110
 111   /** Change current stack_ value to correspond to the one we would have
 112    *  had if we executed transition to get to state. This is required when
 113    *  backtracking, and achieved thanks to the fact states save their parent.*/
 114   void restore_stack(std::shared_ptr<State> state);
 115
 116   RecordTrace get_record_trace_of_stack(stack_t stack);
 117 };
 118
 119 } // namespace simgrid::mc
 120
 121 #endif