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"
20 /** A model-checking algorithm
22 * The goal is to move the data/state/configuration of a model-checking
23 * algorihms in subclasses. Implementing this interface will probably
24 * not be really mandatory, you might be able to write your
25 * model-checking algorithm as plain imperative code instead.
27 * It works by manipulating a model-checking Session.
33 Checker(Session& session);
36 Checker(Checker const&) = delete;
37 Checker& operator=(Checker const&) = delete;
40 virtual int run() = 0;
42 // Give me your internal state:
44 /** Show the current trace/stack
46 * Could this be handled in the Session/ModelChecker instead?
48 virtual RecordTrace getRecordTrace();
49 virtual std::vector<std::string> getTextualTrace();
52 Session& getSession() { return *session_; }
55 XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
56 XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
57 XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);