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 py::class_(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_(m, "SymbolicModelDescription", "Symbolic description of model") + .def(py::init(), "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(); } 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(); }