[mc] Working on an interface between a model-checking session and a model-checking...

[simgrid.git] / src / mc / Checker.hpp

diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp
new file mode 100644 (file)
index 0000000..478665a
--- /dev/null
+++ b/src/mc/Checker.hpp
@@ -0,0 +1,58 @@
+/* Copyright (c) 2016. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_CHECKER_HPP
+#define SIMGRID_MC_CHECKER_HPP
+
+#include <functional>
+#include <memory>
+
+#include "src/mc/mc_forward.hpp"
+
+namespace simgrid {
+namespace mc {
+
+/** A model-checking algorithm
+ *
+ *  The goal is to move the data/state/configuration of a model-checking
+ *  algorihms in subclasses. Implementing this interface will probably
+ *  not be really mandatory, you might be able to write your
+ *  model-checking algorithm as plain imperative code instead.
+ *
+ *  It works by manipulating a model-checking Session.
+ */
+// abstract
+class Checker {
+  Session* session_;
+public:
+  Checker(Session& session) : session_(&session) {}
+
+  // No copy:
+  Checker(Checker const&) = delete;
+  Checker& operator=(Checker const&) = delete;
+
+  virtual ~Checker();
+  virtual int run() = 0;
+
+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;
+};
+
+}
+}
+
+#endif