From 300902a5cd4e62e2f1114df350d505f1ebed0c48 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 3 Dec 2019 17:12:58 +0100 Subject: [PATCH] support for getting results for a particular state with symbolic model checking --- examples/analysis/02-analysis.py | 25 +++++++++++++++++++++++++ src/core/result.cpp | 13 ++++++++++--- src/storage/model.cpp | 6 ++++++ 3 files changed, 41 insertions(+), 3 deletions(-) diff --git a/examples/analysis/02-analysis.py b/examples/analysis/02-analysis.py index 4cee8d2..c744539 100644 --- a/examples/analysis/02-analysis.py +++ b/examples/analysis/02-analysis.py @@ -5,6 +5,8 @@ import stormpy.examples import stormpy.examples.files +from stormpy.storage import Expression + def example_analysis_02(): path = stormpy.examples.files.prism_dtmc_die prism_program = stormpy.parse_prism_program(path) @@ -18,5 +20,28 @@ def example_analysis_02(): assert result.min == result.max print(result.min) + + # Create an auxiliary mapping to build expressions that matches some state. + variables = dict() + for m in prism_program.modules: + for v in m.integer_variables: + variables[v.name] = v.expression_variable.get_expression() + expr_manager = prism_program.expression_manager + + expr_for_state_1 = Expression.And(Expression.Eq(variables["s"],expr_manager.create_integer(1)), + Expression.Eq(variables["d"],expr_manager.create_integer(0))) + expr_for_state_2 = Expression.And(Expression.Eq(variables["s"],expr_manager.create_integer(4)), + Expression.Eq(variables["d"],expr_manager.create_integer(0))) + + result = stormpy.model_checking(model, properties[0]) + cached_res = result.clone() + cached_res.filter(stormpy.create_filter_symbolic(model,expr_for_state_1)) + print(cached_res.min) + result.filter(stormpy.create_filter_symbolic(model,expr_for_state_2)) + assert result.min == result.max + print(result.min) + + + if __name__ == '__main__': example_analysis_02() \ No newline at end of file diff --git a/src/core/result.cpp b/src/core/result.cpp index 1209737..70babdc 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -18,6 +18,10 @@ std::shared_ptr createFilterInitial return std::make_unique>(model->getReachableStates(), model->getInitialStates()); } +template +std::shared_ptr createFilterSymbolic(std::shared_ptr> model, storm::expressions::Expression const& expr) { + return std::make_unique>(model->getReachableStates(), model->getStates(expr)); +} // Define python bindings void define_result(py::module& m) { @@ -82,7 +86,8 @@ void define_result(py::module& m) { .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) - ; + .def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult const& dd) {return dd.clone()->asSymbolicQuantitativeCheckResult(); }) + ; 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") ; @@ -95,7 +100,8 @@ void define_result(py::module& m) { .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) - ; + .def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult const& dd) {return dd.clone()->asSymbolicQuantitativeCheckResult(); }) + ; 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") ; @@ -108,12 +114,13 @@ void define_result(py::module& m) { .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) + .def("clone", [](storm::modelchecker::SymbolicQuantitativeCheckResult const& dd) {return dd.clone()->asSymbolicQuantitativeCheckResult(); }) ; 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") ; - + m.def("create_filter_symbolic", &createFilterSymbolic, "Creates a filter for the given states and a symbolic model", py::arg("model"), py::arg("states")); m.def("create_filter_initial_states_sparse", &createFilterInitialStatesSparse, "Create a filter for the initial states on a sparse model", py::arg("model")); m.def("create_filter_initial_states_symbolic", &createFilterInitialStatesSymbolic, "Create a filter for the initial states on a symbolic model", py::arg("model")); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index caa2d52..da572db 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -304,6 +304,9 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) { // Models with double numbers py::class_, std::shared_ptr>, ModelBase> model(m, ("_"+prefixClassName+"Model").c_str(), "A probabilistic model where transitions are represented by doubles and saved in a symbolic representation"); model.def_property_readonly("reward_models", [](SymbolicModel& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("reachable_states", &SymbolicModel::getReachableStates, "reachable states as DD") + .def_property_readonly("initial_states", &SymbolicModel::getInitialStates, "initial states as DD") + .def("get_states", [](SymbolicModel const& model, storm::expressions::Expression const& expr) {return model.getStates(expr);}, py::arg("expression"), "Get states that are described by the expression") .def("reduce_to_state_based_rewards", &SymbolicModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter()) ; @@ -331,6 +334,9 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) { py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, ("_"+prefixParametricClassName+"Model").c_str(), "A probabilistic model where transitions are represented by rational functions and saved in a symbolic representation"); modelRatFunc.def("get_parameters", &SymbolicModel::getParameters, "Get parameters") .def_property_readonly("reward_models", [](SymbolicModel const& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("reachable_states", &SymbolicModel::getReachableStates, "reachable states as DD") + .def_property_readonly("initial_states", &SymbolicModel::getInitialStates, "initial states as DD") + .def("get_states", [](SymbolicModel const& model, storm::expressions::Expression const& expr) {return model.getStates(expr);}, py::arg("expression"), "Get states that are described by the expression") .def("reduce_to_state_based_rewards", &SymbolicModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter("ParametricModel")) ;