From 76870b61be451c2f9e953c12cb58c6f404d64dfd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 3 Oct 2019 14:21:47 +0200 Subject: [PATCH] building models with valuations --- .../building_models/03-building-models.py | 30 +++++++++++++++++++ src/core/core.cpp | 2 ++ src/mod_storage.cpp | 3 ++ src/storage/model.cpp | 4 +++ src/storage/prism.cpp | 1 + src/storage/valuation.cpp | 21 +++++++++++++ src/storage/valuation.h | 6 ++++ 7 files changed, 67 insertions(+) create mode 100644 examples/building_models/03-building-models.py create mode 100644 src/storage/valuation.cpp create mode 100644 src/storage/valuation.h diff --git a/examples/building_models/03-building-models.py b/examples/building_models/03-building-models.py new file mode 100644 index 0000000..0068c34 --- /dev/null +++ b/examples/building_models/03-building-models.py @@ -0,0 +1,30 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_building_models_01(): + path = stormpy.examples.files.prism_pdtmc_brp + prism_program = stormpy.parse_prism_program(path) + formula_str = "P=? [F s=5]" + properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + model = stormpy.build_sparse_parametric_model_with_options(prism_program, options) + eval2 = model.state_valuations.get_state(2) + integer_variables = [] + boolean_variables = [] + for module in prism_program.modules: + print("module {}".format(module.name)) + integer_variables += module.integer_variables + boolean_variables += module.boolean_variables + + print(",".join(["{}: {}".format(str(iv.name), eval2.get_integer_value(iv.expression_variable)) for iv in integer_variables])) + + + +if __name__ == '__main__': + example_building_models_01() diff --git a/src/core/core.cpp b/src/core/core.cpp index e9d074e..67a0c24 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -98,6 +98,7 @@ void define_build(py::module& m) { m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("build_sparse_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); @@ -109,6 +110,7 @@ void define_build(py::module& m) { .def(py::init> const&>(), "Initialise with formulae to preserve", py::arg("formulae")) .def(py::init(), "Initialise without formulae", py::arg("build_all_reward_models"), py::arg("build_all_labels")) .def_property_readonly("preserved_label_names", &storm::builder::BuilderOptions::getLabelNames, "Labels preserved") + .def("set_build_state_valuations", &storm::builder::BuilderOptions::setBuildStateValuations, "Build state valuations", py::arg("new_value")=true) .def("set_build_with_choice_origins", &storm::builder::BuilderOptions::setBuildChoiceOrigins, "Build choice origins", py::arg("new_value")=true) .def("set_add_out_of_bounds_state", &storm::builder::BuilderOptions::setAddOutOfBoundsState, "Build with out of bounds state", py::arg("new_value")=true) .def("set_add_overlapping_guards_label", &storm::builder::BuilderOptions::setAddOverlappingGuardsLabel, "Build with overlapping guards state labeled", py::arg("new_value")=true); diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 997d037..4bdca9c 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -8,6 +8,7 @@ #include "storage/prism.h" #include "storage/jani.h" #include "storage/state.h" +#include "src/storage/valuation.h" #include "storage/choiceorigins.h" #include "storage/labeling.h" #include "storage/expressions.h" @@ -24,6 +25,8 @@ PYBIND11_MODULE(storage, m) { define_bitvector(m); define_model(m); + define_statevaluation(m); + define_simplevaluation(m); define_sparse_model(m); define_sparse_matrix(m); define_symbolic_model(m, "Sylvan"); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 441b434..5864f80 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -193,6 +193,8 @@ void define_sparse_model(py::module& m) { .def_property_readonly("reward_models", [](SparseModel& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &SparseModel::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def("has_state_valuations", [](SparseModel const& model) {return model.hasStateValuations();}, "has state valuation?") + .def_property_readonly("state_valuations", [](SparseModel const& model) {return model.getStateValuations();}, "state valuations") .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter()) .def("to_dot", [](SparseModel& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string") @@ -250,6 +252,8 @@ void define_sparse_model(py::module& m) { .def_property_readonly("reward_models", [](SparseModel const& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &SparseModel::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def("has_state_valuations", [](SparseModel const& model) {return model.hasStateValuations();}, "has state valuation?") + .def_property_readonly("state_valuations", [](SparseModel const& model) {return model.getStateValuations();}, "state valuations") .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter("ParametricModel")) .def("to_dot", [](SparseModel& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string") diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 6eb7c78..e7d4ca9 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -79,6 +79,7 @@ void define_prism(py::module& m) { py::class_> variable(m, "Prism_Variable", "A program variable in a Prism program"); variable.def_property_readonly("name", &Variable::getName, "Variable Name") .def_property_readonly("initial_value_expression", &Variable::getInitialValueExpression, "The expression represented the initial value of the variable") + .def_property_readonly("expression_variable", &Variable::getExpressionVariable, "The expression variable corresponding to the variable") ; py::class_> integer_variable(m, "Prism_Integer_Variable", variable, "A program integer variable in a Prism program"); diff --git a/src/storage/valuation.cpp b/src/storage/valuation.cpp new file mode 100644 index 0000000..36c9699 --- /dev/null +++ b/src/storage/valuation.cpp @@ -0,0 +1,21 @@ +#include "valuation.h" +#include "src/helpers.h" + +#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/expressions/SimpleValuation.h" +#include "storm/storage/expressions/Variable.h" + +// Define python bindings +void define_statevaluation(py::module& m) { + + py::class_> statevaluation(m,"StateValuation", "Valuations for explicit states"); + statevaluation.def("get_state", &storm::storage::sparse::StateValuations::getStateValuation) + ; + +} + +void define_simplevaluation(py::module& m) { + py::class_> simplevaluation(m, "SimpleValuation", "Valuations for storm variables"); + simplevaluation.def("get_boolean_value", &storm::expressions::SimpleValuation::getBooleanValue); + simplevaluation.def("get_integer_value", &storm::expressions::SimpleValuation::getIntegerValue); +} \ No newline at end of file diff --git a/src/storage/valuation.h b/src/storage/valuation.h new file mode 100644 index 0000000..0a59597 --- /dev/null +++ b/src/storage/valuation.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +void define_statevaluation(py::module& m); +void define_simplevaluation(py::module& m); \ No newline at end of file