Migrate dft and pars to experimental new generic handling - #445
Migrate dft and pars to experimental new generic handling#445linusheck wants to merge 2 commits into
Conversation
There was a problem hiding this comment.
🟡 Changes recommended
It introduces breaking public API changes (notably removed/renamed DFT export and concrete-type entry points) without compatibility aliases, and includes a small test hygiene issue (unused import).
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Pull request overview
This PR introduces an experimental generic “template family” mechanism for Stormpy’s Python bindings, enabling subscriptable access to compiled C++ template specializations (e.g., DFT[float]) and optional constructor-based deduction, and migrates DFT and parametric instantiation (pars) APIs/tests/docs to use it.
Changes:
- Added C++ infrastructure to name and register template specializations and expose them to Python via a
_template_instantiationsregistry. - Migrated DFT and pars bindings to register specializations under generic families and updated Python packages to expose them via
TemplateClass. - Updated tests, examples, and documentation to use the new generic APIs (subscriptions and deduction).
File summaries
| File | Description |
|---|---|
| tests/pars/test_model_instantiator.py | Updates tests to use ModelInstantiator[...] and ModelInstantiationChecker[...]. |
| tests/dft/test_transformations.py | Updates DFT instantiator test to use the new generic specialization mapping. |
| tests/dft/test_dft.py | Adds coverage for generic DFT typing and updates parametric DFT assertions. |
| tests/dft/test_dft_simulator.py | Switches simulator usage to generic DFTSimulator and unified as_be/as_dependency. |
| tests/dft/test_analysis.py | Migrates explicit model builder tests to generic ExplicitDFTModelBuilder[...] / deduction. |
| src/template_binding.h | Adds generic registration utilities for template families/specializations. |
| src/pars/model_instantiator.cpp | Migrates pars instantiator/checker bindings to generic template registration. |
| src/mod_dft.cpp | Updates DFT module init to call typed binders without suffix naming. |
| src/dft/transformations.cpp | Registers DFTInstantiator as a generic template specialization. |
| src/dft/simulator.h | Updates typed simulator binder signature for generic registration. |
| src/dft/simulator.cpp | Registers DFTSimulator specializations via the template registry. |
| src/dft/io.cpp | Changes export binding names to overload export_dft_json_* across value types. |
| src/dft/dft.h | Updates typed DFT binder signature for generic registration. |
| src/dft/dft.cpp | Registers DFT specializations via the template registry and adds copy construction. |
| src/dft/dft_state.h | Updates typed DFTState binder signature for generic registration. |
| src/dft/dft_state.cpp | Registers DFTState via the template registry and unifies as_be/as_dependency via overloads. |
| src/dft/dft_elements.h | Updates typed DFT element binder signature for generic registration. |
| src/dft/dft_elements.cpp | Registers DFTElement/DFTBE/DFTDependency specializations via the template registry. |
| src/dft/analysis.h | Updates typed analysis binder signature for generic registration. |
| src/dft/analysis.cpp | Registers ExplicitDFTModelBuilder and overloads analysis functions by value type. |
| src/binding_type_index.h | Adds stable Python-key/native-label generation for template parameter tuples. |
| lib/stormpy/pars/init.py | Exposes pars template families via TemplateClass and removes the custom wrapper class. |
| lib/stormpy/dft/simulator.py | Updates high-level simulator wrapper to use generic simulator and unified accessors. |
| lib/stormpy/dft/init.py | Exposes DFT template families via TemplateClass and removes type-dispatch wrappers. |
| lib/stormpy/_template.py | Introduces the Python runtime TemplateClass that provides subscription and deduction. |
| examples/parametric_models/01-parametric-models.py | Updates example to use ModelInstantiator[...]. |
| examples/dfts/03-generic-types.py | Adds a new example demonstrating explicit and inferred generic specializations. |
| doc/source/doc/parametric_models.ipynb | Updates notebook snippet to use ModelInstantiator[...]. |
Review details
- Files reviewed: 28/28 changed files
- Comments generated: 3
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| @@ -1,4 +1,5 @@ | |||
| import stormpy | |||
| import pytest | |||
| 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")); |
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:This replaces the custom Python wrapper functions that currently check input types.