From 6c8815d29fa4a63681052b7e7a6a558b4b287ca5 Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Tue, 25 Aug 2026 14:50:28 +0200
Subject: [PATCH] Migrate dft and pars to experimental new generic handling

---
 doc/source/doc/parametric_models.ipynb        |   2 +-
 examples/dfts/03-generic-types.py             |  37 ++++
 .../parametric_models/01-parametric-models.py |   2 +-
 lib/stormpy/_template.py                      | 142 +++++++++++++++
 lib/stormpy/dft/__init__.py                   |  49 +-----
 lib/stormpy/dft/simulator.py                  |   6 +-
 lib/stormpy/pars/__init__.py                  |  30 +---
 src/binding_type_index.h                      |  81 +++++++++
 src/dft/analysis.cpp                          |  34 ++--
 src/dft/analysis.h                            |   2 +-
 src/dft/dft.cpp                               |  11 +-
 src/dft/dft.h                                 |   2 +-
 src/dft/dft_elements.cpp                      |  19 +-
 src/dft/dft_elements.h                        |   2 +-
 src/dft/dft_state.cpp                         |  20 ++-
 src/dft/dft_state.h                           |   2 +-
 src/dft/io.cpp                                |   6 +-
 src/dft/simulator.cpp                         |  11 +-
 src/dft/simulator.h                           |   2 +-
 src/dft/transformations.cpp                   |   6 +-
 src/mod_dft.cpp                               |  20 +--
 src/pars/model_instantiator.cpp               |  98 ++++-------
 src/template_binding.h                        | 165 ++++++++++++++++++
 tests/dft/test_analysis.py                    |   6 +-
 tests/dft/test_dft.py                         |  17 +-
 tests/dft/test_dft_simulator.py               |  18 +-
 tests/dft/test_transformations.py             |   5 +-
 tests/pars/test_model_instantiator.py         |   9 +-
 28 files changed, 586 insertions(+), 218 deletions(-)
 create mode 100644 examples/dfts/03-generic-types.py
 create mode 100644 lib/stormpy/_template.py
 create mode 100644 src/binding_type_index.h
 create mode 100644 src/template_binding.h

