#include <functional>
#include <memory>
+#include <string>
#include "src/mc/mc_forward.hpp"
+#include "src/mc/mc_record.h"
+#include "src/mc/Session.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.
+ * This is an abstract base class used to group the data, state, configuration
+ * of a model-checking algorithm.
*
- * It works by manipulating a model-checking Session.
- */
+ * 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 is expected to interact with the model-checking core through the
+ * `Session` interface (but currently the `Session` interface does not
+ * have all the necessary features). */
// abstract
class Checker {
Session* session_;
public:
- Checker(Session& session) : session_(&session) {}
+ Checker(Session& session);
// No copy:
Checker(Checker const&) = delete;
Checker& operator=(Checker const&) = delete;
virtual ~Checker();
+
+ /** Main function of this algorithm */
virtual int run() = 0;
+ /* These methods are callbacks called by the model-checking engine
+ * to get and display information about the current state of the
+ * model-checking algorithm: */
+
+ /** Show the current trace/stack
+ *
+ * Could this be handled in the Session/ModelChecker instead? */
+ virtual RecordTrace getRecordTrace();
+
+ /** Generate a textual execution trace of the simulated application */
+ virtual std::vector<std::string> getTextualTrace();
+
+ /** Log additional information about the state of the model-checker */
+ virtual void logState();
+
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);
}
}
