Convert PrismProgram to SymbolicModelDescription

Former-commit-id: 91f9de93d9 [formerly fa5c0246d3]
Former-commit-id: b9947c4b08

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")

stormpy/src/core/prism.cpp → 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>();
 }

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_ */

stormpy/src/core/prism.h

@@ -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_ */

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();
 }