building models with valuations

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()

src/core/core.cpp

@@ -98,6 +98,7 @@ void define_build(py::module& m) {
     m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
     m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
     m.def("build_sparse_model_with_options", &buildSparseModelWithOptions<double>, "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<storm::RationalFunction>, "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<storm::dd::DdType::Sylvan, double>, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"));
@@ -109,6 +110,7 @@ void define_build(py::module& m) {
             .def(py::init<std::vector<std::shared_ptr<storm::logic::Formula const>> const&>(), "Initialise with formulae to preserve", py::arg("formulae"))
             .def(py::init<bool, bool>(), "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);

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<storm::dd::DdType::Sylvan>(m, "Sylvan");

src/storage/model.cpp

@@ -193,6 +193,8 @@ void define_sparse_model(py::module& m) {
         .def_property_readonly("reward_models", [](SparseModel<double>& model) {return model.getRewardModels(); }, "Reward models")
         .def_property_readonly("transition_matrix", &getTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
         .def_property_readonly("backward_transition_matrix", &SparseModel<double>::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix")
+        .def("has_state_valuations", [](SparseModel<double> const& model) {return model.hasStateValuations();}, "has state valuation?")
+        .def_property_readonly("state_valuations",  [](SparseModel<double> const& model) {return model.getStateValuations();}, "state valuations")
         .def("reduce_to_state_based_rewards", &SparseModel<double>::reduceToStateBasedRewards)
         .def("__str__", getModelInfoPrinter<double>())
         .def("to_dot", [](SparseModel<double>& 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<RationalFunction> const& model) {return model.getRewardModels(); }, "Reward models")
         .def_property_readonly("transition_matrix", &getTransitionMatrix<RationalFunction>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
         .def_property_readonly("backward_transition_matrix", &SparseModel<RationalFunction>::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix")
+        .def("has_state_valuations", [](SparseModel<RationalFunction> const& model) {return model.hasStateValuations();}, "has state valuation?")
+        .def_property_readonly("state_valuations",  [](SparseModel<RationalFunction> const& model) {return model.getStateValuations();}, "state valuations")
         .def("reduce_to_state_based_rewards", &SparseModel<RationalFunction>::reduceToStateBasedRewards)
         .def("__str__", getModelInfoPrinter<RationalFunction>("ParametricModel"))
         .def("to_dot", [](SparseModel<RationalFunction>& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string")

src/storage/prism.cpp

@@ -79,6 +79,7 @@ void define_prism(py::module& m) {
     py::class_<Variable, std::shared_ptr<Variable>> 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_<IntegerVariable, std::shared_ptr<IntegerVariable>> integer_variable(m, "Prism_Integer_Variable", variable, "A program integer variable in a Prism program");

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_<storm::storage::sparse::StateValuations, std::shared_ptr<storm::storage::sparse::StateValuations>> statevaluation(m,"StateValuation", "Valuations for explicit states");
+    statevaluation.def("get_state", &storm::storage::sparse::StateValuations::getStateValuation)
+            ;
+
+}
+
+void define_simplevaluation(py::module& m) {
+    py::class_<storm::expressions::SimpleValuation, std::shared_ptr<storm::expressions::SimpleValuation>> 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);
+}

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);