high level counterexamples

src/core/counterexample.cpp

@@ -0,0 +1,16 @@
+#include "counterexample.h"
+#include "storm/environment/Environment.h"
+
+using namespace storm::counterexamples;
+
+// Define python bindings
+void define_counterexamples(py::module& m) {
+    py::class_<boost::container::flat_set<uint_fast64_t>>(m, "FlatSet", "Container to pass to program");
+
+
+            py::class_<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend").
+            def_static("build", &SMTMinimalLabelSetGenerator<double>::computeCounterexampleCommandSet)
+            ;
+
+
+}

src/core/counterexample.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_counterexamples(py::module& m);

src/mod_core.cpp

@@ -6,6 +6,7 @@
 #include "core/bisimulation.h"
 #include "core/input.h"
 #include "core/analysis.h"
+#include "core/counterexample.h"
 #include "core/environment.h"
 
 PYBIND11_MODULE(core, m) {
@@ -23,6 +24,7 @@ PYBIND11_MODULE(core, m) {
     define_export(m);
     define_result(m);
     define_modelchecking(m);
+    define_counterexamples(m);
     define_bisimulation(m);
     define_input(m);
     define_graph_constraints(m);