From 299538b4e480204936280291eb91045f10c35e2e Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 12 Jan 2017 19:52:49 +0100
Subject: [PATCH] fixed mdp model instantiator, and added jani properties
 towards compatibility with current storm version

---
 src/core/core.cpp     | 4 ++--
 src/core/input.cpp    | 7 +++++++
 src/core/input.h      | 2 ++
 src/storage/model.cpp | 4 ++--
 4 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/core/core.cpp b/src/core/core.cpp
index 332aac5..4f9d672 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -11,8 +11,8 @@ 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::parseFormulasForPrismProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program"));
+    m.def("parse_properties", &storm::parsePropertiesForExplicit, "Parse explicit formulas", py::arg("formula_string"), py::arg("property_filter") = nullptr);
+    m.def("parse_properties_for_prism_program", &storm::parsePropertiesForPrismProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program"), py::arg("property_filter") = nullptr);
 
     // Pair <Model,Formulas>
     py::class_<storm::storage::ModelFormulasPair>(m, "ModelFormulasPair", "Pair of model and formulas")
diff --git a/src/core/input.cpp b/src/core/input.cpp
index 8c9f915..d83ee93 100644
--- a/src/core/input.cpp
+++ b/src/core/input.cpp
@@ -1,5 +1,12 @@
 #include "input.h"
 
+void define_property(py::module& m) {
+    py::class_<storm::jani::Property>(m, "Property", "Property")
+    .def_property_readonly("name", &storm::jani::Property::getName, "Obtain the name of the property")
+    .def_property_readonly("raw_formula", &storm::jani::Property::getRawFormula, "Obtain the formula directly");
+}
+
+
 // Define python bindings
 void define_input(py::module& m) {
 
diff --git a/src/core/input.h b/src/core/input.h
index 304dc9a..636b73a 100644
--- a/src/core/input.h
+++ b/src/core/input.h
@@ -3,6 +3,8 @@
 
 #include "common.h"
 
+void define_property(py::module& m);
 void define_input(py::module& m);
 
+
 #endif /* PYTHON_CORE_INPUT_H_ */
diff --git a/src/storage/model.cpp b/src/storage/model.cpp
index 791b6f4..79cd114 100644
--- a/src/storage/model.cpp
+++ b/src/storage/model.cpp
@@ -94,7 +94,7 @@ void define_model_instantiator(py::module& m) {
             .def(py::init<storm::models::sparse::Dtmc<storm::RationalFunction>>(), "parametric model"_a)
             .def("instantiate", &storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>>::instantiate, "Instantiate model with given parameter values");
 
-    py::class_<storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>,storm::models::sparse::Mdp<double>>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to MDPs")
+    py::class_<storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>,storm::models::sparse::Mdp<double>>>(m, "MdpInstantiator", "Instantiate PDTMCs to MDPs")
             .def(py::init<storm::models::sparse::Mdp<storm::RationalFunction>>(), "parametric model"_a)
     .def("instantiate", &storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>>::instantiate, "Instantiate model with given parameter values");
-}
\ No newline at end of file
+}