Move core module to generic template bindings

examples/building_models/04-building-models.py

@@ -37,7 +37,7 @@ def permissive_policy(state_valuation, action_index):
         cond3 = json.loads(str(state_valuation.to_json()))["x1"] < 40
         return cond1 or (cond2 and cond3)
 
-    constructor = stormpy.make_sparse_model_builder(prism_program, options, stormpy.StateValuationFunctionActionMaskDouble(permissive_policy))
+    constructor = stormpy.make_sparse_model_builder(prism_program, options, stormpy.StateValuationFunctionActionMask[float](permissive_policy))
     model = constructor.build()
     print(model)
 

lib/stormpy/simulator.py

@@ -105,10 +105,7 @@ class SparseSimulator(Simulator):
     def __init__(self, model, seed=None):
         super().__init__(seed)
         self._model = model
-        if self._model.is_exact:
-            self._engine = stormpy._core._DiscreteTimeSparseModelSimulatorExact(model)
-        else:
-            self._engine = stormpy._core._DiscreteTimeSparseModelSimulatorDouble(model)
+        self._engine = stormpy.DiscreteTimeSparseModelSimulator(model)
         if seed is not None:
             self._engine.set_seed(seed)
         self._state_valuations = None
@@ -234,7 +231,7 @@ def __init__(self, program, seed=None, options=stormpy.BuilderOptions()):
         super().__init__(seed)
         self._program = program
         # TODO support exact arithmetic here
-        self._engine = stormpy._core._DiscreteTimePrismProgramSimulatorDouble(program, options)
+        self._engine = stormpy.DiscreteTimePrismProgramSimulator[float](program, options)
         if seed is not None:
             self._engine.set_seed(seed)
         self.set_full_observability(self._program.model_type != stormpy.storage.PrismModelType.POMDP)

lib/stormpy/storage/__init__.py

@@ -55,45 +55,50 @@
     deduce=_deduce_from_object(SparseMatrix.parameters_of, keyword="transition_matrix", default=(float,)),
 )
 
+
 # src/storage/model.cpp
-_model_parameters = lambda source: SparseMatrix.parameters_of(source.transition_matrix)
+def parameters_of_model(model):
+    """Return the value-type parameter of a sparse model or model components."""
+
+    return SparseMatrix.parameters_of(model.transition_matrix)
+
 
 SparseModel = TemplateClass("stormpy.storage.SparseModel", _storage, parameters=("ValueType",), deduce=_deduce_default(float))
 SparseDtmc = TemplateClass(
     "stormpy.storage.SparseDtmc",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")),
+    deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")),
 )
 SparseMdp = TemplateClass(
     "stormpy.storage.SparseMdp",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")),
+    deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")),
 )
 SparsePomdp = TemplateClass(
     "stormpy.storage.SparsePomdp",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")),
+    deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")),
 )
 SparseCtmc = TemplateClass(
     "stormpy.storage.SparseCtmc",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")),
+    deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")),
 )
 SparseMA = TemplateClass(
     "stormpy.storage.SparseMA",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")),
+    deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")),
 )
 SparseSmg = TemplateClass(
     "stormpy.storage.SparseSmg",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword=("components", "other_model")),
+    deduce=_deduce_from_object(parameters_of_model, keyword=("components", "other_model")),
 )
 SparseRewardModel = TemplateClass("stormpy.storage.SparseRewardModel", _storage, parameters=("ValueType",), deduce=_deduce_default(float))
 SymbolicModel = TemplateClass("stormpy.storage.SymbolicModel", _storage, parameters=(_TemplateParameter("DdType", kind="value"), "ValueType"))
@@ -108,15 +113,15 @@
     "stormpy.storage.MaximalEndComponentDecomposition",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword="model"),
+    deduce=_deduce_from_object(parameters_of_model, keyword="model"),
 )
 
 # src/storage/memorystructure.cpp
 MemoryStructureBuilder = TemplateClass(
     "stormpy.storage.MemoryStructureBuilder",
     _storage,
     parameters=("ValueType",),
-    deduce=_deduce_from_object(_model_parameters, keyword="model", position=1),
+    deduce=_deduce_from_object(parameters_of_model, keyword="model", position=1),
 )
 MemoryStructureProduct = TemplateClass("stormpy.storage.MemoryStructureProduct", _storage, parameters=("ValueType",), deduce=_deduce_default(float))
 

src/core/analysis.cpp

@@ -2,10 +2,13 @@
 
 #include <storm/analysis/GraphConditions.h>
 
