From 35fc0699ee4750ece45f6c8fdd5605863abb3f4a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 8 Nov 2019 11:18:38 +0100 Subject: [PATCH] Bindings for InstantiationModelchecker with RationalNumber --- src/core/result.cpp | 16 ++++++++++ src/pars/model_instantiator.cpp | 43 +++++++++++++++++++-------- tests/pars/test_model_instantiator.py | 37 +++++++++++++++++++++++ 3 files changed, 84 insertions(+), 12 deletions(-) diff --git a/src/core/result.cpp b/src/core/result.cpp index 9827950..1209737 100644 --- a/src/core/result.cpp +++ b/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(); }, "Convert into explicit quantitative result") + .def("as_explicit_exact_quantitative", [](storm::modelchecker::CheckResult const& result) { + return result.asExplicitQuantitativeCheckResult(); + }, "Convert into explicit quantitative result") .def("as_explicit_parametric_quantitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, "Convert into explicit quantitative result") @@ -84,6 +87,19 @@ void define_result(py::module& m) { .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") ; + py::class_, std::shared_ptr>> exactQuantitativeCheckResult(m, "_ExactQuantitativeCheckResult", "Abstract class for exact quantitative model checking results", checkResult); + py::class_, std::shared_ptr>>(m, "ExplicitExactQuantitativeCheckResult", "Explicit exact quantitative model checking result", exactQuantitativeCheckResult) + .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult 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 const& res) { return res.getValueVector();}, "Get model checking result values for all states") + ; + py::class_, std::shared_ptr>>(m, "SymbolicExactQuantitativeCheckResult", "Symbolic exact quantitative model checking result", quantitativeCheckResult) + ; + py::class_, std::shared_ptr>>(m, "HybridExactQuantitativeCheckResult", "Symbolic exact hybrid quantitative model checking result", quantitativeCheckResult) + .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") + ; + py::class_, std::shared_ptr>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult); py::class_, std::shared_ptr>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult) .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& result, storm::storage::sparse::state_type state) { diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp index e13c0a7..2886fdb 100644 --- a/src/pars/model_instantiator.cpp +++ b/src/pars/model_instantiator.cpp @@ -42,33 +42,52 @@ void define_model_instantiator(py::module& m) { py::class_,Ctmc>>(m, "PCtmcInstantiator", "Instantiate PCTMCs to CTMCs") .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, Ctmc>::instantiate, "Instantiate model with given parameter values"); + .def("instantiate", &storm::utility::ModelInstantiator, Ctmc>::instantiate, "Instantiate model with given parameter values") + ; py::class_,MarkovAutomaton>>(m, "PMaInstantiator", "Instantiate PMAs to MAs") .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, MarkovAutomaton>::instantiate, "Instantiate model with given parameter values"); + .def("instantiate", &storm::utility::ModelInstantiator, MarkovAutomaton>::instantiate, "Instantiate model with given parameter values") + ; } void define_model_instantiation_checker(py::module& m) { py::class_, double>, std::shared_ptr, double>>> bpdtmcinstchecker(m, "_PDtmcInstantiationCheckerBase", "Instantiate pDTMCs to DTMCs and immediately check (base)"); - bpdtmcinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a) - ; - py::class_, double>, std::shared_ptr, double>>> (m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs and immediately check", bpdtmcinstchecker) + bpdtmcinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a); + py::class_, double>, std::shared_ptr, double>>> (m, "PDtmcInstantiationChecker", "Instantiate pDTMCs to DTMCs and immediately check", bpdtmcinstchecker) .def(py::init>(), "parametric model"_a) .def("check", [](SparseDtmcInstantiationModelChecker, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) - .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a); + .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a) + ; + + py::class_, storm::RationalNumber>, std::shared_ptr, storm::RationalNumber>>> bpdtmcexactinstchecker(m, "_PDtmcExactInstantiationCheckerBase", "Instantiate pDTMCs to exact DTMCs and immediately check (base)"); + bpdtmcexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker, storm::RationalNumber>::specifyFormula, "check_task"_a); + + py::class_, storm::RationalNumber>, std::shared_ptr, storm::RationalNumber>>> (m, "PDtmcExactInstantiationChecker", "Instantiate pDTMCs to exact DTMCs and immediately check", bpdtmcexactinstchecker) + .def(py::init>(), "parametric model"_a) + .def("check", [](SparseDtmcInstantiationModelChecker, storm::RationalNumber> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) + .def("set_graph_preserving", &SparseDtmcInstantiationModelChecker, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_a) + ; py::class_, double>, std::shared_ptr, double>>> bpmdpinstchecker(m, "_PMdpInstantiationCheckerBase", "Instantiate pMDPs to MDPs and immediately check (base)"); - bpmdpinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a) - ; + bpmdpinstchecker.def("specify_formula", &SparseInstantiationModelChecker, double>::specifyFormula, "check_task"_a); + py::class_, double>, std::shared_ptr, double>>> (m, "PMdpInstantiationChecker", "Instantiate PMDP to MDPs and immediately check", bpmdpinstchecker) + .def(py::init>(), "parametric model"_a) + .def("check", [](SparseMdpInstantiationModelChecker, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) + .def("set_graph_preserving", &SparseMdpInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a) + ; - .def(py::init>(), "parametric model"_a) - .def("check", [](SparseMdpInstantiationModelChecker, double> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) - .def("set_graph_preserving", &SparseMdpInstantiationModelChecker, double>::setInstantiationsAreGraphPreserving, "value"_a); -; + py::class_, storm::RationalNumber>, std::shared_ptr, storm::RationalNumber>>> bpmdpexactinstchecker(m, "_PMdpExactInstantiationCheckerBase", "Instantiate pMDPs to exact MDPs and immediately check (base)"); + bpmdpexactinstchecker.def("specify_formula", &SparseInstantiationModelChecker, storm::RationalNumber>::specifyFormula, "check_task"_a); + + py::class_, storm::RationalNumber>, std::shared_ptr, storm::RationalNumber>>> (m, "PMdpExactInstantiationChecker", "Instantiate PMDP to exact MDPs and immediately check", bpmdpexactinstchecker) + .def(py::init>(), "parametric model"_a) + .def("check", [](SparseMdpInstantiationModelChecker, storm::RationalNumber> &sdimc, storm::Environment const& env, storm::utility::parametric::Valuation const& val) -> std::shared_ptr {return sdimc.check(env,val);}, "env"_a, "instantiation"_a) + .def("set_graph_preserving", &SparseMdpInstantiationModelChecker, storm::RationalNumber>::setInstantiationsAreGraphPreserving, "value"_a) + ; } \ No newline at end of file diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index cfad8a0..ac1bef4 100644 --- a/tests/pars/test_model_instantiator.py +++ b/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")