X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5787a5c839c1f49fec942290449d18b72b036d98..0433449947b08247ca57c84e32f547c35e351145:/src/mc/Checker.hpp diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp index 478665a8f9..8f7e0cc2e6 100644 --- a/src/mc/Checker.hpp +++ b/src/mc/Checker.hpp @@ -9,8 +9,11 @@ #include #include +#include #include "src/mc/mc_forward.hpp" +#include "src/mc/mc_record.h" +#include "src/mc/Session.hpp" namespace simgrid { namespace mc { @@ -28,7 +31,7 @@ namespace mc { class Checker { Session* session_; public: - Checker(Session& session) : session_(&session) {} + Checker(Session& session); // No copy: Checker(Checker const&) = delete; @@ -37,20 +40,22 @@ public: virtual ~Checker(); virtual int run() = 0; + // Give me your internal state: + + /** Show the current trace/stack + * + * Could this be handled in the Session/ModelChecker instead? + */ + virtual RecordTrace getRecordTrace(); + virtual std::vector getTextualTrace(); + protected: Session& getSession() { return *session_; } }; -/** Adapt a std::function to a checker */ -class FunctionalChecker : public Checker { - Session* session_; - std::function function_; -public: - FunctionalChecker(Session& session, std::function f) - : Checker(session), function_(std::move(f)) {} - ~FunctionalChecker(); - int run() override; -}; +XBT_PUBLIC() Checker* createLivenessChecker(Session& session); +XBT_PUBLIC() Checker* createSafetyChecker(Session& session); +XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session); } }