+#include "src/binding_type_index.h"
+
 // Define python bindings
 void define_graph_constraints(py::module& m) {
     // ConstraintCollector
-    py::classh<storm::analysis::ConstraintCollector<storm::RationalFunction>>(m, "ConstraintCollector", "Collector for constraints on parametric Markov chains")
+    stormpy::bindings::bindTemplateClass<storm::analysis::ConstraintCollector<storm::RationalFunction>>(
+        m, "ConstraintCollector", stormpy::bindings::typeIndex<storm::RationalFunction>(), "Collector for constraints on parametric Markov chains")
         .def(py::init<storm::models::sparse::Model<storm::RationalFunction> const&>(), py::arg("model"))
         .def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getWellformedConstraints,
                                "Get the constraints ensuring a wellformed model")

src/core/bisimulation.cpp

@@ -17,11 +17,11 @@ void define_bisimulation(py::module& m) {
     // Bisimulation
     m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization<double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"),
           py::arg("bisimulation_type"), py::arg("graph_preserving"), py::arg("tolerance"));
-    m.def("_perform_parametric_bisimulation", &storm::api::performBisimulationMinimization<storm::RationalFunction>, "Perform bisimulation on parametric model",
+    m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization<storm::RationalFunction>, "Perform bisimulation on parametric model",
           py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("graph_preserving"), py::arg("tolerance"));
     m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, double>, "Perform bisimulation", py::arg("model"),
           py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"), py::arg("bisimulation_options"));
-    m.def("_perform_symbolic_parametric_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, storm::RationalFunction>,
+    m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, storm::RationalFunction>,
           "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"),
           py::arg("bisimulation_options"));
 

src/core/core.cpp

@@ -15,6 +15,8 @@
 #include <storm/utility/SignalHandler.h>
 #include <storm/utility/initialize.h>
 
+#include "src/binding_type_index.h"
+
 void define_core(py::module& m) {
     // Init
     m.def(
@@ -103,30 +105,35 @@ std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> buildSymbolic
     }
 }
 
+template<typename ValueType>
+void define_explicit_model_builder(py::module& m, std::string const& name) {
+    m.def(name.c_str(), &storm::api::makeExplicitModelBuilder<ValueType>, "Construct a builder instance", py::arg("model_description"), py::arg("options"),
+          py::arg("action_mask") = nullptr, py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
+
+    stormpy::bindings::bindTemplateClass<storm::builder::ExplicitModelBuilder<ValueType>>(m, "ExplicitModelBuilder", stormpy::bindings::typeIndex<ValueType>(),
+                                                                                          "Model builder for sparse models")
+        .def("build", &storm::builder::ExplicitModelBuilder<ValueType>::build, "Build the model", py::call_guard<py::gil_scoped_release>())
+        .def("export_lookup", &storm::builder::ExplicitModelBuilder<ValueType>::exportExplicitStateLookup, "Export a lookup model");
+}
+
 template<typename ValueType>
 void define_build_sparse_model_defs(py::module& m) {
     std::string type;
-    std::string classType;
     std::string desc;
     if constexpr (std::is_same_v<ValueType, double>) {
         type = "";
-        classType = "";
         desc = "";
     } else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
         type = "exact_";
-        classType = "Exact";
         desc = "";
     } else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
         type = "parametric_";
-        classType = "Parametric";
         desc = "parametric ";
     } else if constexpr (std::is_same_v<ValueType, storm::Interval>) {
         type = "interval_";
-        classType = "Interval";
         desc = "interval ";
     } else if constexpr (std::is_same_v<ValueType, storm::RationalInterval>) {
         type = "exact_interval_";
-        classType = "ExactInterval";
         desc = "exact interval ";
     }
 
@@ -144,8 +151,8 @@ void define_build_sparse_model_defs(py::module& m) {
           ("Build the " + desc + "model from DRN" + (std::is_same_v<ValueType, storm::RationalFunction> ? " (parametric)" : "")).c_str(), py::arg("file"),
           py::arg("options") = storm::parser::DirectEncodingParserOptions());
 
-    py::classh<typename storm::builder::ExplicitModelBuilder<ValueType>::Options>(m, ("Explicit" + classType + "ModelBuilderOptions").c_str(),
-                                                                                  "Options for the explicit model builder")
+    stormpy::bindings::bindTemplateClass<typename storm::builder::ExplicitModelBuilder<ValueType>::Options>(
+        m, "ExplicitModelBuilderOptions", stormpy::bindings::typeIndex<ValueType>(), "Options for the explicit model builder")
         .def(py::init<>(), "Create")
         .def_readwrite("exploration_order", &storm::builder::ExplicitModelBuilder<ValueType>::Options::explorationOrder,
                        "The order in which to explore the model")
