src/mc/checker/SafetyChecker.hpp

   1 /* Copyright (c) 2008-2022. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
   8 #define SIMGRID_MC_SAFETY_CHECKER_HPP
   9
  10 #include "src/mc/VisitedState.hpp"
  11 #include "src/mc/checker/Checker.hpp"
  12 #include "src/mc/mc_safety.hpp"
  13
  14 #include <list>
  15 #include <memory>
  16 #include <string>
  17 #include <vector>
  18
  19 namespace simgrid {
  20 namespace mc {
  21
  22 class XBT_PRIVATE SafetyChecker : public Checker {
  23   ReductionMode reductionMode_ = ReductionMode::unset;
  24
  25 public:
  26   explicit SafetyChecker(Session* session);
  27   void run() override;
  28   RecordTrace get_record_trace() override;
  29   std::vector<std::string> get_textual_trace() override;
  30   void log_state() override;
  31
  32 private:
  33   void check_non_termination(const State* current_state);
  34   void backtrack();
  35   void restore_state();
  36
  37   /** Stack representing the position in the exploration graph */
  38   std::list<std::unique_ptr<State>> stack_;
  39   VisitedStates visited_states_;
  40   std::unique_ptr<VisitedState> visited_state_;
  41   unsigned long expanded_states_count_ = 0;
  42 };
  43
  44 } // namespace mc
  45 } // namespace simgrid
  46
  47 #endif