Bindings for InstantiationModelchecker with RationalNumber

src/core/result.cpp

@@ -43,6 +43,9 @@ void define_result(py::module& m) {
         .def("as_explicit_quantitative", [](storm::modelchecker::CheckResult const& result) {
                 return result.asExplicitQuantitativeCheckResult<double>();
             }, "Convert into explicit quantitative result")
+        .def("as_explicit_exact_quantitative", [](storm::modelchecker::CheckResult const& result) {
+                return result.asExplicitQuantitativeCheckResult<storm::RationalNumber>();
+            }, "Convert into explicit quantitative result")
         .def("as_explicit_parametric_quantitative", [](storm::modelchecker::CheckResult const& result) {
                 return result.asExplicitQuantitativeCheckResult<storm::RationalFunction>();
             }, "Convert into explicit quantitative result")
@@ -84,6 +87,19 @@ void define_result(py::module& m) {
         .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>::getExplicitValueVector, "Get model checking result values for all states")
     ;
 
+    py::class_<storm::modelchecker::QuantitativeCheckResult<storm::RationalNumber>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<storm::RationalNumber>>> exactQuantitativeCheckResult(m, "_ExactQuantitativeCheckResult", "Abstract class for exact quantitative model checking results", checkResult);
+    py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>, std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>>>(m, "ExplicitExactQuantitativeCheckResult", "Explicit exact quantitative model checking result", exactQuantitativeCheckResult)
+        .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber> const& result, storm::storage::sparse::state_type state) {
+            return result[state];
+        }, py::arg("state"), "Get result for given state")
+        .def("get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber> const& res) { return res.getValueVector();}, "Get model checking result values for all states")
+    ;
+    py::class_<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>, std::shared_ptr<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>>>(m, "SymbolicExactQuantitativeCheckResult", "Symbolic exact quantitative model checking result", quantitativeCheckResult)
+    ;
+    py::class_<storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>, std::shared_ptr<storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>>>(m, "HybridExactQuantitativeCheckResult", "Symbolic exact hybrid quantitative model checking result", quantitativeCheckResult)
+        .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalNumber>::getExplicitValueVector, "Get model checking result values for all states")
+    ;
+
     py::class_<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult);
     py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>, std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult)
         .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction> const& result, storm::storage::sparse::state_type state) {

src/pars/model_instantiator.cpp

@@ -42,33 +42,52 @@ void define_model_instantiator(py::module& m) {
 
     py::class_<storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>,Ctmc<double>>>(m, "PCtmcInstantiator", "Instantiate PCTMCs to CTMCs")
         .def(py::init<Ctmc<storm::RationalFunction>>(), "parametric model"_a)
-        .def("instantiate", &storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>, Ctmc<double>>::instantiate, "Instantiate model with given parameter values");
+        .def("instantiate", &storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>, Ctmc<double>>::instantiate, "Instantiate model with given parameter values")
+    ;
 
     py::class_<storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>,MarkovAutomaton<double>>>(m, "PMaInstantiator", "Instantiate PMAs to MAs")
         .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");
+        .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 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 and immediately check", bpdtmcinstchecker)
+    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 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);
+        .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, double>::setInstantiationsAreGraphPreserving, "value"_a)
+    ;
 
+    py::class_<SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, storm::RationalNumber>, std::shared_ptr<SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, storm::RationalNumber>>> bpdtmcexactinstchecker(m, "_PDtmcExactInstantiationCheckerBase", "Instantiate pDTMCs to exact DTMCs and immediately check (base)");
+    bpdtmcexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker<Dtmc<storm::RationalFunction>, storm::RationalNumber>::specifyFormula, "check_task"_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_<SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, storm::RationalNumber>, std::shared_ptr<SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, storm::RationalNumber>>> (m, "PDtmcExactInstantiationChecker", "Instantiate pDTMCs to exact DTMCs and immediately check", bpdtmcexactinstchecker)
+        .def(py::init<Dtmc<storm::RationalFunction>>(), "parametric model"_a)
+        .def("check", [](SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, storm::RationalNumber> &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>, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_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)
 
+
+    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);
+        .def("set_graph_preserving", &SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, double>::setInstantiationsAreGraphPreserving, "value"_a)
+    ;
+
+    py::class_<SparseInstantiationModelChecker<Mdp<storm::RationalFunction>, storm::RationalNumber>, std::shared_ptr<SparseInstantiationModelChecker<Mdp<storm::RationalFunction>, storm::RationalNumber>>> bpmdpexactinstchecker(m, "_PMdpExactInstantiationCheckerBase", "Instantiate pMDPs to exact MDPs and immediately check (base)");
+    bpmdpexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker<Mdp<storm::RationalFunction>, storm::RationalNumber>::specifyFormula, "check_task"_a);
+
+    py::class_<SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, storm::RationalNumber>, std::shared_ptr<SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, storm::RationalNumber>>> (m, "PMdpExactInstantiationChecker", "Instantiate PMDP to exact MDPs and immediately check", bpmdpexactinstchecker)
+        .def(py::init<Mdp<storm::RationalFunction>>(), "parametric model"_a)
+        .def("check", [](SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, storm::RationalNumber> &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>, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_a)
     ;
 
 }

tests/pars/test_model_instantiator.py

@@ -3,6 +3,7 @@ import stormpy.logic
 from helpers.helper import get_example_path
 
 from configurations import pars
+import math
 
 
 @pars
@@ -42,3 +43,39 @@ class TestModelInstantiator:
         point = {p: stormpy.RationalRF("0.5") for p in parameters}
         instantiated_model2 = instantiator.instantiate(point)
         assert "0.5" in str(instantiated_model2.transition_matrix[1])
+
+    def test_pdtmc_instantiation_checker(self):
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm"))
+        formulas = stormpy.parse_properties_for_prism_program("R=? [F \"stable\"]", program)
+        model = stormpy.build_parametric_model(program, formulas)
+
+        parameters = model.collect_probability_parameters()
+        inst_checker = stormpy.pars.PDtmcInstantiationChecker(model)
+        inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True))
+        inst_checker.set_graph_preserving(True)
+        env = stormpy.Environment()
+
+        point = {p: stormpy.RationalRF(1 / 2) for p in parameters}
+        result = inst_checker.check(env, point)
+        assert isinstance(result, stormpy.ExplicitQuantitativeCheckResult)
+        res = result.at(model.initial_states[0])
+        assert isinstance(res, float)
+        assert math.isclose(res, 29 / 15)
+
+    def test_pdtmc_exact_instantiation_checker(self):
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm"))
+        formulas = stormpy.parse_properties_for_prism_program("R=? [F \"stable\"]", program)
+        model = stormpy.build_parametric_model(program, formulas)
+
+        parameters = model.collect_probability_parameters()
+        inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(model)
+        inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True))
+        inst_checker.set_graph_preserving(True)
+        env = stormpy.Environment()
+
+        point = {p: stormpy.RationalRF("1/2") for p in parameters}
+        result = inst_checker.check(env, point)
+        assert isinstance(result, stormpy.ExplicitExactQuantitativeCheckResult)
+        res = result.at(model.initial_states[0])
+        assert isinstance(res, stormpy.Rational)
+        assert res == stormpy.Rational("29/15")