+ * 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). */