add instantiation checker (for pDTMCs)

src/mod_pars.cpp

@@ -15,4 +15,5 @@ PYBIND11_MODULE(pars, m) {
     define_pars(m);
     define_pla(m);
     define_model_instantiator(m);
+    define_model_instantiation_checker(m);
 }

src/pars/model_instantiator.cpp

@@ -1,5 +1,24 @@
 #include "model_instantiator.h"
 #include "storm/models/sparse/Model.h"
+#include "storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+
+
+#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
+
+#include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/Multiplier.h"
+#include "storm/utility/vector.h"
+#include "storm/utility/graph.h"
+#include "storm/utility/NumberTraits.h"
 
 template<typename ValueType> using Model = storm::models::sparse::Model<ValueType>;
 template<typename ValueType> using Dtmc = storm::models::sparse::Dtmc<ValueType>;
@@ -7,6 +26,8 @@ template<typename ValueType> using Mdp = storm::models::sparse::Mdp<ValueType>;
 template<typename ValueType> using Ctmc = storm::models::sparse::Ctmc<ValueType>;
 template<typename ValueType> using MarkovAutomaton = storm::models::sparse::MarkovAutomaton<ValueType>;
 
+using namespace storm::modelchecker;
+
 // Model instantiator
 void define_model_instantiator(py::module& m) {
     py::class_<storm::utility::ModelInstantiator<Dtmc<storm::RationalFunction>, Dtmc<double>>>(m, "PDtmcInstantiator", "Instantiate PDTMCs to DTMCs")
@@ -27,3 +48,17 @@ void define_model_instantiator(py::module& m) {
         .def(py::init<MarkovAutomaton<storm::RationalFunction>>(), "parametric model"_a)
         .def("instantiate", &storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>, MarkovAutomaton<double>>::instantiate, "Instantiate model with given parameter values");
 }
+
+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)");
+    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)
+
+        .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);
+;
+
+}

src/pars/model_instantiator.h

@@ -4,5 +4,6 @@
 #include "common.h"
 
 void define_model_instantiator(py::module& m);
+void define_model_instantiation_checker(py::module& m);
 
 #endif /* PYTHON_PARS_MODEL_INSTANTIATOR_H_ */