#include <string>
#include <vector>
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/checker/Checker.hpp"
#include "src/mc/VisitedState.hpp"
+#include "src/mc/checker/Checker.hpp"
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/mc_safety.h"
namespace simgrid {
namespace mc {
class XBT_PRIVATE SafetyChecker : public Checker {
simgrid::mc::ReductionMode reductionMode_ = simgrid::mc::ReductionMode::unset;
public:
- SafetyChecker(Session& session);
- ~SafetyChecker();
- int run() override;
+ explicit SafetyChecker(Session& session);
+ ~SafetyChecker() = default;
+ void run() override;
RecordTrace getRecordTrace() override;
std::vector<std::string> getTextualTrace() override;
void logState() override;
private:
- bool checkNonTermination(simgrid::mc::State* current_state);
- int backtrack();
+ void checkNonTermination(simgrid::mc::State* current_state);
+ void backtrack();
void restoreState();
private:
/** Stack representing the position in the exploration graph */
