From e9ddc058f68509ad2cf71af07d1d41a7a213601a Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 15 Feb 2019 12:43:24 +0100
Subject: [PATCH] instantiation checker for mdps

---
 src/pars/model_instantiator.cpp | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp
index 6040230..e13c0a7 100644
--- a/src/pars/model_instantiator.cpp
+++ b/src/pars/model_instantiator.cpp
@@ -51,14 +51,24 @@ void define_model_instantiator(py::module& m) {
 
 void define_model_instantiation_checker(py::module& m) {
 
-    py::class_<SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>, std::shared_ptr<SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>>> bpdtmcinstchecker(m, "PDtmcInstantiationCheckerBase", "Instantiate pDTMCs to DTMCs (base)");
+    py::class_<SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>, std::shared_ptr<SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>>> bpdtmcinstchecker(m, "_PDtmcInstantiationCheckerBase", "Instantiate pDTMCs to DTMCs and immediately check (base)");
     bpdtmcinstchecker.def("specify_formula", &SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>::specifyFormula, "check_task"_a)
             ;
-    py::class_<SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>, std::shared_ptr<SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>>> (m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs", bpdtmcinstchecker)
+    py::class_<SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>, std::shared_ptr<SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>>> (m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs and immediately check", bpdtmcinstchecker)
 
         .def(py::init<Dtmc<storm::RationalFunction>>(), "parametric model"_a)
         .def("check", [](SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation<storm::RationalFunction> const& val) -> std::shared_ptr<CheckResult> {return sdimc.check(env,val);}, "env"_a, "instantiation"_a)
         .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>::setInstantiationsAreGraphPreserving, "value"_a);
+
+
+    py::class_<SparseInstantiationModelChecker<Mdp<storm::RationalFunction>, double>, std::shared_ptr<SparseInstantiationModelChecker<Mdp<storm::RationalFunction>, double>>> bpmdpinstchecker(m, "_PMdpInstantiationCheckerBase", "Instantiate pMDPs to MDPs and immediately check (base)");
+    bpmdpinstchecker.def("specify_formula", &SparseInstantiationModelChecker<Mdp<storm::RationalFunction>, double>::specifyFormula, "check_task"_a)
+            ;
+    py::class_<SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, double>, std::shared_ptr<SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, double>>> (m, "PMdpInstantiationChecker", "Instantiate PMDP to MDPs and immediately check", bpmdpinstchecker)
+
+            .def(py::init<Mdp<storm::RationalFunction>>(), "parametric model"_a)
+            .def("check", [](SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation<storm::RationalFunction> const& val) -> std::shared_ptr<CheckResult> {return sdimc.check(env,val);}, "env"_a, "instantiation"_a)
+            .def("set_graph_preserving", &SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, double>::setInstantiationsAreGraphPreserving, "value"_a);
 ;
 
 }
\ No newline at end of file