src/mc/checker/SafetyChecker.hpp

   1 /* Copyright (c) 2008-2020. 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   ~SafetyChecker() override = default;
  28   void run() override;
  29   RecordTrace get_record_trace() override;
  30   std::vector<std::string> get_textual_trace() override;
  31   void log_state() override;
  32
  33 private:
  34   void check_non_termination(const State* current_state);
  35   void backtrack();
  36   void restore_state();
  37
  38   /** Stack representing the position in the exploration graph */
  39   std::list<std::unique_ptr<State>> stack_;
  40   VisitedStates visited_states_;
  41   std::unique_ptr<VisitedState> visited_state_;
  42   unsigned long expanded_states_count_ = 0;
  43 };
  44
  45 } // namespace mc
  46 } // namespace simgrid
  47
  48 #endif