From 703034660fc3125f6a9910bb10eba26d1a6750df Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Thu, 21 Dec 2017 00:39:14 +0100
Subject: [PATCH] high level counterexamples

---
 src/core/counterexample.cpp | 16 ++++++++++++++++
 src/core/counterexample.h   |  5 +++++
 src/mod_core.cpp            |  2 ++
 3 files changed, 23 insertions(+)
 create mode 100644 src/core/counterexample.cpp
 create mode 100644 src/core/counterexample.h

diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp
new file mode 100644
index 0000000..9676790
--- /dev/null
+++ b/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)
+            ;
+
+
+}
diff --git a/src/core/counterexample.h b/src/core/counterexample.h
new file mode 100644
index 0000000..aa82a95
--- /dev/null
+++ b/src/core/counterexample.h
@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_counterexamples(py::module& m);
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 583eff6..f7f1140 100644
--- a/src/mod_core.cpp
+++ b/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);