Bindings for symbolic model building

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.

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<storm::models::sparse::Model<ValueType>> buildSparseModel(storm:
     }
 }
 
+// Thin wrapper for model building using symbolic representation
+template<storm::dd::DdType DdType, typename ValueType>
+std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+    if (formulas.empty()) {
+        // Build full model
+        return storm::api::buildSymbolicModel<DdType, ValueType>(modelDescription, formulas, true);
+    } else {
+        // Only build labels necessary for formulas
+        return storm::api::buildSymbolicModel<DdType, ValueType>(modelDescription, formulas, false);
+    }
+}
+
 void define_build(py::module& m) {
     // Build model
     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_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"));
     m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"));
     m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "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") = "");