#include <functional>
#include <memory>
+#include <string>
#include "src/mc/mc_forward.hpp"
+#include "src/mc/mc_record.h"
namespace simgrid {
namespace mc {
class Checker {
Session* session_;
public:
- Checker(Session& session) : session_(&session) {}
+ Checker(Session& session);
// No copy:
Checker(Checker const&) = delete;
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<std::string> getTextualTrace();
+
protected:
Session& getSession() { return *session_; }
};
-/** Adapt a std::function to a checker */
-class FunctionalChecker : public Checker {
- Session* session_;
- std::function<int(Session& session)> function_;
-public:
- FunctionalChecker(Session& session, std::function<int(Session& session)> 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);
}
}