From f5a014ed5e082684d03a2a2a965f8e017a7d4eec Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 18 May 2018 11:53:40 +0200 Subject: [PATCH] Bindings for symbolic model building --- lib/stormpy/__init__.py | 71 +++++++++++++++++++++++++++++++++++++++++ src/core/core.cpp | 17 ++++++++++ 2 files changed, 88 insertions(+) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 0720ee3..161e459 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -56,6 +56,39 @@ def _convert_sparse_model(model, parametric=False): raise StormError("Not supported non-parametric model constructed") +def _convert_symbolic_model(model, parametric=False): + """ + Convert (parametric) model in symbolic representation into model corresponding to exact model type. + :param model: Symbolic model. + :param parametric: Flag indicating if the model is parametric. + :return: Model corresponding to exact model type. + """ + if parametric: + assert model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_symbolic_pdtmc() + elif model.model_type == ModelType.MDP: + return model._as_symbolic_pmdp() + elif model.model_type == ModelType.CTMC: + return model._as_symbolic_pctmc() + elif model.model_type == ModelType.MA: + return model._as_symbolic_pma() + else: + raise StormError("Not supported parametric model constructed") + else: + assert not model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_symbolic_dtmc() + elif model.model_type == ModelType.MDP: + return model._as_symbolic_mdp() + elif model.model_type == ModelType.CTMC: + return model._as_symbolic_ctmc() + elif model.model_type == ModelType.MA: + return model._as_symbolic_ma() + else: + raise StormError("Not supported non-parametric model constructed") + + def build_model(symbolic_description, properties=None): """ Build a model in sparse representation from a symbolic description. @@ -94,6 +127,44 @@ def build_parametric_model(symbolic_description, properties=None): return _convert_sparse_model(intermediate, parametric=True) +def build_symbolic_model(symbolic_description, properties=None): + """ + Build a model in symbolic 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 symbolic representation. + """ + if not symbolic_description.undefined_constants_are_graph_preserving: + raise StormError("Program still contains undefined constants") + + if properties: + formulae = [prop.raw_formula for prop in properties] + intermediate = core._build_symbolic_model_from_symbolic_description(symbolic_description, formulae) + else: + intermediate = core._build_symbolic_model_from_symbolic_description(symbolic_description) + return _convert_symbolic_model(intermediate, parametric=False) + + +def build_symbolic_parametric_model(symbolic_description, properties=None): + """ + Build a parametric model in symbolic 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 symbolic representation. + """ + if not symbolic_description.undefined_constants_are_graph_preserving: + raise StormError("Program still contains undefined constants") + + if properties: + formulae = [prop.raw_formula for prop in properties] + intermediate = core._build_symbolic_parametric_model_from_symbolic_description(symbolic_description, formulae) + else: + intermediate = core._build_symbolic_parametric_model_from_symbolic_description(symbolic_description) + return _convert_symbolic_model(intermediate, parametric=True) + + def build_model_from_drn(file): """ Build a model in sparse representation from the explicit DRN representation. diff --git a/src/core/core.cpp b/src/core/core.cpp index e0e4af4..eafd9bd 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -2,7 +2,10 @@ #include "storm/utility/initialize.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/storage/ModelFormulasPair.h" +#include "storm/storage/dd/DdType.h" #include "storm/solver/OptimizationDirection.h" +#include "storm/models/symbolic/StandardRewardModel.h" + void define_core(py::module& m) { // Init @@ -59,10 +62,24 @@ std::shared_ptr> buildSparseModel(storm: } } +// Thin wrapper for model building using symbolic representation +template +std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas) { + if (formulas.empty()) { + // Build full model + return storm::api::buildSymbolicModel(modelDescription, formulas, true); + } else { + // Only build labels necessary for formulas + return storm::api::buildSymbolicModel(modelDescription, formulas, false); + } +} + void define_build(py::module& m) { // Build model 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_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")); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");