From 5e457d3b0feb4bc1cebfdd0d07e5c7c065785b25 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 16 Nov 2016 17:48:38 +0100
Subject: [PATCH] Convert PrismProgram to SymbolicModelDescription

Former-commit-id: 91f9de93d999befc365f751e3dcd40e3710d230b [formerly fa5c0246d37335ff5867ca4202285e9a813117f0]
Former-commit-id: b9947c4b0856d0985c449accc5d9eca9d8c17f47
---
 stormpy/src/core/core.cpp                 |  2 +-
 stormpy/src/core/{prism.cpp => input.cpp} | 12 ++++++++++--
 stormpy/src/core/input.h                  |  8 ++++++++
 stormpy/src/core/prism.h                  |  8 --------
 stormpy/src/mod_core.cpp                  |  4 ++--
 5 files changed, 21 insertions(+), 13 deletions(-)
 rename stormpy/src/core/{prism.cpp => input.cpp} (63%)
 create mode 100644 stormpy/src/core/input.h
 delete mode 100644 stormpy/src/core/prism.h

diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp
index 422ecb53d..98d74dc80 100644
--- a/stormpy/src/core/core.cpp
+++ b/stormpy/src/core/core.cpp
@@ -12,7 +12,7 @@ void define_core(py::module& m) {
 void define_parse(py::module& m) {
     // Parse formulas
     m.def("parse_formulas", &storm::parseFormulasForExplicit, "Parse explicit formulas", py::arg("formula_string"));
-    m.def("parse_formulas_for_prism_program", &storm::parseFormulasForProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program"));
+    m.def("parse_formulas_for_prism_program", &storm::parseFormulasForPrismProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program"));
 
     // Pair <Model,Formulas>
     py::class_<storm::storage::ModelFormulasPair>(m, "ModelFormulasPair", "Pair of model and formulas")
diff --git a/stormpy/src/core/prism.cpp b/stormpy/src/core/input.cpp
similarity index 63%
rename from stormpy/src/core/prism.cpp
rename to stormpy/src/core/input.cpp
index 9c88bc13d..8c9f915e4 100644
--- a/stormpy/src/core/prism.cpp
+++ b/stormpy/src/core/input.cpp
@@ -1,7 +1,7 @@
-#include "prism.h"
+#include "input.h"
 
 // Define python bindings
-void define_prism(py::module& m) {
+void define_input(py::module& m) {
 
     // Parse prism program
     m.def("parse_prism_program", &storm::parseProgram, "Parse prism program", py::arg("path"));
@@ -23,4 +23,12 @@ void define_prism(py::module& m) {
         .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants")
     ;
     
+    // SymbolicModelDescription
+    py::class_<storm::storage::SymbolicModelDescription>(m, "SymbolicModelDescription", "Symbolic description of model")
+        .def(py::init<storm::prism::Program const&>(), "Construct from Prism program", py::arg("prism_program"))
+        .def_property_readonly("is_prism_program", &storm::storage::SymbolicModelDescription::isPrismProgram, "Flag if program is in Prism format")
+    ;
+
+    // PrismProgram can be converted into SymbolicModelDescription
+    py::implicitly_convertible<storm::prism::Program, storm::storage::SymbolicModelDescription>();
 }
diff --git a/stormpy/src/core/input.h b/stormpy/src/core/input.h
new file mode 100644
index 000000000..304dc9a9f
--- /dev/null
+++ b/stormpy/src/core/input.h
@@ -0,0 +1,8 @@
+#ifndef PYTHON_CORE_INPUT_H_
+#define PYTHON_CORE_INPUT_H_
+
+#include "common.h"
+
+void define_input(py::module& m);
+
+#endif /* PYTHON_CORE_INPUT_H_ */
diff --git a/stormpy/src/core/prism.h b/stormpy/src/core/prism.h
deleted file mode 100644
index 6a4d43307..000000000
--- a/stormpy/src/core/prism.h
+++ /dev/null
@@ -1,8 +0,0 @@
-#ifndef PYTHON_CORE_PRISM_H_
-#define PYTHON_CORE_PRISM_H_
-
-#include "common.h"
-
-void define_prism(py::module& m);
-
-#endif /* PYTHON_CORE_PRISM_H_ */
diff --git a/stormpy/src/mod_core.cpp b/stormpy/src/mod_core.cpp
index a985aa228..b008e40d0 100644
--- a/stormpy/src/mod_core.cpp
+++ b/stormpy/src/mod_core.cpp
@@ -3,7 +3,7 @@
 #include "core/core.h"
 #include "core/modelchecking.h"
 #include "core/bisimulation.h"
-#include "core/prism.h"
+#include "core/input.h"
 
 PYBIND11_PLUGIN(core) {
     py::module m("core");
@@ -12,6 +12,6 @@ PYBIND11_PLUGIN(core) {
     define_build(m);
     define_modelchecking(m);
     define_bisimulation(m);
-    define_prism(m);
+    define_input(m);
     return m.ptr();
 }