From 62f3d3630ed07d2843d5439e7cf8fe7e7be34961 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 15:02:13 +0200 Subject: [PATCH] Bindings for dd and hybrid model checking --- lib/stormpy/__init__.py | 82 +++++++++++++++++++++++++++++++- src/core/modelchecking.cpp | 22 +++++++-- src/core/result.cpp | 28 +++++++---- tests/core/test_modelchecking.py | 21 ++++++++ tests/pars/test_parametric.py | 28 ++++++++++- 5 files changed, 168 insertions(+), 13 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 161e459..1424892 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -93,6 +93,28 @@ def build_model(symbolic_description, properties=None): """ Build a model in sparse representation from a symbolic description. + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Model in sparse representation. + """ + return build_sparse_model(symbolic_description, properties=properties) + + +def build_parametric_model(symbolic_description, properties=None): + """ + Build a parametric model in sparse representation from a symbolic description. + + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Parametric model in sparse representation. + """ + return build_sparse_parametric_model(symbolic_description, properties=properties) + + +def build_sparse_model(symbolic_description, properties=None): + """ + Build a model in sparse representation from a symbolic description. + :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Model in sparse representation. @@ -108,7 +130,7 @@ def build_model(symbolic_description, properties=None): return _convert_sparse_model(intermediate, parametric=False) -def build_parametric_model(symbolic_description, properties=None): +def build_sparse_parametric_model(symbolic_description, properties=None): """ Build a parametric model in sparse representation from a symbolic description. @@ -203,6 +225,20 @@ def perform_bisimulation(model, properties, bisimulation_type): def model_checking(model, property, only_initial_states=False, extract_scheduler=False): + """ + Perform model checking on model for property. + :param model: Model. + :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. + :param extract_scheduler: If True, try to extract a scheduler + :return: Model checking result. + :rtype: CheckResult + """ + return check_model_sparse(model, property, only_initial_states=only_initial_states, + extract_scheduler=extract_scheduler) + + +def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False): """ Perform model checking on model for property. :param model: Model. @@ -227,6 +263,50 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler return core._model_checking_sparse_engine(model, task) +def check_model_dd(model, property, only_initial_states=False): + """ + Perform model checking using dd engine. + :param model: Model. + :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. + :return: Model checking result. + :rtype: CheckResult + """ + if isinstance(property, Property): + formula = property.raw_formula + else: + formula = property + + if model.supports_parameters: + task = core.ParametricCheckTask(formula, only_initial_states) + return core._parametric_model_checking_dd_engine(model, task) + else: + task = core.CheckTask(formula, only_initial_states) + return core._model_checking_dd_engine(model, task) + + +def check_model_hybrid(model, property, only_initial_states=False): + """ + Perform model checking using hybrid engine. + :param model: Model. + :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. + :return: Model checking result. + :rtype: CheckResult + """ + if isinstance(property, Property): + formula = property.raw_formula + else: + formula = property + + if model.supports_parameters: + task = core.ParametricCheckTask(formula, only_initial_states) + return core._parametric_model_checking_hybrid_engine(model, task) + else: + task = core.CheckTask(formula, only_initial_states) + return core._model_checking_hybrid_engine(model, task) + + def prob01min_states(model, eventually_formula): assert type(eventually_formula) == logic.EventuallyFormula labelform = eventually_formula.subformula diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 703e53c..1084a12 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -4,12 +4,24 @@ template using CheckTask = storm::modelchecker::CheckTask; -// Thin wrapper for model checking +// Thin wrapper for model checking using sparse engine template std::shared_ptr modelCheckingSparseEngine(std::shared_ptr> model, CheckTask const& task) { return storm::api::verifyWithSparseEngine(model, task); } +// Thin wrapper for model checking using dd engine +template +std::shared_ptr modelCheckingDdEngine(std::shared_ptr> model, CheckTask const& task) { + return storm::api::verifyWithDdEngine(model, task); +} + +// Thin wrapper for model checking using hybrid engine +template +std::shared_ptr modelCheckingHybridEngine(std::shared_ptr> model, CheckTask const& task) { + return storm::api::verifyWithHybridEngine(model, task); +} + // Thin wrapper for computing prob01 states template std::pair computeProb01(storm::models::sparse::Dtmc const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { @@ -42,8 +54,12 @@ void define_modelchecking(py::module& m) { ; // Model checking - m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking", py::arg("model"), py::arg("task")); - m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking", py::arg("model"), py::arg("task")); + m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task")); + m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task")); + m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", py::arg("model"), py::arg("task")); + m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task")); + m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task")); + m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task")); m.def("_compute_prob01states_double", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_rationalfunc", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_min_double", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); diff --git a/src/core/result.cpp b/src/core/result.cpp index b564e3c..9025c63 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -1,11 +1,9 @@ #include "result.h" #include "storm/analysis/GraphConditions.h" - -// Thin wrapper -template -std::vector getValues(storm::modelchecker::ExplicitQuantitativeCheckResult const& result) { - return result.getValueVector(); -} +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "storm/models/symbolic/StandardRewardModel.h" // Define python bindings void define_result(py::module& m) { @@ -49,6 +47,8 @@ void define_result(py::module& m) { }, py::arg("state"), "Get result for given state") .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") ; + py::class_, std::shared_ptr>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) + ; // QuantitativeCheckResult py::class_, std::shared_ptr>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult); @@ -56,15 +56,27 @@ void define_result(py::module& m) { .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", &getValues, "Get model checking result values for all states") + .def("get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getValueVector();}, "Get model checking result values for all states") .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getScheduler();}, "get scheduler") ; + py::class_, std::shared_ptr>>(m, "SymbolicQuantitativeCheckResult", "Symbolic quantitative model checking result", quantitativeCheckResult) + ; + py::class_, std::shared_ptr>>(m, "HybridQuantitativeCheckResult", "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) { return result[state]; }, py::arg("state"), "Get result for given state") - .def("get_values", &getValues, "Get model checking result values for all states") + .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, "SymbolicParametricQuantitativeCheckResult", "Symbolic parametric quantitative model checking result", quantitativeCheckResult) ; + py::class_, std::shared_ptr>>(m, "HybridParametricQuantitativeCheckResult", "Symbolic parametric hybrid quantitative model checking result", quantitativeCheckResult) + .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") + ; + } diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 89cce9e..c8687bc 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -127,3 +127,24 @@ class TestModelChecking: assert initial_state == 1 result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 4.166666667) + + def test_model_checking_prism_dd_dtmc(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_symbolic_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + result = stormpy.check_model_dd(model, formulas[0]) + assert type(result) is stormpy.SymbolicQuantitativeCheckResult + + def test_model_checking_prism_hybrid_dtmc(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_symbolic_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + result = stormpy.check_model_hybrid(model, formulas[0]) + assert type(result) is stormpy.HybridQuantitativeCheckResult + values = result.get_values() + assert len(values) == 3 + assert math.isclose(values[0], 0.16666666666666663) diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 71944e4..677a6ff 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -8,7 +8,7 @@ from configurations import pars @pars class TestParametric: - def test_parametric_state_elimination(self): + def test_parametric_model_checking_sparse(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) prop = "P=? [F s=5]" formulas = stormpy.parse_properties_for_prism_program(prop, program) @@ -24,6 +24,32 @@ class TestParametric: one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) assert func.denominator == one + def test_parametric_model_checking_dd(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + prop = "P=? [F s=5]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_symbolic_parametric_model(program, formulas) + assert model.nr_states == 11 + assert model.nr_transitions == 17 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + result = stormpy.check_model_dd(model, formulas[0]) + assert type(result) is stormpy.SymbolicParametricQuantitativeCheckResult + + def test_parametric_model_checking_hybrid(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + prop = "P=? [F s=5]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_symbolic_parametric_model(program, formulas) + assert model.nr_states == 11 + assert model.nr_transitions == 17 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + result = stormpy.check_model_hybrid(model, formulas[0]) + assert type(result) is stormpy.HybridParametricQuantitativeCheckResult + values = result.get_values() + assert len(values) == 3 + def test_constraints_collector(self): from pycarl.formula import FormulaType, Relation if stormpy.info.storm_ratfunc_use_cln():