Consistent and readable generics

[linusheck]

Adds a new generic handling that automatically generates instantiations for the given types and then puts a wrapper (in _template.py) around it to allow for this functionality:

# 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

This replaces the custom Python wrapper functions that currently check input types.

This is a breaking API change for version 2.0. Let's discuss whether to re-export the old type names.

This PR migrates pars and dft, more PRs that I will open on top of this will migrate the rest of stormpy.

[volkm]

Thanks for adding these changes. Can you maybe rebase from the latest master? Then it is easier to see your changes.

[Copilot]

🔵 Needs a closer look

The new parser has incorrect implication association and ambiguous equality parsing, and the release version conflicts with the stated breaking-change plan.

Pull request overview

Introduces generic runtime bindings for DFT and parametric model types while migrating stormpy to Storm 1.14, pybind11 smart holders, revised valuations, and a Lark-based parser.

Changes:

• Adds generic specialization registration and inference for DFT/pars APIs.
• Updates Storm 1.14 bindings, valuations, environments, build configuration, and tests.
• Replaces carl-parser with optional Lark parsing and modernizes CI/release packaging.

File summaries

File	Description
tests/storage/test_valuations.py	Tests generalized valuations.
tests/storage/test_state_valuation.py	Removes superseded tests.
tests/storage/test_model_components.py	Migrates valuation construction.
tests/storage/test_matrix_builder.py	Removes debug output.
tests/storage/test_bitvector.py	Tests expanded BitVector API.
tests/pycarl/parse/conftest.py	Configures optional Lark parser.
tests/pycarl/formula/test_constraint.py	Strengthens constraint tests.
tests/pycarl/core/test_pycarl_core.py	Removes parser capability check.
tests/pycarl/core/test_polynomial.py	Replaces debug output with assertions.
tests/pycarl/core/test_factorized_polynomial.py	Adds type assertions.
tests/pars/test_model_instantiator.py	Tests generic pars APIs.
tests/dft/test_transformations.py	Tests generic DFT instantiation.
tests/dft/test_dft.py	Tests DFT specialization metadata.
tests/dft/test_dft_simulator.py	Migrates generic simulator usage.
tests/dft/test_analysis.py	Migrates generic builder usage.
tests/configurations.py	Simplifies optional dependency detection.
src/utility/smtsolver.cpp	Adopts smart-holder bindings.
src/utility/shortestPaths.cpp	Adopts smart-holder bindings.
src/utility/json.cpp	Adopts smart-holder bindings.
src/utility/chrono.cpp	Adopts smart-holder bindings.
src/template_binding.h	Implements native template registration.
src/storage/valuation.h	Renames valuation binding entry points.
src/storage/umb.cpp	Adopts smart-holder bindings.
src/storage/state.h	Updates valuation formatting.
src/storage/state.cpp	Adopts smart-holder bindings.
src/storage/scheduler.cpp	Adopts smart-holder bindings.
src/storage/prism.cpp	Adopts smart-holder bindings.
src/storage/model_components.cpp	Adopts smart-holder bindings.
src/storage/memorystructure.cpp	Consolidates typed products.
src/storage/matrix.cpp	Adopts smart-holder bindings.
src/storage/labeling.cpp	Adopts smart-holder bindings.
src/storage/geometry.cpp	Adopts smart-holder bindings.
src/storage/expressions.cpp	Adds string expression support.
src/storage/distribution.cpp	Adopts smart-holder bindings.
src/storage/decomposition.cpp	Adopts smart-holder bindings.
src/storage/dd.h	Splits typed DD registration.
src/storage/dd.cpp	Generalizes typed ADD bindings.
src/storage/choiceorigins.cpp	Adopts smart-holder bindings.
src/storage/bitvector.cpp	Exposes additional BitVector operations.
src/pycarl/typed_parse/parser.h	Removes carl-parser wrapper.
src/pycarl/typed_parse/parser.cpp	Removes carl-parser implementation.
src/pycarl/typed_formula/formula.cpp	Adopts smart-holder bindings.
src/pycarl/typed_formula/constraint.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/term.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/rationalfunction.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/rational.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/polynomial.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/interval.h	Adopts smart-holder bindings.
src/pycarl/typed_core/integer.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/factorizedrationalfunction.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/factorizedpolynomial.cpp	Adopts smart-holder bindings.
src/pycarl/typed_core/factorization.cpp	Adopts smart-holder bindings.
src/pycarl/mod_typed_parse.cpp	Removes native typed parser module.
src/pycarl/mod_parse.cpp	Removes native parser module.
src/pycarl/core/variable.cpp	Adopts smart-holder bindings.
src/pycarl/core/monomial.cpp	Adopts smart-holder bindings.
src/pomdp/transformations.cpp	Updates ownership and Storm API usage.
src/pomdp/tracker.cpp	Adopts smart-holder bindings.
src/pomdp/quantitative_analysis.cpp	Adopts smart-holder bindings.
src/pomdp/qualitative_analysis.cpp	Adopts smart-holder bindings.
src/pomdp/memory.cpp	Adopts smart-holder bindings.
src/pomdp/generator.cpp	Adopts smart-holder bindings.
src/pars/pla.cpp	Updates Storm includes and holders.
src/pars/pars.cpp	Adopts smart-holder bindings.
src/pars/model_instantiator.h	Declares typed registrations.
src/mod_storage.cpp	Registers generalized valuations and DDs.
src/mod_pars.cpp	Registers pars specializations.
src/mod_info.cpp	Adopts smart-holder bindings.
src/mod_dft.cpp	Registers DFT specializations.
src/gspn/gspn.cpp	Adopts smart-holder bindings.
src/gspn/gspn_io.cpp	Adopts smart-holder bindings.
src/dft/transformations.cpp	Registers generic DFT instantiator.
src/dft/simulator.h	Simplifies typed declaration.
src/dft/simulator.cpp	Registers generic simulators.
src/dft/module.cpp	Adopts smart-holder bindings.
src/dft/io.cpp	Uses overloaded generic exports.
src/dft/dft.h	Simplifies typed declaration.
src/dft/dft.cpp	Registers generic DFT classes.
src/dft/dft_state.h	Simplifies typed declaration.
src/dft/dft_state.cpp	Registers states and overloaded conversions.
src/dft/dft_elements.h	Simplifies typed declaration.
src/dft/dft_elements.cpp	Registers generic element classes.
src/dft/analysis.h	Simplifies typed declaration.
src/dft/analysis.cpp	Exposes overloaded generic analysis APIs.
src/core/transformation.cpp	Consolidates typed transformations.
src/core/simulator.cpp	Adopts smart-holder bindings.
src/core/multiobjective.cpp	Adopts smart-holder bindings.
src/core/input.cpp	Updates constant parsing API.
src/core/environment.cpp	Adds DD environment bindings.
src/core/counterexample.cpp	Adopts smart-holder bindings.
src/core/bisimulation.cpp	Adds bisimulation options and tolerance.
src/core/analysis.cpp	Adopts smart-holder bindings.
src/common.h	Removes explicit shared-pointer holders.
src/binding_type_index.h	Maps C++ types to template indices.
pyproject.toml	Updates dependencies and build metadata.
MANIFEST.in	Removes obsolete manifest rules.
lib/stormpy/storage/init.py	Adds valuation compatibility shims.
lib/stormpy/pycarl/parse/transformer.py	Implements Lark transformations.
lib/stormpy/pycarl/parse/lark_grammar.lark	Defines parser grammar.
lib/stormpy/pycarl/parse/init.py	Implements optional Lark parser.
lib/stormpy/pycarl/gmp/parse/init.py	Removes native parser exports.
lib/stormpy/pycarl/cln/parse/init.py	Removes native parser exports.
lib/stormpy/pycarl/cln/init.py	Updates CLN guidance.
lib/stormpy/pycarl/init.py	Removes carl-parser capability APIs.
lib/stormpy/pars/init.py	Defines generic pars families.
lib/stormpy/examples/files/pomdp/maze-concise.prism	Renames observables.
lib/stormpy/examples/files/mdp/slipgrid_sketch.nm	Documents parameter bound.
lib/stormpy/dft/simulator.py	Uses generic simulator APIs.
lib/stormpy/dft/init.py	Defines generic DFT families.
lib/stormpy/_version.py	Sets release version.
lib/stormpy/init.py	Adds environments and bisimulation options.
examples/parametric_models/01-parametric-models.py	Demonstrates generic instantiator.
examples/highlevel_models/02-highlevel-models.py	Corrects parameter range.
examples/dfts/03-generic-types.py	Demonstrates generic DFT APIs.
Dockerfile	Removes carl-parser build.
doc/source/installation.md	Documents renamed build options.
doc/source/doc/parametric_models.ipynb	Updates generic pars example.
doc/source/doc/info.ipynb	Adds installation information guide.
doc/source/advanced_topics.md	Links information guide.
CMakeLists.txt	Migrates Storm 1.14 build configuration.
cmake/pycarl_core_config.py.in	Removes parser configuration.
cmake/macros.cmake	Renames configuration variables.
cmake/info_config.py.in	Uses renamed feature variables.
CHANGELOG.md	Documents version 1.14 changes.
.github/workflows/update_storm.yml	Updates checkout and version automation.
.github/workflows/release.yml	Updates checkout action.
.github/workflows/release_docker.yml	Reuses the root Dockerfile.
.github/workflows/formatcheck.yml	Updates checkout action.
.github/workflows/formatapply.yml	Updates checkout action.
.github/workflows/Dockerfile.stable	Removes carl-parser build.
.github/workflows/Dockerfile.release	Removes duplicate Dockerfile.
.github/workflows/Dockerfile.fetch	Removes duplicate Dockerfile.
.github/workflows/create_wheel.yml	Modernizes wheel build workflow.

