1 /* Copyright (c) 2016. The SimGrid Team.
2 * All rights reserved. */
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. */
7 #ifndef SIMGRID_MC_CHECKER_HPP
8 #define SIMGRID_MC_CHECKER_HPP
14 #include "src/mc/mc_forward.hpp"
15 #include "src/mc/mc_record.h"
16 #include "src/mc/Session.hpp"
21 /** A model-checking algorithm
23 * The goal is to move the data/state/configuration of a model-checking
24 * algorihms in subclasses. Implementing this interface will probably
25 * not be really mandatory, you might be able to write your
26 * model-checking algorithm as plain imperative code instead.
28 * It works by manipulating a model-checking Session.
34 Checker(Session& session);
37 Checker(Checker const&) = delete;
38 Checker& operator=(Checker const&) = delete;
41 virtual int run() = 0;
43 // Give me your internal state:
45 /** Show the current trace/stack
47 * Could this be handled in the Session/ModelChecker instead?
49 virtual RecordTrace getRecordTrace();
50 virtual std::vector<std::string> getTextualTrace();
51 virtual void logState();
54 Session& getSession() { return *session_; }
57 XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
58 XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
59 XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);