diff --git a/doc/source/doc/parametric_models.ipynb b/doc/source/doc/parametric_models.ipynb
index 334fcd6963..0cde72858d 100644
--- a/doc/source/doc/parametric_models.ipynb
+++ b/doc/source/doc/parametric_models.ipynb
@@ -58,7 +58,7 @@
    "source": [
     "import stormpy.pars\n",
     "\n",
-    "instantiator = stormpy.pars.PDtmcInstantiator(model)"
+    "instantiator = stormpy.pars.ModelInstantiator[stormpy.ModelType.DTMC, float](model)"
    ]
   },
   {
diff --git a/examples/dfts/03-generic-types.py b/examples/dfts/03-generic-types.py
new file mode 100644
index 0000000000..7af8d4b116
--- /dev/null
+++ b/examples/dfts/03-generic-types.py
@@ -0,0 +1,37 @@
+"""Demonstrate explicit and inferred stormpy template specializations."""
+
+import stormpy
+import stormpy.dft
+import stormpy.examples.files
+
+
+def demonstrate_generic_dft_types():
+    # Readable aliases:
+    assert stormpy.dft._dft._DFT_Double is stormpy.dft.DFT[float]
+    assert stormpy.dft._dft._DFT_RationalFunction is stormpy.dft.DFT[stormpy.RationalFunction]
+
+    path = stormpy.examples.files.dft_json_and
+    double_dft = stormpy.dft.load_dft_json_file(path)
+    assert type(double_dft) is stormpy.dft.DFT[float]
+
+    rational_function_dft = stormpy.dft.load_parametric_dft_json_file(path)
+    assert type(rational_function_dft) is stormpy.dft.DFT[stormpy.RationalFunction]
+
+    # Construct a specialization explicitly:
+    explicit_builder = stormpy.dft.ExplicitDFTModelBuilder[float](double_dft)
+    assert type(explicit_builder) is stormpy.dft.ExplicitDFTModelBuilder[float]
+
+    # Or deduce the specialization from the constructor argument:
+    inferred_builder = stormpy.dft.ExplicitDFTModelBuilder(rational_function_dft)
+    assert type(inferred_builder) is stormpy.dft.ExplicitDFTModelBuilder[stormpy.RationalFunction]
+
+    # Overloaded functions call the specialization:
+    concrete_model = stormpy.dft.build_model(double_dft)
+    assert not concrete_model.supports_parameters
+
+    parametric_model = stormpy.dft.build_model(rational_function_dft)
+    assert parametric_model.supports_parameters
+
+
+if __name__ == "__main__":
+    demonstrate_generic_dft_types()
diff --git a/examples/parametric_models/01-parametric-models.py b/examples/parametric_models/01-parametric-models.py
index 8218c5fd3b..aba4e07ded 100644
--- a/examples/parametric_models/01-parametric-models.py
+++ b/examples/parametric_models/01-parametric-models.py
@@ -16,7 +16,7 @@ def example_parametric_models_01():
     parameters = model.collect_all_parameters()
     assert len(parameters) == 2
 
-    instantiator = stormpy.pars.PDtmcInstantiator(model)
+    instantiator = stormpy.pars.ModelInstantiator[stormpy.ModelType.DTMC, float](model)
     point = dict()
     for x in parameters:
         print(x.name)
diff --git a/lib/stormpy/_template.py b/lib/stormpy/_template.py
new file mode 100644
index 0000000000..13c2497eb1
--- /dev/null
+++ b/lib/stormpy/_template.py
@@ -0,0 +1,142 @@
+"""Runtime representation of C++ template families.
+
+C++ template specializations still need to be compiled and bound separately.
+``TemplateClass`` groups those concrete Python classes behind one public,
+subscriptable object.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Iterator, Mapping
+from types import MappingProxyType
+from typing import Any
+
+
+class TemplateClass:
+    """Native C++ template family exposed as a subscriptable Python object.
+
+    ``family[parameters]`` returns a registered concrete Python class.
+    ``family(*args, **kwargs)`` constructs a class selected by a configured
+    deduction rule.
+    """
+
+    def __init__(
+        self,
+        name: str,
+        module: object,
+        *,
+        deduce_from: TemplateClass | None = None,
+    ) -> None:
+        """Load a native template family.
+
+        :param name: Family name used by the native registration table.
+        :param module: Native module containing the registered specializations.
+        :param deduce_from: Optional constructor deduction guide. For an
+            unsubscripted call, copy the complete parameter tuple of the first
+            argument from this template family. For example,
+            ``deduce_from=DFT`` makes ``Builder(dft)`` select
+            ``Builder[float]`` when ``dft`` is a ``DFT[float]``. Source and
+            target families must have equivalent parameter tuples; no defaults
+            or partial deduction are performed.
+        :raises RuntimeError: If the module has no registrations for ``name``,
+            has an empty registration table, or mixes parameter arities.
+        """
+        try:
+            implementations = module._template_instantiations[name]
+        except (AttributeError, KeyError):
+            raise RuntimeError(f"Native module has no registrations for {name}") from None
+        if not implementations:
+            raise RuntimeError(f"Native module has no registrations for {name}")
+
+        arities = {len(parameters) for parameters in implementations}
+        if len(arities) != 1:
+            raise RuntimeError(f"Native module has inconsistent registrations for {name}")
+
+        self.__name__ = name
+        self._arity = arities.pop()
+        self._deduction_source = deduce_from
+        self._instantiations: dict[tuple[object, ...], type] = {}
+        for parameters, implementation in implementations.items():
+            self.register(parameters, implementation)
+
+    def _normalize(self, parameters: object) -> tuple[object, ...]:
+        """Convert subscription parameters to a validated tuple."""
+        key = parameters if isinstance(parameters, tuple) else (parameters,)
+        if len(key) != self._arity:
+            raise TypeError(f"{self.__name__} expects {self._arity} template " f"parameter{'s' if self._arity != 1 else ''}, got {len(key)}")
+        return key
+
+    def register(self, parameters: object, implementation: type) -> None:
+        """Add a concrete specialization to this family.
+
+        :param parameters: One parameter or a tuple containing the complete
+            template-parameter list.
+        :param implementation: Concrete Python class for those parameters.
+        :raises TypeError: If the parameter count differs from the family's
+            native arity.
+        :raises ValueError: If the parameter tuple is already registered.
+        """
+        key = self._normalize(parameters)
+        if key in self._instantiations:
+            raise ValueError(f"{self.__name__}{key!r} is already registered")
+        self._instantiations[key] = implementation
+
+    def __getitem__(self, parameters: object) -> type:
+        """Return the concrete class registered for ``parameters``.
+
+        A single parameter may be written directly as ``family[T]``; multiple
+        parameters use normal subscription tuple syntax, ``family[T, U]``.
+
+        :raises TypeError: If the parameter count is wrong or no matching
+            specialization is registered.
+        """
+        key = self._normalize(parameters)
+        try:
+            return self._instantiations[key]
+        except KeyError:
+            raise TypeError(f"{self.__name__} has no instantiation for {key!r}") from None
+
+    def __call__(self, *args: Any, **kwargs: Any) -> Any:
+        """Construct an instance of the specialization selected from the first argument.
+
+        The first positional argument is matched against ``deduce_from``. If no
+        deduction source is configured, it is matched against this family,
+        enabling copy-like construction such as ``DFT(existing_dft)``.
+
+        :raises TypeError: If no arguments permit deduction, the first argument
+            is not a uniquely registered instance, or the resulting
+            specialization is unavailable.
+        """
+        if args:
+            parameters = (self._deduction_source or self).parameters_of(args[0])
+        else:
+            raise TypeError(f"{self.__name__} requires explicit template parameters")
+        return self[parameters](*args, **kwargs)
+
+    def parameters_of(self, instance: object) -> tuple[object, ...]:
+        """Return the complete parameter tuple of a registered instance.
+
+        :raises TypeError: If the instance matches zero or multiple registered
+            specializations.
+        """
+        matches = [parameters for parameters, implementation in self._instantiations.items() if isinstance(instance, implementation)]
+        if len(matches) != 1:
+            raise TypeError(f"Cannot infer {self.__name__} template parameters from {type(instance)!r}")
+        return matches[0]
+
+    @property
+    def instantiations(self) -> Mapping[tuple[object, ...], type]:
+        """Map registered parameter tuples to classes without allowing mutation."""
+        return MappingProxyType(self._instantiations)
+
+    def is_instantiation(self, instance: object) -> bool:
+        """Return whether ``instance`` belongs to any registered specialization."""
+        return isinstance(instance, tuple(self._instantiations.values()))
+
+    def __iter__(self) -> Iterator[tuple[object, ...]]:
+        """Iterate over registered parameter tuples in registration order."""
+        return iter(self._instantiations)
+
+    def __repr__(self) -> str:
+        """Return a concise template-family representation."""
+        return f"<template class {self.__name__}>"
diff --git a/lib/stormpy/dft/__init__.py b/lib/stormpy/dft/__init__.py
index ac39a46a95..a5b4f5a0cb 100644
--- a/lib/stormpy/dft/__init__.py
+++ b/lib/stormpy/dft/__init__.py
@@ -6,58 +6,27 @@
 from . import _dft
 from ._dft import *
 from .modules import modules_json
+from stormpy._template import TemplateClass
 
 _dft._set_up()
 
+DFT = TemplateClass("DFT", _dft)
 
-def analyze_dft(ft, properties, symred=True, allow_modularisation=False, relevant_events=RelevantEvents(), allow_dc_for_relevant=False):
-    if isinstance(ft, DFT_double):
-        return _dft._analyze_dft_double(ft, properties, symred, allow_modularisation, relevant_events, allow_dc_for_relevant)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._analyze_dft_ratfunc(ft, properties, symred, allow_modularisation, relevant_events, allow_dc_for_relevant)
+DFTElement = TemplateClass("DFTElement", _dft)
 
+DFTBE = TemplateClass("DFTBE", _dft)
 
-def build_model(ft, symmetries=DftSymmetries(), relevant_events=RelevantEvents(), allow_dc_for_relevant=False):
-    if isinstance(ft, DFT_double):
-        return _dft._build_model_double(ft, symmetries, relevant_events, allow_dc_for_relevant)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._build_model_ratfunc(ft, symmetries, relevant_events, allow_dc_for_relevant)
+DFTDependency = TemplateClass("DFTDependency", _dft)
 
+DFTState = TemplateClass("DFTState", _dft)
 
-def transform_dft(ft, unique_constant_be, binary_fdeps, exponential_distributions):
-    if isinstance(ft, DFT_double):
-        return _dft._transform_dft_double(ft, unique_constant_be, binary_fdeps, exponential_distributions)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._transform_dft_ratfunc(ft, unique_constant_be, binary_fdeps, exponential_distributions)
+DFTSimulator = TemplateClass("DFTSimulator", _dft, deduce_from=DFT)
 
+ExplicitDFTModelBuilder = TemplateClass("ExplicitDFTModelBuilder", _dft, deduce_from=DFT)
 
-def compute_dependency_conflicts(ft, use_smt=False, solver_timeout=0):
-    if isinstance(ft, DFT_double):
-        return _dft._compute_dependency_conflicts_double(ft, use_smt, solver_timeout)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._compute_dependency_conflicts_ratfunc(ft, use_smt, solver_timeout)
+DFTInstantiator = TemplateClass("DFTInstantiator", _dft)
 
 
 def prepare_for_analysis(ft):
     compute_dependency_conflicts(ft, use_smt=False)
     return transform_dft(ft, unique_constant_be=True, binary_fdeps=True, exponential_distributions=True)
-
-
-def is_well_formed(ft, check_valid_for_analysis=True):
-    if isinstance(ft, DFT_double):
-        return _dft._is_well_formed_double(ft, check_valid_for_analysis)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._is_well_formed_ratfunc(ft, check_valid_for_analysis)
-
-
-def has_potential_modeling_issues(ft):
-    if isinstance(ft, DFT_double):
-        return _dft._has_potential_modeling_issues_double(ft)
-    else:
-        assert isinstance(ft, DFT_ratfunc)
-        return _dft._has_potential_modeling_issues_ratfunc(ft)
diff --git a/lib/stormpy/dft/simulator.py b/lib/stormpy/dft/simulator.py
index 44ae3db5c8..f5c0960097 100644
--- a/lib/stormpy/dft/simulator.py
+++ b/lib/stormpy/dft/simulator.py
@@ -25,7 +25,7 @@ def __init__(self, dft, seed=42, relevant=[]):
         # Initialize random generator
         generator = stormpy.dft.RandomGenerator.create(seed)
         # Create simulator
-        self._simulator = stormpy.dft.DFTSimulator_double(self._dft, info, generator)
+        self._simulator = stormpy.dft.DFTSimulator(self._dft, info, generator)
         # Initialize variables
         self._state = None
         self._fail_candidates = dict()
@@ -104,11 +104,11 @@ def _update(self):
         for f in self._state.failable():
             if f.is_due_dependency():
                 self._is_failable_dependency = True
-                fail_dependency = f.as_dependency_double(self._dft)
+                fail_dependency = f.as_dependency(self._dft)
                 fail_be = fail_dependency.dependent_events[0]
                 self._fail_candidates[fail_be.name] = f
             else:
-                fail_be = f.as_be_double(self._dft)
+                fail_be = f.as_be(self._dft)
                 self._fail_candidates[fail_be.name] = f
 
     def let_fail(self, be, dependency_successful=True):
diff --git a/lib/stormpy/pars/__init__.py b/lib/stormpy/pars/__init__.py
index e540a19266..9e6a325478 100644
--- a/lib/stormpy/pars/__init__.py
+++ b/lib/stormpy/pars/__init__.py
@@ -7,38 +7,14 @@
 from ._pars import *
 
 from stormpy import ModelType
+from stormpy._template import TemplateClass
 
 _pars._set_up()
 
 
-class ModelInstantiator:
-    """
-    Class for instantiating models.
-    """
+ModelInstantiator = TemplateClass("ModelInstantiator", _pars)
 
-    def __init__(self, model):
-        """
-        Constructor.
-        :param model: Model.
-        """
-        if model.model_type == ModelType.MDP:
-            self._instantiator = PMdpInstantiator(model)
-        elif model.model_type == ModelType.DTMC:
-            self._instantiator = PDtmcInstantiator(model)
-        elif model.model_type == ModelType.CTMC:
-            self._instantiator = PCtmcInstantiator(model)
-        elif model.model_type == ModelType.MA:
-            self._instantiator = PMaInstantiator(model)
-        else:
-            raise stormpy.exceptions.StormError("Model type {} not supported".format(model.model_type))
-
-    def instantiate(self, valuation):
-        """
-        Instantiate model with given valuation.
-        :param valuation: Valuation from parameter to value.
-        :return: Instantiated model.
-        """
-        return self._instantiator.instantiate(valuation)
+ModelInstantiationChecker = TemplateClass("ModelInstantiationChecker", _pars)
 
 
 def simplify_model(model, formula):
diff --git a/src/binding_type_index.h b/src/binding_type_index.h
new file mode 100644
index 0000000000..a5e82d0633
--- /dev/null
+++ b/src/binding_type_index.h
@@ -0,0 +1,81 @@
+#pragma once
+
+#include <storm/adapters/RationalFunctionAdapter.h>
+#include <storm/adapters/RationalNumberAdapter.h>
+#include <storm/models/ModelType.h>
+
+#include "src/template_binding.h"
+
+namespace stormpy::bindings {
+
+template<typename ValueType>
+struct BindingTypeArgument;
+
+template<>
+struct BindingTypeArgument<double> {
+    static TemplateArgument get() {
+        return {pybind11::module_::import("builtins").attr("float"), "Double"};
+    }
+};
+
+template<>
+struct BindingTypeArgument<storm::RationalNumber> {
+    static TemplateArgument get() {
+        return {pybind11::module_::import("stormpy").attr("Rational"), "Rational"};
+    }
+};
+
+template<>
+struct BindingTypeArgument<storm::RationalFunction> {
+    static TemplateArgument get() {
+        return {pybind11::module_::import("stormpy").attr("RationalFunction"), "RationalFunction"};
+    }
+};
+
+template<typename ValueType>
+TemplateArgument bindingTypeArgument() {
+    return BindingTypeArgument<ValueType>::get();
+}
+
+template<storm::models::ModelType ModelKind>
+struct BindingModelTypeArgument;
+
+template<>
+struct BindingModelTypeArgument<storm::models::ModelType::Dtmc> {
+    static TemplateArgument get() {
+        return {pybind11::cast(storm::models::ModelType::Dtmc), "DTMC"};
+    }
+};
+
+template<>
+struct BindingModelTypeArgument<storm::models::ModelType::Mdp> {
+    static TemplateArgument get() {
+        return {pybind11::cast(storm::models::ModelType::Mdp), "MDP"};
+    }
+};
+
+template<>
+struct BindingModelTypeArgument<storm::models::ModelType::Ctmc> {
+    static TemplateArgument get() {
+        return {pybind11::cast(storm::models::ModelType::Ctmc), "CTMC"};
+    }
+};
+
+template<>
+struct BindingModelTypeArgument<storm::models::ModelType::MarkovAutomaton> {
+    static TemplateArgument get() {
+        return {pybind11::cast(storm::models::ModelType::MarkovAutomaton), "MA"};
+    }
+};
+
+template<typename... ValueTypes>
+TemplateIndex typeIndex() {
+    return makeTemplateIndex({bindingTypeArgument<ValueTypes>()...});
+}
+
+template<storm::models::ModelType ModelKind, typename... ValueTypes>
+TemplateIndex typeIndex() {
+    return makeTemplateIndex({BindingModelTypeArgument<ModelKind>::get(), bindingTypeArgument<ValueTypes>()...});
+}
+
+}  // namespace stormpy::bindings
diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp
index 7599e7cbfe..0abc3616c9 100644
--- a/src/dft/analysis.cpp
+++ b/src/dft/analysis.cpp
@@ -5,6 +5,8 @@
 #include <storm-dft/storage/DftSymmetries.h>
 #include <storm/adapters/RationalFunctionAdapter.h>
 
+#include "src/binding_type_index.h"
+
 template<typename ValueType>
 using ExplicitDFTModelBuilder = storm::dft::builder::ExplicitDFTModelBuilder<ValueType>;
 
@@ -52,9 +54,10 @@ void define_analysis(py::module& m) {
 }
 
 template<typename ValueType>
-void define_analysis_typed(py::module& m, std::string const& vt_suffix) {
-    py::class_<ExplicitDFTModelBuilder<ValueType>, std::shared_ptr<ExplicitDFTModelBuilder<ValueType>>>(m, ("ExplicitDFTModelBuilder" + vt_suffix).c_str(),
-                                                                                                        "Builder to generate explicit model from DFT")
+void define_analysis_typed(py::module& m) {
+    auto builder = stormpy::bindings::bindTemplateClass<ExplicitDFTModelBuilder<ValueType>, std::shared_ptr<ExplicitDFTModelBuilder<ValueType>>>(
+        m, "ExplicitDFTModelBuilder", stormpy::bindings::typeIndex<ValueType>(), "Builder to generate explicit model from DFT");
+    builder
         .def(py::init<storm::dft::storage::DFT<ValueType> const&, storm::dft::storage::DftSymmetries const&>(), "Constructor", py::arg("dft"),
              py::arg("symmetries") = storm::dft::storage::DftSymmetries())
         .def("build", &ExplicitDFTModelBuilder<ValueType>::buildModel, "Build state space of model", py::arg("iteration"),
@@ -63,24 +66,25 @@ void define_analysis_typed(py::module& m, std::string const& vt_suffix) {
         .def("get_partial_model", &ExplicitDFTModelBuilder<ValueType>::getModelApproximation, "Get partial model", py::arg("lower_bound"),
              py::arg("expected_time"));
 
-    m.def(("_analyze_dft" + vt_suffix).c_str(), &analyzeDFT<ValueType>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred") = true,
+    m.def("analyze_dft", &analyzeDFT<ValueType>, "Analyze the DFT", py::arg("dft"), py::arg("properties"), py::arg("symred") = true,
           py::arg("allow_modularisation") = false, py::arg("relevant_events") = storm::dft::utility::RelevantEvents(),
           py::arg("allow_dc_for_relevant") = false);
 
-    m.def(("_build_model" + vt_suffix).c_str(), &buildModel<ValueType>, "Build state-space model (CTMC or MA) for DFT", py::arg("dft"), py::arg("symmetries"),
-          py::arg("relevant_events") = storm::dft::utility::RelevantEvents(), py::arg("allow_dc_for_relevant") = false);
+    m.def("build_model", &buildModel<ValueType>, "Build state-space model (CTMC or MA) for DFT", py::arg("dft"),
+          py::arg("symmetries") = storm::dft::storage::DftSymmetries(), py::arg("relevant_events") = storm::dft::utility::RelevantEvents(),
+          py::arg("allow_dc_for_relevant") = false);
 
-    m.def(("_transform_dft" + vt_suffix).c_str(), &storm::dft::api::applyTransformations<ValueType>, "Apply transformations on DFT", py::arg("dft"),
-          py::arg("unique_constant_be"), py::arg("binary_fdeps"), py::arg("exponential_distributions"));
+    m.def("transform_dft", &storm::dft::api::applyTransformations<ValueType>, "Apply transformations on DFT", py::arg("dft"), py::arg("unique_constant_be"),
+          py::arg("binary_fdeps"), py::arg("exponential_distributions"));
 
-    m.def(("_compute_dependency_conflicts" + vt_suffix).c_str(), &storm::dft::api::computeDependencyConflicts<ValueType>,
-          "Set conflicts between FDEPs. Is used in analysis.", py::arg("dft"), py::arg("use_smt") = false, py::arg("solver_timeout") = 0);
+    m.def("compute_dependency_conflicts", &storm::dft::api::computeDependencyConflicts<ValueType>, "Set conflicts between FDEPs. Is used in analysis.",
+          py::arg("dft"), py::arg("use_smt") = false, py::arg("solver_timeout") = 0);
 
-    m.def(("_is_well_formed" + vt_suffix).c_str(), &storm::dft::api::isWellFormed<ValueType>, "Check whether DFT is well-formed.", py::arg("dft"),
+    m.def("is_well_formed", &storm::dft::api::isWellFormed<ValueType>, "Check whether DFT is well-formed.", py::arg("dft"),
           py::arg("check_valid_for_analysis") = true);
-    m.def(("_has_potential_modeling_issues" + vt_suffix).c_str(), &storm::dft::api::hasPotentialModelingIssues<ValueType>,
-          "Check whether DFT has potential modeling issues.", py::arg("dft"));
+    m.def("has_potential_modeling_issues", &storm::dft::api::hasPotentialModelingIssues<ValueType>, "Check whether DFT has potential modeling issues.",
+          py::arg("dft"));
 }
 
-template void define_analysis_typed<double>(py::module& m, std::string const& vt_suffix);
-template void define_analysis_typed<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
+template void define_analysis_typed<double>(py::module& m);
+template void define_analysis_typed<storm::RationalFunction>(py::module& m);
diff --git a/src/dft/analysis.h b/src/dft/analysis.h
index c58b639ee3..6e1657a7ae 100644
--- a/src/dft/analysis.h
+++ b/src/dft/analysis.h
@@ -5,4 +5,4 @@
 void define_analysis(py::module& m);
 
 template<typename ValueType>
-void define_analysis_typed(py::module& m, std::string const& vt_suffix);
+void define_analysis_typed(py::module& m);
diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp
index eb61ae5ff3..127dc5a4f3 100644
--- a/src/dft/dft.cpp
+++ b/src/dft/dft.cpp
@@ -9,6 +9,7 @@
 #include <storm/adapters/RationalFunctionAdapter.h>
 #include <storm/settings/SettingsManager.h>
 
+#include "src/binding_type_index.h"
 #include "src/helpers.h"
 
 template<typename ValueType>
@@ -34,9 +35,11 @@ void define_dft(py::module& m) {
 }
 
 template<typename ValueType>
-void define_dft_typed(py::module& m, std::string const& vt_suffix) {
+void define_dft_typed(py::module& m) {
     // DFT class
-    py::class_<DFT<ValueType>, std::shared_ptr<DFT<ValueType>>>(m, ("DFT" + vt_suffix).c_str(), "Dynamic Fault Tree")
+    auto dft = stormpy::bindings::bindTemplateClass<DFT<ValueType>, std::shared_ptr<DFT<ValueType>>>(m, "DFT", stormpy::bindings::typeIndex<ValueType>(),
+                                                                                                     "Dynamic Fault Tree");
+    dft.def(py::init<DFT<ValueType> const&>(), "Copy a Dynamic Fault Tree")
         .def("nr_elements", &DFT<ValueType>::nrElements, "Total number of elements")
         .def("nr_be", &DFT<ValueType>::nrBasicElements, "Number of basic elements")
         .def("nr_dynamic", &DFT<ValueType>::nrDynamicElements, "Number of dynamic elements")
@@ -74,5 +77,5 @@ void define_symmetries(py::module& m) {
         .def("__str__", &streamToString<storm::dft::storage::DftSymmetries>);
 }
 
-template void define_dft_typed<double>(py::module& m, std::string const& vt_suffix);
-template void define_dft_typed<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
+template void define_dft_typed<double>(py::module& m);
+template void define_dft_typed<storm::RationalFunction>(py::module& m);
diff --git a/src/dft/dft.h b/src/dft/dft.h
index d766f65cce..cd6c6a56b1 100644
--- a/src/dft/dft.h
+++ b/src/dft/dft.h
@@ -5,6 +5,6 @@
 void define_dft(py::module& m);
 
 template<typename ValueType>
-void define_dft_typed(py::module& m, std::string const& vt_suffix);
+void define_dft_typed(py::module& m);
 
 void define_symmetries(py::module& m);
diff --git a/src/dft/dft_elements.cpp b/src/dft/dft_elements.cpp
index 6e62b91608..73f9a8c74d 100644
--- a/src/dft/dft_elements.cpp
+++ b/src/dft/dft_elements.cpp
@@ -3,6 +3,7 @@
 #include <storm-dft/storage/elements/DFTElements.h>
 #include <storm/adapters/RationalFunctionAdapter.h>
 
+#include "src/binding_type_index.h"
 #include "src/helpers.h"
 
 template<typename ValueType>
@@ -32,22 +33,24 @@ void define_dft_elements(py::module& m) {
 }
 
 template<typename ValueType>
-void define_dft_elements_typed(py::module& m, std::string const& vt_suffix) {
+void define_dft_elements_typed(py::module& m) {
     // DFT elements
-    py::class_<DFTElement<ValueType>, std::shared_ptr<DFTElement<ValueType>>> element(m, ("DFTElement" + vt_suffix).c_str(), "DFT element");
+    auto const index = stormpy::bindings::typeIndex<ValueType>();
+    auto element = stormpy::bindings::bindTemplateClass<DFTElement<ValueType>, std::shared_ptr<DFTElement<ValueType>>>(m, "DFTElement", index, "DFT element");
     element.def_property_readonly("id", &DFTElement<ValueType>::id, "Id")
         .def_property_readonly("name", &DFTElement<ValueType>::name, "Name")
         .def_property_readonly("type", &DFTElement<ValueType>::type, "Type")
         .def("__str__", &DFTElement<ValueType>::toString);
 
-    py::class_<BE<ValueType>, std::shared_ptr<BE<ValueType>>>(m, ("DFTBE" + vt_suffix).c_str(), "Basic Event", element)
-        .def("__str__", &BE<ValueType>::toString);
+    auto be = stormpy::bindings::bindTemplateClass<BE<ValueType>, std::shared_ptr<BE<ValueType>>>(m, "DFTBE", index, "Basic Event", element);
+    be.def("__str__", &BE<ValueType>::toString);
 
-    py::class_<Dependency<ValueType>, std::shared_ptr<Dependency<ValueType>>>(m, ("DFTDependency" + vt_suffix).c_str(), "Dependency", element)
-        .def_property_readonly("trigger", &Dependency<ValueType>::triggerEvent, "Trigger event")
+    auto dependency =
+        stormpy::bindings::bindTemplateClass<Dependency<ValueType>, std::shared_ptr<Dependency<ValueType>>>(m, "DFTDependency", index, "Dependency", element);
+    dependency.def_property_readonly("trigger", &Dependency<ValueType>::triggerEvent, "Trigger event")
         .def_property_readonly("dependent_events", &Dependency<ValueType>::dependentEvents, "Dependent events")
         .def("__str__", &Dependency<ValueType>::toString);
 }
 
-template void define_dft_elements_typed<double>(py::module& m, std::string const& vt_suffix);
-template void define_dft_elements_typed<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
+template void define_dft_elements_typed<double>(py::module& m);
+template void define_dft_elements_typed<storm::RationalFunction>(py::module& m);
diff --git a/src/dft/dft_elements.h b/src/dft/dft_elements.h
index 6b1e34577c..80880fcce6 100644
--- a/src/dft/dft_elements.h
+++ b/src/dft/dft_elements.h
@@ -5,4 +5,4 @@
 void define_dft_elements(py::module& m);
 
 template<typename ValueType>
-void define_dft_elements_typed(py::module& m, std::string const& vt_suffix);
+void define_dft_elements_typed(py::module& m);
diff --git a/src/dft/dft_state.cpp b/src/dft/dft_state.cpp
index 0cece1f799..a930a56669 100644
--- a/src/dft/dft_state.cpp
+++ b/src/dft/dft_state.cpp
@@ -4,6 +4,7 @@
 #include <storm-dft/storage/FailableElements.h>
 #include <storm/adapters/RationalFunctionAdapter.h>
 
+#include "src/binding_type_index.h"
 #include "src/helpers.h"
 
 template<typename ValueType>
@@ -12,10 +13,11 @@ typedef storm::dft::storage::FailableElements Failable;
 typedef storm::dft::storage::FailableElements::const_iterator FailableIter;
 
 template<typename ValueType>
-void define_dft_state(py::module& m, std::string const& vt_suffix) {
+void define_dft_state(py::module& m) {
     // DFT state
-    py::class_<DFTState<ValueType>, std::shared_ptr<DFTState<ValueType>>>(m, ("DFTState" + vt_suffix).c_str(), "DFT state")
-        .def("operational", &DFTState<ValueType>::isOperational, "Is element operational", py::arg("id"))
+    auto state = stormpy::bindings::bindTemplateClass<DFTState<ValueType>, std::shared_ptr<DFTState<ValueType>>>(
+        m, "DFTState", stormpy::bindings::typeIndex<ValueType>(), "DFT state");
+    state.def("operational", &DFTState<ValueType>::isOperational, "Is element operational", py::arg("id"))
         .def(
             "failed", [](DFTState<ValueType> const& state, size_t id) { return state.hasFailed(id); }, "Is element failed", py::arg("id"))
         .def(
@@ -62,11 +64,11 @@ void define_failable_elements(py::module& m) {
 
     py::class_<FailableIter, std::shared_ptr<FailableIter>>(m, "FailableElement", "Failable element")
         .def("is_due_dependency", &FailableIter::isFailureDueToDependency, "Is failure due to dependency")
-        .def("as_be_double", &FailableIter::asBE<double>, py::arg("dft"), "Get BE which fails")
-        .def("as_be_ratfunc", &FailableIter::asBE<storm::RationalFunction>, py::arg("dft"), "Get BE which fails")
-        .def("as_dependency_double", &FailableIter::asDependency<double>, py::arg("dft"), "Get dependency which is triggered")
-        .def("as_dependency_ratfunc", &FailableIter::asDependency<storm::RationalFunction>, py::arg("dft"), "Get dependency which is triggered");
+        .def("as_be", &FailableIter::asBE<double>, py::arg("dft"), "Get BE which fails")
+        .def("as_be", &FailableIter::asBE<storm::RationalFunction>, py::arg("dft"), "Get BE which fails")
+        .def("as_dependency", &FailableIter::asDependency<double>, py::arg("dft"), "Get dependency which is triggered")
+        .def("as_dependency", &FailableIter::asDependency<storm::RationalFunction>, py::arg("dft"), "Get dependency which is triggered");
 }
 
-template void define_dft_state<double>(py::module& m, std::string const& vt_suffix);
-template void define_dft_state<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
+template void define_dft_state<double>(py::module& m);
+template void define_dft_state<storm::RationalFunction>(py::module& m);
diff --git a/src/dft/dft_state.h b/src/dft/dft_state.h
index ff3e0ad187..1e190b7945 100644
--- a/src/dft/dft_state.h
+++ b/src/dft/dft_state.h
@@ -3,6 +3,6 @@
 #include "src/dft/common.h"
 
 template<typename ValueType>
-void define_dft_state(py::module& m, std::string const& vt_suffix);
+void define_dft_state(py::module& m);
 
 void define_failable_elements(py::module& m);
diff --git a/src/dft/io.cpp b/src/dft/io.cpp
index e05ea43791..82965cbdfe 100644
--- a/src/dft/io.cpp
+++ b/src/dft/io.cpp
@@ -20,8 +20,6 @@ void define_output(py::module& m) {
     // Export DFT
     m.def("export_dft_json_file", &storm::dft::api::exportDFTToJsonFile<double>, "Export DFT to JSON file", py::arg("dft"), py::arg("path"));
     m.def("export_dft_json_string", &storm::dft::api::exportDFTToJsonString<double>, "Export DFT to JSON string", py::arg("dft"));
-    m.def("export_parametric_dft_json_file", &storm::dft::api::exportDFTToJsonFile<storm::RationalFunction>, "Export parametric DFT to JSON file",
-          py::arg("dft"), py::arg("path"));
-    m.def("export_parametric_dft_json_string", &storm::dft::api::exportDFTToJsonString<storm::RationalFunction>, "Export parametric DFT to JSON string",
-          py::arg("dft"));
+    m.def("export_dft_json_file", &storm::dft::api::exportDFTToJsonFile<storm::RationalFunction>, "Export DFT to JSON file", py::arg("dft"), py::arg("path"));
+    m.def("export_dft_json_string", &storm::dft::api::exportDFTToJsonString<storm::RationalFunction>, "Export DFT to JSON string", py::arg("dft"));
 }
diff --git a/src/dft/simulator.cpp b/src/dft/simulator.cpp
index 50c98ae0c2..05608d5ce9 100644
--- a/src/dft/simulator.cpp
+++ b/src/dft/simulator.cpp
@@ -4,6 +4,7 @@
 #include <storm-dft/generator/DftNextStateGenerator.h>
 #include <storm-dft/simulator/DFTTraceSimulator.h>
 
+#include "src/binding_type_index.h"
 #include "src/helpers.h"
 
 template<typename ValueType>
@@ -32,9 +33,11 @@ void define_simulator(py::module& m) {
 }
 
 template<typename ValueType>
-void define_simulator_typed(py::module& m, std::string const& vt_suffix) {
+void define_simulator_typed(py::module& m) {
     // Simulator for DFTs
-    py::class_<Simulator<ValueType>, std::shared_ptr<Simulator<ValueType>>>(m, ("DFTSimulator" + vt_suffix).c_str(), "Simulator for DFT traces")
+    auto simulator = stormpy::bindings::bindTemplateClass<Simulator<ValueType>, std::shared_ptr<Simulator<ValueType>>>(
+        m, "DFTSimulator", stormpy::bindings::typeIndex<ValueType>(), "Simulator for DFT traces");
+    simulator
         .def(py::init<storm::dft::storage::DFT<ValueType> const&, DFTStateInfo const&, RandomGenerator&>(), py::keep_alive<1, 2>(), py::keep_alive<1, 3>(),
              py::keep_alive<1, 4>(), py::arg("dft"), py::arg("state_generation_info"), py::arg("generator"), "Create Simulator")
         .def("reset", &Simulator<ValueType>::resetToInitial, "Reset to initial state")
@@ -47,5 +50,5 @@ void define_simulator_typed(py::module& m, std::string const& vt_suffix) {
         .def("simulate_trace", &Simulator<ValueType>::simulateCompleteTrace, py::arg("timebound"), "Simulate complete trace for given timebound");
 }
 
-template void define_simulator_typed<double>(py::module& m, std::string const& vt_suffix);
-template void define_simulator_typed<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
+template void define_simulator_typed<double>(py::module& m);
+template void define_simulator_typed<storm::RationalFunction>(py::module& m);
diff --git a/src/dft/simulator.h b/src/dft/simulator.h
index 3a745e046b..50e2db25d3 100644
--- a/src/dft/simulator.h
+++ b/src/dft/simulator.h
@@ -5,4 +5,4 @@
 void define_simulator(py::module& m);
 
 template<typename ValueType>
-void define_simulator_typed(py::module& m, std::string const& vt_suffix);
+void define_simulator_typed(py::module& m);
diff --git a/src/dft/transformations.cpp b/src/dft/transformations.cpp
index eaef552983..5e51b090dd 100644
--- a/src/dft/transformations.cpp
+++ b/src/dft/transformations.cpp
@@ -3,12 +3,14 @@
 #include <storm-dft/transformations/DftInstantiator.h>
 #include <storm/adapters/RationalFunctionAdapter.h>
 
+#include "src/binding_type_index.h"
 #include "src/helpers.h"
 
 using DFTInstantiator = storm::dft::transformations::DftInstantiator<storm::RationalFunction, double>;
 
 void define_transformations(py::module& m) {
-    py::class_<DFTInstantiator, std::shared_ptr<DFTInstantiator>>(m, "DFTInstantiator", "Instantiator for parametric DFT")
-        .def(py::init<storm::dft::storage::DFT<storm::RationalFunction> const&>(), "Initialize with parametric DFT", py::arg("dft"))
+    auto instantiator = stormpy::bindings::bindTemplateClass<DFTInstantiator, std::shared_ptr<DFTInstantiator>>(
+        m, "DFTInstantiator", stormpy::bindings::typeIndex<storm::RationalFunction, double>(), "Instantiator for parametric DFT");
+    instantiator.def(py::init<storm::dft::storage::DFT<storm::RationalFunction> const&>(), "Initialize with parametric DFT", py::arg("dft"))
         .def("instantiate", &DFTInstantiator::instantiate, "Instantiate parametric DFT and obtain concrete DFT", py::arg("valuation"));
 }
diff --git a/src/mod_dft.cpp b/src/mod_dft.cpp
index de16a5cec1..229d9c6217 100644
--- a/src/mod_dft.cpp
+++ b/src/mod_dft.cpp
@@ -18,22 +18,22 @@ PYBIND11_MODULE(_dft, m) {
 
     define_symmetries(m);  // Must be before define_analysis_typed
     define_analysis(m);
-    define_analysis_typed<double>(m, "_double");
-    define_analysis_typed<storm::RationalFunction>(m, "_ratfunc");
+    define_analysis_typed<double>(m);
+    define_analysis_typed<storm::RationalFunction>(m);
     define_dft(m);
-    define_dft_typed<double>(m, "_double");
-    define_dft_typed<storm::RationalFunction>(m, "_ratfunc");
+    define_dft_typed<double>(m);
+    define_dft_typed<storm::RationalFunction>(m);
     define_dft_elements(m);
-    define_dft_elements_typed<double>(m, "_double");
-    define_dft_elements_typed<storm::RationalFunction>(m, "_ratfunc");
-    define_dft_state<double>(m, "_double");
-    define_dft_state<storm::RationalFunction>(m, "_ratfunc");
+    define_dft_elements_typed<double>(m);
+    define_dft_elements_typed<storm::RationalFunction>(m);
+    define_dft_state<double>(m);
+    define_dft_state<storm::RationalFunction>(m);
     define_failable_elements(m);
     define_input(m);
     define_module(m);
     define_output(m);
     define_simulator(m);
-    define_simulator_typed<double>(m, "_double");
-    define_simulator_typed<storm::RationalFunction>(m, "_ratfunc");
+    define_simulator_typed<double>(m);
+    define_simulator_typed<storm::RationalFunction>(m);
     define_transformations(m);
 }
diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp
index fc946c9024..267b54e60b 100644
--- a/src/pars/model_instantiator.cpp
+++ b/src/pars/model_instantiator.cpp
@@ -18,6 +18,8 @@
 #include <storm/utility/graph.h>
 #include <storm/utility/vector.h>
 
+#include "src/binding_type_index.h"
+
 template<typename ValueType>
 using Model = storm::models::sparse::Model<ValueType>;
 template<typename ValueType>
@@ -32,59 +34,41 @@ using MarkovAutomaton = storm::models::sparse::MarkovAutomaton<ValueType>;
 using namespace storm::modelchecker;
 
 // Helper: define typed ModelInstantiator class
-template<typename ParametricModel, typename InstantiatedModel>
-void define_typed_instantiator(py::module& m, const char* pyName, const char* pyDesc) {
-    py::class_<storm::utility::ModelInstantiator<ParametricModel, InstantiatedModel>>(m, pyName, pyDesc)
-        .def(py::init<ParametricModel>(), "parametric model"_a)
-        .def("instantiate", &storm::utility::ModelInstantiator<ParametricModel, InstantiatedModel>::instantiate,
-             "Instantiate model with given parameter values");
+template<storm::models::ModelType ModelKind, template<typename> class SparseModel, typename ValueType>
+void define_typed_instantiator(py::module& m) {
+    using ParametricModel = SparseModel<storm::RationalFunction>;
+    using InstantiatedModel = SparseModel<ValueType>;
+    using Instantiator = storm::utility::ModelInstantiator<ParametricModel, InstantiatedModel>;
+
+    auto implementation = stormpy::bindings::bindTemplateClass<Instantiator>(m, "ModelInstantiator", stormpy::bindings::typeIndex<ModelKind, ValueType>(),
+                                                                             "Instantiate a parametric model");
+    implementation.def(py::init<ParametricModel>(), "parametric model"_a)
+        .def("instantiate", &Instantiator::instantiate, "Instantiate model with given parameter values");
 }
 
 template<typename ValueType>
 void define_model_instantiator(py::module& m) {
-    std::string prefix;
-    if constexpr (std::is_same_v<ValueType, double>) {
-        prefix = "";
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
-        prefix = "Partial";
-    }
-
-    define_typed_instantiator<Dtmc<storm::RationalFunction>, Dtmc<ValueType>>(m, (prefix + "PDtmcInstantiator").c_str(), "Instantiate PDTMCs to DTMCs");
-    define_typed_instantiator<Mdp<storm::RationalFunction>, Mdp<ValueType>>(m, (prefix + "PMdpInstantiator").c_str(), "Instantiate PMDPs to MDPs");
-    define_typed_instantiator<Ctmc<storm::RationalFunction>, Ctmc<ValueType>>(m, (prefix + "PCtmcInstantiator").c_str(), "Instantiate PCTMCs to CTMCs");
-    define_typed_instantiator<MarkovAutomaton<storm::RationalFunction>, MarkovAutomaton<ValueType>>(m, (prefix + "PMaInstantiator").c_str(),
-                                                                                                    "Instantiate PMAs to MAs");
+    define_typed_instantiator<storm::models::ModelType::Dtmc, Dtmc, ValueType>(m);
+    define_typed_instantiator<storm::models::ModelType::Mdp, Mdp, ValueType>(m);
+    define_typed_instantiator<storm::models::ModelType::Ctmc, Ctmc, ValueType>(m);
+    define_typed_instantiator<storm::models::ModelType::MarkovAutomaton, MarkovAutomaton, ValueType>(m);
 }
 
-// Trait: maps (ModelType, ResultType) to the specific checker class
-template<typename, typename>
-struct instantiation_checker;
-
-template<typename ResultType>
-struct instantiation_checker<Dtmc<storm::RationalFunction>, ResultType> {
-    using type = SparseDtmcInstantiationModelChecker<Dtmc<storm::RationalFunction>, ResultType>;
-};
-
-template<typename ResultType>
-struct instantiation_checker<Mdp<storm::RationalFunction>, ResultType> {
-    using type = SparseMdpInstantiationModelChecker<Mdp<storm::RationalFunction>, ResultType>;
-};
-
-template<typename ResultType>
-struct instantiation_checker<Ctmc<storm::RationalFunction>, ResultType> {
-    using type = SparseCtmcInstantiationModelChecker<Ctmc<storm::RationalFunction>, ResultType>;
-};
-
 // Helper: define typed base + derived instantiation checker pair
-template<typename ModelType, typename ResultType>
-void define_typed_checker(py::module& m, const char* baseName, const char* baseDesc, const char* derivedName, const char* derivedDesc) {
-    using CheckerType = typename instantiation_checker<ModelType, ResultType>::type;
-    using BaseChecker = SparseInstantiationModelChecker<ModelType, ResultType>;
-    auto base = py::class_<BaseChecker, std::shared_ptr<BaseChecker>>(m, baseName, baseDesc);
+template<storm::models::ModelType ModelKind, template<typename> class SparseModel, template<typename, typename> class InstantiationChecker, typename ResultType>
+void define_typed_checker(py::module& m) {
+    using ParametricModel = SparseModel<storm::RationalFunction>;
+    using CheckerType = InstantiationChecker<ParametricModel, ResultType>;
+    using BaseChecker = SparseInstantiationModelChecker<ParametricModel, ResultType>;
+    auto const index = stormpy::bindings::typeIndex<ModelKind, ResultType>();
+
+    auto base = stormpy::bindings::bindInternalClass<BaseChecker, std::shared_ptr<BaseChecker>>(
+        m, stormpy::bindings::templateClassName("ModelInstantiationCheckerBase", index), "Instantiation checker base");
     base.def("specify_formula", &BaseChecker::specifyFormula, "check_task"_a);
 
-    py::class_<CheckerType, std::shared_ptr<CheckerType>>(m, derivedName, derivedDesc, base)
-        .def(py::init<ModelType>(), "parametric model"_a)
+    auto implementation = stormpy::bindings::bindTemplateClass<CheckerType, std::shared_ptr<CheckerType>>(m, "ModelInstantiationChecker", index,
+                                                                                                          "Instantiate and check a parametric model", base);
+    implementation.def(py::init<ParametricModel>(), "parametric model"_a)
         .def(
             "check",
             [](CheckerType& c, storm::Environment const& env,
@@ -95,29 +79,9 @@ void define_typed_checker(py::module& m, const char* baseName, const char* baseD
 
 template<typename ValueType>
 void define_model_instantiation_checker(py::module& m) {
-    std::string exactStr, exactDesc;
-    if constexpr (std::is_same_v<ValueType, double>) {
-        exactStr = "";
-        exactDesc = "";
-    } else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
-        exactStr = "Exact";
-        exactDesc = "exact ";
-    }
-
-    // Dtmc
-    define_typed_checker<Dtmc<storm::RationalFunction>, ValueType>(
-        m, ("_PDtmc" + exactStr + "InstantiationCheckerBase").c_str(), ("Instantiate pDTMCs to " + exactDesc + "DTMCs and immediately check (base)").c_str(),
-        ("PDtmc" + exactStr + "InstantiationChecker").c_str(), ("Instantiate pDTMCs to " + exactDesc + "DTMCs and immediately check").c_str());
-
-    // Mdp
-    define_typed_checker<Mdp<storm::RationalFunction>, ValueType>(
-        m, ("_PMdp" + exactStr + "InstantiationCheckerBase").c_str(), ("Instantiate pMDPs to " + exactDesc + "MDPs and immediately check (base)").c_str(),
-        ("PMdp" + exactStr + "InstantiationChecker").c_str(), ("Instantiate PMDP to " + exactDesc + "MDPs and immediately check").c_str());
-
-    // Ctmc
-    define_typed_checker<Ctmc<storm::RationalFunction>, ValueType>(
-        m, ("_PCtmc" + exactStr + "InstantiationCheckerBase").c_str(), ("Instantiate pCTMCs to " + exactDesc + "CTMCs and immediately check (base)").c_str(),
-        ("PCtmc" + exactStr + "InstantiationChecker").c_str(), ("Instantiate pCTMCs to " + exactDesc + "CTMCs and immediately check").c_str());
+    define_typed_checker<storm::models::ModelType::Dtmc, Dtmc, SparseDtmcInstantiationModelChecker, ValueType>(m);
+    define_typed_checker<storm::models::ModelType::Mdp, Mdp, SparseMdpInstantiationModelChecker, ValueType>(m);
+    define_typed_checker<storm::models::ModelType::Ctmc, Ctmc, SparseCtmcInstantiationModelChecker, ValueType>(m);
 }
 
 template void define_model_instantiator<double>(py::module&);
diff --git a/src/template_binding.h b/src/template_binding.h
new file mode 100644
index 0000000000..98e1797a65
--- /dev/null
+++ b/src/template_binding.h
@@ -0,0 +1,165 @@
+#pragma once
+
+#include <initializer_list>
+#include <pybind11/pybind11.h>
+#include <stdexcept>
+#include <string>
+#include <string_view>
+#include <utility>
+
+namespace stormpy::bindings {
+
+/**
+ * Python lookup key and stable native-name component for one template
+ * parameter.
+ *
+ * The key is used by Python subscription, for example `float` in `DFT[float]`.
+ * The label is used only in the descriptive native class name, for example
+ * `Double` in `_DFT_Double`. Labels are explicit so implementation-specific
+ * Python type names do not leak into the binding API.
+ */
+struct TemplateArgument {
+    /// Object accepted as this parameter in Python template subscription.
+    pybind11::object key;
+
+    /// Identifier fragment used in the concrete native class name.
+    std::string label;
+};
+
+/** Complete lookup key and native-name suffix for one specialization. */
+struct TemplateIndex {
+    /// Ordered Python template-parameter tuple.
+    pybind11::tuple key;
+
+    /// Concatenated label fragments, each prefixed by an underscore.
+    std::string label;
+};
+
+/**
+ * Combine individual template arguments into a specialization index.
+ *
+ * Argument order is preserved in both the Python key and native label. For
+ * example, arguments `(ModelType.DTMC, float)` with labels `(DTMC, Double)`
+ * produce the key `(ModelType.DTMC, float)` and label `_DTMC_Double`.
+ *
+ * @param arguments Ordered template arguments.
+ * @return Complete index used for lookup, naming, and registration.
+ */
+inline TemplateIndex makeTemplateIndex(std::initializer_list<TemplateArgument> arguments) {
+    pybind11::tuple key(arguments.size());
+    std::string label;
+    std::size_t position = 0;
+    for (auto const& argument : arguments) {
+        key[position++] = argument.key;
+        label += "_" + argument.label;
+    }
+    return {std::move(key), std::move(label)};
+}
+
+/**
+ * Produce the stable native name of a concrete template specialization.
+ *
+ * Native names intentionally begin with an underscore because the generic
+ * `TemplateClass` object is the public API. The concrete class remains
+ * directly accessible from the native module for inspection and advanced use.
+ *
+ * @param family Public template-family name.
+ * @param index Specialization index.
+ * @return A name such as `_DFT_Double`.
+ */
+inline std::string templateClassName(std::string_view family, TemplateIndex const& index) {
+    return "_" + std::string(family) + index.label;
+}
+
+/**
+ * Bind a descriptively named native class without registering a template
+ * specialization.
+ *
+ * This is used for implementation classes such as specialization-specific
+ * bases that Python users do not select through `TemplateClass`.
+ *
+ * @tparam Class Bound C++ class.
+ * @tparam Options Additional `pybind11::class_` options, such as holder types.
+ * @tparam Extra Types of additional constructor arguments forwarded to
+ *     `pybind11::class_`, such as base-class handles.
+ * @param module Native module receiving the class.
+ * @param name Complete native Python class name.
+ * @param description Python class docstring.
+ * @param extra Additional arguments forwarded to `pybind11::class_`.
+ * @return The class binding, ready for `.def(...)` calls.
+ */
+template<typename Class, typename... Options, typename... Extra>
+pybind11::class_<Class, Options...> bindInternalClass(pybind11::module_& module, std::string const& name, char const* description, Extra&&... extra) {
+    pybind11::class_<Class, Options...> result(module, name.c_str(), description, std::forward<Extra>(extra)...);
+    return result;
+}
+
+/**
+ * Return the registration dictionary for a template family, creating it when
+ * necessary.
+ *
+ * Registrations are stored on the native module as:
+ *
+ * @code{.py}
+ * module._template_instantiations = {
+ *     "DFT": {
+ *         (float,): module._DFT_Double,
+ *     },
+ * }
+ * @endcode
+ *
+ * `TemplateClass` reads this table when the Python package is initialized.
+ *
+ * @param module Native module owning the registrations.
+ * @param family Public template-family name.
+ * @return Borrowed family dictionary mapping parameter tuples to classes.
+ */
+inline pybind11::dict templateInstantiations(pybind11::module_& module, std::string_view family) {
+    pybind11::dict families;
+    if (pybind11::hasattr(module, "_template_instantiations")) {
+        families = pybind11::reinterpret_borrow<pybind11::dict>(module.attr("_template_instantiations"));
+    } else {
+        families = pybind11::dict();
+        module.attr("_template_instantiations") = families;
+    }
+
+    pybind11::str const familyName(family);
+    if (!families.contains(familyName)) {
+        families[familyName] = pybind11::dict();
+    }
+    return pybind11::reinterpret_borrow<pybind11::dict>(families[familyName]);
+}
+
+/**
+ * Bind and register one concrete specialization of a template family.
+ *
+ * The class receives a stable descriptive native name and is inserted into the
+ * module registration table under `index.key`. Registering the same family and
+ * key twice is an error.
+ *
+ * @tparam Class Bound C++ specialization.
+ * @tparam Options Additional `pybind11::class_` options, such as holder types.
+ * @tparam Extra Types of additional constructor arguments forwarded to
+ *     `pybind11::class_`, such as base-class handles.
+ * @param module Native module receiving the class and registration.
+ * @param family Public template-family name.
+ * @param index Complete specialization lookup and naming index.
+ * @param description Python class docstring.
+ * @param extra Additional arguments forwarded to `pybind11::class_`.
+ * @return The class binding, ready for `.def(...)` calls.
+ * @throws std::runtime_error If the family already contains `index.key`.
+ */
+template<typename Class, typename... Options, typename... Extra>
+pybind11::class_<Class, Options...> bindTemplateClass(pybind11::module_& module, std::string_view family, TemplateIndex const& index, char const* description,
+                                                      Extra&&... extra) {
+    pybind11::dict instantiations = templateInstantiations(module, family);
+    if (instantiations.contains(index.key)) {
+        throw std::runtime_error("Duplicate native template instantiation for " + std::string(family));
+    }
+
+    auto result = bindInternalClass<Class, Options...>(module, templateClassName(family, index), description, std::forward<Extra>(extra)...);
+    instantiations[index.key] = result;
+    return result;
+}
+
+}  // namespace stormpy::bindings
diff --git a/tests/dft/test_analysis.py b/tests/dft/test_analysis.py
index 8acb9b2f1b..e4c8481bbb 100644
--- a/tests/dft/test_analysis.py
+++ b/tests/dft/test_analysis.py
@@ -25,7 +25,7 @@ def test_build_model(self):
 
     def test_explicit_model_builder(self):
         dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
-        builder = stormpy.dft.ExplicitDFTModelBuilder_double(dft)
+        builder = stormpy.dft.ExplicitDFTModelBuilder[float](dft)
         builder.build(0)
         model = builder.get_model()
         assert model.model_type == stormpy.ModelType.CTMC
@@ -42,7 +42,7 @@ def test_explicit_model_builder_approximation(self):
         assert not issue
         properties = stormpy.parse_properties('T=? [ F "failed" ]')
         prop = properties[0]
-        builder = stormpy.dft.ExplicitDFTModelBuilder_double(dft)
+        builder = stormpy.dft.ExplicitDFTModelBuilder(dft)
 
         # Iteration 0
         builder.build(0, 1.0)
@@ -98,7 +98,7 @@ def test_explicit_model_builder_approximation_complete(self):
         dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc.dft"))
         properties = stormpy.parse_properties('T=? [ F "failed" ]')
         prop = properties[0]
-        builder = stormpy.dft.ExplicitDFTModelBuilder_double(dft)
+        builder = stormpy.dft.ExplicitDFTModelBuilder(dft)
 
         # Iteration 0
         builder.build(0, 1.0)
diff --git a/tests/dft/test_dft.py b/tests/dft/test_dft.py
index 6ae4e9cf16..7f2fdcea97 100644
--- a/tests/dft/test_dft.py
+++ b/tests/dft/test_dft.py
@@ -9,6 +9,21 @@
 
 @dft
 class TestDft:
+    def test_generic_dft_type(self):
+        dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
+
+        concrete_type = stormpy.dft.DFT[float]
+        assert type(dft) is concrete_type
+        assert concrete_type is stormpy.dft._dft._DFT_Double
+
+        explicit_copy = stormpy.dft.DFT[float](dft)
+        inferred_copy = stormpy.dft.DFT(dft)
+        assert type(explicit_copy) is concrete_type
+        assert type(inferred_copy) is concrete_type
+
+        builder = stormpy.dft.ExplicitDFTModelBuilder(dft)
+        assert type(builder) is stormpy.dft.ExplicitDFTModelBuilder[float]
+
     def test_parametric_dft(self):
         from stormpy import pycarl
 
@@ -17,7 +32,7 @@ def test_parametric_dft(self):
         assert dft.nr_elements() == 7
         assert dft.nr_be() == 4
         assert dft.nr_dynamic() == 0
-        assert type(dft) is stormpy.dft.DFT_ratfunc
+        assert type(dft) is stormpy.dft.DFT[stormpy.RationalFunction]
         parameters = stormpy.dft.get_parameters(dft)
         param_names = [x.name for x in parameters]
         assert "x" in param_names
diff --git a/tests/dft/test_dft_simulator.py b/tests/dft/test_dft_simulator.py
index f24e41b6bf..311725e0cf 100644
--- a/tests/dft/test_dft_simulator.py
+++ b/tests/dft/test_dft_simulator.py
@@ -12,7 +12,7 @@ def test_random_steps(self):
         dft.set_relevant_events(stormpy.dft.RelevantEvents(), False)
         info = dft.state_generation_info()
         generator = stormpy.dft.RandomGenerator.create(5)
-        simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
+        simulator = stormpy.dft.DFTSimulator(dft, info, generator)
         old_time = 0
         res = simulator.random_step()
         assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
@@ -35,7 +35,7 @@ def test_simulate_trace(self):
         dft.set_relevant_events(stormpy.dft.RelevantEvents(), False)
         info = dft.state_generation_info()
         generator = stormpy.dft.RandomGenerator.create(5)
-        simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
+        simulator = stormpy.dft.DFTSimulator(dft, info, generator)
         res = simulator.simulate_trace(2)
         assert res == stormpy.dft.SimulationTraceResult.SUCCESSFUL
         res = simulator.simulate_trace(2)
@@ -49,7 +49,7 @@ def test_simulate_trace(self):
         dft.set_relevant_events(stormpy.dft.RelevantEvents(), False)
         info = dft.state_generation_info()
         generator = stormpy.dft.RandomGenerator.create(5)
-        simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
+        simulator = stormpy.dft.DFTSimulator(dft, info, generator)
         res = simulator.simulate_trace(2)
         assert res == stormpy.dft.SimulationTraceResult.UNSUCCESSFUL
         res = simulator.simulate_trace(2)
@@ -62,7 +62,7 @@ def test_steps(self):
         dft.set_relevant_events(stormpy.dft.RelevantEvents(), False)
         info = dft.state_generation_info()
         generator = stormpy.dft.RandomGenerator.create(5)
-        simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
+        simulator = stormpy.dft.DFTSimulator(dft, info, generator)
 
         failable_check = ["B", "C"]
         a = dft.get_element_by_name("A").id
@@ -81,7 +81,7 @@ def test_steps(self):
         failable = state.failable()
         for f in failable:
             assert not f.is_due_dependency()
-            fail_be = f.as_be_double(dft)
+            fail_be = f.as_be(dft)
             assert fail_be.name in failable_check
             if fail_be.name == "C":
                 next_fail = f
@@ -100,7 +100,7 @@ def test_steps(self):
         failable = state.failable()
         for f in failable:
             assert not f.is_due_dependency()
-            fail_be = f.as_be_double(dft)
+            fail_be = f.as_be(dft)
             assert fail_be.name == "B"
             next_fail = f
         res = simulator.step(next_fail)
@@ -123,7 +123,7 @@ def test_steps_dependency(self):
         dft.set_relevant_events(stormpy.dft.RelevantEvents(), False)
         info = dft.state_generation_info()
         generator = stormpy.dft.RandomGenerator.create(5)
-        simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
+        simulator = stormpy.dft.DFTSimulator(dft, info, generator)
 
         p = dft.get_element_by_name("P").id
         b = dft.get_element_by_name("B").id
@@ -138,7 +138,7 @@ def test_steps_dependency(self):
         failable = state.failable()
         for f in failable:
             assert not f.is_due_dependency()
-            fail_be = f.as_be_double(dft)
+            fail_be = f.as_be(dft)
             assert fail_be.name in ["B", "P", "B_Power"]
             if fail_be.name == "B_Power":
                 next_fail = f
@@ -153,7 +153,7 @@ def test_steps_dependency(self):
         failable = state.failable()
         for f in failable:
             assert f.is_due_dependency
-            fail_dependency = f.as_dependency_double(dft)
+            fail_dependency = f.as_dependency(dft)
             assert len(fail_dependency.dependent_events) == 1
             fail_be = fail_dependency.dependent_events[0]
             assert fail_be.name in ["B", "P"]
diff --git a/tests/dft/test_transformations.py b/tests/dft/test_transformations.py
index a9dd697a45..032cc7f1ac 100644
--- a/tests/dft/test_transformations.py
+++ b/tests/dft/test_transformations.py
@@ -14,7 +14,10 @@ def test_instantiate_dft(self):
         assert dft.nr_elements() == 7
         assert dft.nr_be() == 4
 
-        instantiator = stormpy.dft.DFTInstantiator(dft)
+        instantiator_type = stormpy.dft.DFTInstantiator[stormpy.RationalFunction, float]
+        instantiator = instantiator_type(dft)
+        assert type(instantiator) is instantiator_type
+        assert instantiator_type is stormpy.dft._dft._DFTInstantiator_RationalFunction_Double
         x = pycarl.variable_with_name("x")
         y = pycarl.variable_with_name("y")
         valuation = {x: stormpy.RationalRF("5"), y: stormpy.RationalRF("0.01")}
diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py
index b01483a777..f14667c568 100644
--- a/tests/pars/test_model_instantiator.py
+++ b/tests/pars/test_model_instantiator.py
@@ -1,4 +1,5 @@
 import stormpy
+import pytest
 from helpers.helper import get_example_path
 
 from configurations import pars
@@ -13,7 +14,7 @@ def test_instantiate_dtmc(self):
         model = stormpy.build_parametric_model(program, formulas)
         parameters = model.collect_all_parameters()
         assert len(parameters) == 2
-        instantiator = stormpy.pars.ModelInstantiator(model)
+        instantiator = stormpy.pars.ModelInstantiator[stormpy.ModelType.DTMC, float](model)
 
         point = {p: stormpy.RationalRF("0.4") for p in parameters}
         instantiated_model = instantiator.instantiate(point)
@@ -31,7 +32,7 @@ def test_sample_pdtmc(self):
         model = stormpy.build_parametric_model(program, formulas)
 
         parameters = model.collect_all_parameters()
-        instantiator = stormpy.pars.PDtmcInstantiator(model)
+        instantiator = stormpy.pars.ModelInstantiator[stormpy.ModelType.DTMC, float](model)
 
         point = {p: stormpy.RationalRF("0.4") for p in parameters}
         instantiated_model = instantiator.instantiate(point)
@@ -49,7 +50,7 @@ def test_pdtmc_instantiation_checker(self):
         model = stormpy.build_parametric_model(program, formulas)
 
         parameters = model.collect_all_parameters()
-        inst_checker = stormpy.pars.PDtmcInstantiationChecker(model)
+        inst_checker = stormpy.pars.ModelInstantiationChecker[stormpy.ModelType.DTMC, float](model)
         inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True))
         inst_checker.set_graph_preserving(True)
         env = stormpy.Environment()
@@ -67,7 +68,7 @@ def test_pdtmc_exact_instantiation_checker(self):
         model = stormpy.build_parametric_model(program, formulas)
 
         parameters = model.collect_all_parameters()
-        inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(model)
+        inst_checker = stormpy.pars.ModelInstantiationChecker[stormpy.ModelType.DTMC, stormpy.Rational](model)
         inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True))
         inst_checker.set_graph_preserving(True)
         env = stormpy.Environment()