#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
+ * algorithms 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.
*
* Could this be handled in the Session/ModelChecker instead?
*/
virtual RecordTrace getRecordTrace();
+ virtual std::vector<std::string> getTextualTrace();
+ virtual void logState();
protected:
Session& getSession() { return *session_; }
};
+XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
+XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
+XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);
+
}
}