Move core module to generic template bindings

[linusheck]

Move core to the new generic system (#449).

[Copilot]

🟡 Changes recommended

Sparse interval model checking can request unregistered CheckTask specializations.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Migrates core bindings from suffix-based APIs to generic template bindings with updated dispatch, tests, and examples.

Changes:

• Adds generic C++ template registrations and Python wrappers.
• Updates model checking, transformations, simulators, and result APIs.
• Refreshes tests and examples for parameterized types.

File summaries

File	Summary
tests/storage/test_maximal_end_components.py	Updates uncertainty bindings.
tests/pars/test_parametric.py	Updates parametric result types.
tests/pars/test_model_instantiator.py	Updates task and result types.
tests/core/test_transformation.py	Updates transformation bindings.
tests/core/test_modelchecking.py	Updates model-checking bindings.
tests/core/test_core_templates.py	Adds generic binding coverage.
src/storage/matrix.cpp	Consolidates topological-sort overloads.
src/storage/dd.cpp	Shares DD type metadata.
src/mod_core.cpp	Registers generic core bindings.
src/core/valuetype.cpp	Defines DD type metadata.
src/core/transformation.h	Supports generic transformations.
src/core/transformation.cpp	Registers generic transformations.
src/core/simulator.h	Supports generic simulators.
src/core/simulator.cpp	Registers generic simulators.
src/core/result.h	Supports generic result types.
src/core/result.cpp	Registers generic result classes.
src/core/multiobjective.h	Supports generic multiobjective checking.
src/core/multiobjective.cpp	Registers generic multiobjective checking.
src/core/modelchecking.h	Supports generic model-checking types.
src/core/modelchecking.cpp	Registers generic tasks and engines.
src/core/counterexample.cpp	Registers generic counterexample classes.
src/core/core.cpp	Migrates builders, masks, and exports.
src/core/bisimulation.cpp	Consolidates bisimulation overloads.
src/core/analysis.cpp	Registers generic constraint collection.
lib/stormpy/storage/__init__.py	Adds model type deduction.
lib/stormpy/simulator.py	Uses generic simulator bindings.
lib/stormpy/__init__.py	Adds generic APIs and dispatch.
examples/building_models/04-building-models.py	Updates action-mask usage.

Review details

• Files reviewed: 28/28 changed files
• Comments generated: 1
• Review effort level: Lite

---

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

[Copilot]

🟡 Changes recommended

Exact symbolic model checking currently lacks a registered Rational DD specialization.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (1)

lib/stormpy/init.py:548

• The exact symbolic case is mapped to CheckTask[Rational], but the C++ bindings register _model_checking_hybrid_engine only for double and RationalFunction (src/core/modelchecking.cpp:171-175). Calling this with an exact symbolic model therefore cannot resolve an overload; reject that combination explicitly or provide the missing exact specialization.

    formula = property.raw_formula if isinstance(property, Property) else property
    value_type = RationalFunction if model.supports_parameters else Rational if model.is_exact else float
    task = CheckTask[value_type](formula, only_initial_states)
    return _core._model_checking_hybrid_engine(model, task, environment=environment)

• Files reviewed: 28/28 changed files
• Comments generated: 1
• Review effort level: Lite

[Copilot]

🟡 Changes recommended

Generic dispatch lacks registered overloads for exact and interval model types, causing unsupported calls to fail without a deliberate error.

Get a fresh assessment by requesting another Copilot review.

Review details

• Files reviewed: 28/28 changed files
• Comments generated: 1
• Review effort level: Lite

[Copilot]

🟡 Changes recommended

Critical DD enum incompatibility and unsupported interval-model dispatch must be resolved.

Get a fresh assessment by requesting another Copilot review.

Review details

Suppressed comments (2)

lib/stormpy/init.py:680

• The generic call now also receives interval-model matrices, but _get_reachable_states is registered only for double, RationalNumber, and RationalFunction in define_modelchecking_mdefs; there is no Interval or RationalInterval overload. Consequently get_reachable_states(interval_model, ...) fails at pybind overload resolution instead of reporting the unsupported operation. Please reject uncertainty models here (or register the missing specializations) before forwarding the call.

    return _core._get_reachable_states(model, initial_states, constraint_states, target_states, maximal_steps, choice_filter)

lib/stormpy/init.py:693

• This dispatch does not exclude interval models: compute_expected_number_of_visits only rejects parametric models, while _compute_expected_number_of_visits is registered only for double and RationalNumber. Calling it with an interval model therefore reaches a missing pybind overload. Add the same explicit uncertainty-model rejection used by the surrounding APIs, or bind the interval implementations if they are intended to be supported.

    return _core._compute_expected_number_of_visits(environment, model)

• Files reviewed: 28/28 changed files
• Comments generated: 1
• Review effort level: Lite

[Copilot]

🟢 Approval recommended

All reviewed changes are covered and no unresolved blocking issues were identified.

Review details

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

[volkm]

In general, it looks great. Thanks for the effort.
I have some comments, for example I think we could also add bindings for exact symbolic models.