@@ -154,33 +161,18 @@ void define_build_sparse_model_defs(py::module& m) {
         .def_readwrite("exploration_state_limit", &storm::builder::ExplicitModelBuilder<ValueType>::Options::explorationStateLimit,
                        "If set, no further states will be explored once the given number is exceeded.");
 
-    if constexpr (std::is_same_v<ValueType, double>) {
-        m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, double>,
-              "Build the model in symbolic representation", py::arg("model_description"),
+    define_explicit_model_builder<ValueType>(m, "make_sparse_model_builder" + type);
+
+    if constexpr (!storm::IsIntervalType<ValueType>) {
+        m.def(("_build_symbolic_" + type + "model_from_symbolic_description").c_str(), &buildSymbolicModel<storm::dd::DdType::Sylvan, ValueType>,
+              ("Build the " + desc + "model in symbolic representation").c_str(), py::arg("model_description"),
               py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("environment"));
+    }
+
+    if constexpr (std::is_same_v<ValueType, double>) {
         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") = "", py::arg("options") = storm::parser::ExplicitModelParserOptions());
-        m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"),
-              py::arg("options"), py::arg("action_mask") = nullptr,
-              py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
-        py::classh<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder", "Model builder for sparse models")
-            .def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model", py::call_guard<py::gil_scoped_release>())
-            .def("export_lookup", &storm::builder::ExplicitModelBuilder<double>::exportExplicitStateLookup, "Export a lookup model");
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
-        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>>(), py::arg("environment"));
-        m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<storm::RationalFunction>, "Construct a builder instance",
-              py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr,
-              py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
-        py::classh<storm::builder::ExplicitModelBuilder<storm::RationalFunction>>(m, "ExplicitParametricModelBuilder", "Model builder for sparse models")
-            .def("build", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::build, "Build the model", py::call_guard<py::gil_scoped_release>())
-            .def("export_lookup", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::exportExplicitStateLookup, "Export a lookup model");
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
-        m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder<storm::RationalNumber>, "Construct a builder instance",
-              py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr,
-              py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
     }
 }
 
@@ -242,9 +234,11 @@ void define_build(py::module& m) {
         .def("set_build_all_reward_models", &storm::builder::BuilderOptions::setBuildAllRewardModels, "Build with all reward models",
              py::arg("new_value") = true);
 
-    py::classh<storm::generator::ActionMask<double>> actionmask(m, "ActionMaskDouble");
-    py::classh<storm::generator::StateValuationFunctionMask<double>> actfuncmask(m, "StateValuationFunctionActionMaskDouble", actionmask);
-    actfuncmask.def(py::init<std::function<bool(storm::expressions::SimpleValuation const&, uint64_t)>>(), py::arg("f"));
+    auto actionmask =
+        stormpy::bindings::bindTemplateClass<storm::generator::ActionMask<double>>(m, "ActionMask", stormpy::bindings::typeIndex<double>(), "Mask for actions");
+    stormpy::bindings::bindTemplateClass<storm::generator::StateValuationFunctionMask<double>>(
+        m, "StateValuationFunctionActionMask", stormpy::bindings::typeIndex<double>(), "Action mask based on state valuations", actionmask)
+        .def(py::init<std::function<bool(storm::expressions::SimpleValuation const&, uint64_t)>>(), py::arg("f"));
 }
 
 void define_optimality_type(py::module& m) {
@@ -270,28 +264,8 @@ void exportDRN(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, s
 
 template<typename ValueType>
 void define_export_drn(py::module& m) {
-    std::string prefix;
-    std::string suffix;
-    if constexpr (std::is_same_v<ValueType, double>) {
-        prefix = "";
-        suffix = "";
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
-        prefix = "_exact";
-        suffix = "";
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
-        prefix = "_parametric";
-        suffix = "";
-    } else if constexpr (std::is_same_v<ValueType, storm::Interval>) {
-        prefix = "";
-        suffix = "_interval";
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalInterval>) {
-        prefix = "_exact";
-        suffix = "_interval";
-    }
-
-    m.def(("_export" + prefix + "_to_drn" + suffix).c_str(), &exportDRN<ValueType>,
-          ("Export " + (std::is_same_v<ValueType, storm::RationalFunction> ? std::string("parametric ") : std::string()) + "model in DRN format").c_str(),
-          py::arg("model"), py::arg("file"), py::arg("options") = storm::io::DirectEncodingExporterOptions());
+    m.def("_export_to_drn", &exportDRN<ValueType>, "Export model in DRN format", py::arg("model"), py::arg("file"),
+          py::arg("options") = storm::io::DirectEncodingExporterOptions());
 }
 
 void define_export(py::module& m) {