Review details

• Files reviewed: 28/28 changed files
• Comments generated: 0
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Copilot]

🟡 Changes recommended

The keyword deduction path rejects DFT(dft=...), and some pars tests still reference removed bindings.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Review details

• Files reviewed: 28/28 changed files
• Comments generated: 2
• Review effort level: Balanced

[Copilot]

🔵 Needs a closer look

The broad cross-language API redesign and intentional compatibility changes warrant final human review.

Review details

• Files reviewed: 29/29 changed files
• Comments generated: 0 new
• Review effort level: Balanced

[volkm]

Overall, it looks really great. It is a very cool idea to integrate templating and will make bindings for templated classes so much easier and nicer.

I have a couple of comments, but mostly special cases.
I would suggest to add some guideline on how to properly write these templated bindings.

[linusheck]

Build currently fails because of the ExtendedNumber mismatch. I won't fix this for now.

[sjunges]

Very nitpicky. I like the generic way, but it is a bit annoying that we have to write stormpy.ModelType.DTMC rather than just DTMC or stormpy.DTMC.

[sjunges]

Not sure that I would use examples for this... to some degree, we would want people to write the non-readable aliases. BUt I also dont know where else to put it. Maybe part of it is a test?

[sjunges]

should this be included in the helpers? We need it basically everywhere?

[sjunges]

Great work, just a small number of nitpicks.