Conversation
Contributor
Author
|
Here's a quick performance comparison between old (current master) and new (this PR) implementation generated using this script benchmark.py |
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…of all occurring labels.
There was a problem hiding this comment.
🟡 Changes recommended
One or more issues must be addressed before approval.
Get a fresh assessment by requesting another Copilot review.
Pull request overview
Replaces the legacy sparse bisimulation engine with a transformer-based implementation supporting MAs, rewards, tolerances, choice metadata, weak bisimulation, and quotient mappings.
Changes:
- Adds new partition-refinement, signature, quotient, and mapping infrastructure.
- Migrates APIs, CLI settings, formula traversal, and callers.
- Replaces legacy tests with comprehensive transformer-based coverage.
File summaries
| File | Description |
|---|---|
| src/test/storm/transformer/bisimulation/PartitionTest.cpp | Updated as part of this pull request. |
| src/test/storm/transformer/bisimulation/BisimulationTestHelper.h | Updated as part of this pull request. |
| src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp | Updated as part of this pull request. |
| src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp | Updated as part of this pull request. |
| src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp | Updated as part of this pull request. |
| src/test/storm/logic/TraverseFormulaVisitorTest.cpp | Updated as part of this pull request. |
| src/test/storm-pars/transformer/BinaryDtmcTransformerTest.cpp | Updated as part of this pull request. |
| src/test/storm-pars/transformer/BigStepTest.cpp | Updated as part of this pull request. |
| src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp | Updated as part of this pull request. |
| src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp | Updated as part of this pull request. |
| src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/WeakBisimulationData.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/WeakBisimulationData.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/SplitterBasedRefinement.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/SparseAccumulator.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/SparseAccumulator.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Signatures.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/SignatureBasedRefinement.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/SignatureBasedRefinement.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/QuotientData.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/QuotientData.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Quotient.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Quotient.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/PreservationInformation.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Partition.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Options.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Options.cpp | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Initialization.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/BisimulationType.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Bisimulation.h | Updated as part of this pull request. |
| src/storm/transformer/bisimulation/Bisimulation.cpp | Updated as part of this pull request. |
| src/storm/storage/sparse/ChoiceOrigins.h | Updated as part of this pull request. |
| src/storm/storage/sparse/ChoiceOrigins.cpp | Updated as part of this pull request. |
| src/storm/storage/dd/bisimulation/PreservationInformation.h | Updated as part of this pull request. |
| src/storm/storage/dd/bisimulation/Partition.h | Updated as part of this pull request. |
| src/storm/storage/dd/bisimulation/Partition.cpp | Updated as part of this pull request. |
| src/storm/storage/dd/bisimulation/BisimulationDecomposition.h | Updated as part of this pull request. |
| src/storm/storage/dd/bisimulation/BisimulationDecomposition.cpp | Updated as part of this pull request. |
| src/storm/storage/bisimulation/Partition.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/Partition.cpp | Updated as part of this pull request. |
| src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp | Updated as part of this pull request. |
| src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/DeterministicBlockData.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/DeterministicBlockData.cpp | Updated as part of this pull request. |
| src/storm/storage/bisimulation/Block.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/Block.cpp | Updated as part of this pull request. |
| src/storm/storage/bisimulation/BisimulationType.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/BisimulationDecomposition.h | Updated as part of this pull request. |
| src/storm/storage/bisimulation/BisimulationDecomposition.cpp | Updated as part of this pull request. |
| src/storm/settings/modules/BisimulationSettings.h | Updated as part of this pull request. |
| src/storm/settings/modules/BisimulationSettings.cpp | Updated as part of this pull request. |
| src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp | Updated as part of this pull request. |
| src/storm/modelchecker/AbstractModelChecker.cpp | Updated as part of this pull request. |
| src/storm/logic/TraverseFormulaVisitor.h | Updated as part of this pull request. |
| src/storm/logic/TraverseFormulaVisitor.cpp | Updated as part of this pull request. |
| src/storm/logic/Formula.h | Updated as part of this pull request. |
| src/storm/logic/Formula.cpp | Updated as part of this pull request. |
| src/storm/api/bisimulation.h | Updated as part of this pull request. |
| src/storm-pomdp-cli/storm-pomdp.cpp | Updated as part of this pull request. |
| src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp | Updated as part of this pull request. |
| src/storm-dft/modelchecker/DFTModelChecker.cpp | Updated as part of this pull request. |
| src/storm-cli-utilities/model-handling.h | Updated as part of this pull request. |
Review details
Suppressed comments (4)
src/storm-cli-utilities/model-handling.h:724
- The
graphPreservingargument is now ignored, so the--assume-graph-preserving falsepath no longer switches to the old all-label preservation mode. In that mode, formula-basedFormulaPropositionalpreservation can merge states that differ in labels outside the maximal propositional subformulas, changing the region-analysis model and potentially invalidating the intended non-graph-preserving behavior; usegraphPreservingto selectStateLabelPreservation::All(and retain the existing reward-selection semantics).
return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), options);
src/storm/transformer/bisimulation/Bisimulation.cpp:117
- The new public state/choice mapping result is not exercised by the bisimulation tests: the current tests only inspect quotient sizes and formula values. A regression in representative selection or mapping non-representative MDP choices would therefore go unnoticed even though scheduler translation is a stated feature; add assertions for both state mappings and choice mappings (including deduplicated choices).
src/storm/transformer/bisimulation/Quotient.cpp:141 - The quotient currently drops
stateValuationseven when the input model has them. This loses state-variable metadata used by exporters and downstream transformations; preserve the representative state entries here, consistent withSubsystemBuilderandGoalStateMerger.
src/storm/transformer/bisimulation/Signatures.cpp:127 devidedis misspelled in this newly added comment; it should bedivided.
- Files reviewed: 70/70 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.
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
There was a problem hiding this comment.
🟡 Changes recommended
One or more issues must be addressed before approval.
Get a fresh assessment by requesting another Copilot review.
Review details
Suppressed comments (6)
Previously missed (3) — in code that hasn't changed since the last review.
src/storm-cli-utilities/model-handling.h:724
- The parametric CLI passes
graphPreservinginto this helper, but this call never uses it when constructing the sparse bisimulation options. Consequently--assume-graph-preserving falsehas no effect on this preprocessing path, even though both callers still pass that setting. Please either propagate the setting into the new implementation or remove/update the parameter and callers if the option is intentionally unsupported.
src/storm/transformer/bisimulation/Quotient.cpp:139 - This quotient rebuilds labels and rewards but silently drops
stateValuationswhenever the input model has them. That loses state metadata used by model exporters, schedulers, and counterexamples; other sparse transformations select representative valuations (for exampleGoalStateMerger). Copy the valuations fortoRepresentativeStatehere, or explicitly reject/warn if this transformation is not meant to preserve them.
src/storm/transformer/bisimulation/Signatures.cpp:127 - The comment contains the typo
devided; please correct it todivided.
src/storm/transformer/bisimulation/Partition.h:174
- The documentation should use the plural “sub-blocks” because a proper superblock contains more than one sub-block.
src/storm/transformer/bisimulation/Signatures.cpp:390 - The PR exposes
toQuotientChoiceMapping, but the tests never request or validate it, including the approximate matching path for choices of non-representative states. Since the implementation has separate representative and non-representative mapping logic below, add focused deterministic and MDP tests covering deduplication and tolerance-based matching.
src/test/storm/transformer/bisimulation/PartitionTest.cpp:74 - This comment uses “their” for the singular block and contains an extra space; please correct the grammar.
- Files reviewed: 70/70 changed files
- Comments generated: 2
- Review effort level: Lite
sjunges
reviewed
Sep 12, 2026
sjunges
reviewed
Sep 12, 2026
sjunges
reviewed
Sep 12, 2026
| .build()) | ||
| .build()); | ||
|
|
||
| this->addOption(storm::settings::OptionBuilder(moduleName, toleranceOptionName, true, |
Contributor
There was a problem hiding this comment.
is this now also used for dd-based bisim?
Contributor
Author
There was a problem hiding this comment.
The tolerance is currently sparse only. The help message already mentions this. Should I make this more clear somehow?
dd-bisim does not use any tolerance-based comparison right now.
This example yields some evidence: sparse-bisim correctly yields a quotient with 4 states while dd-bisim yields a quotient with 5 states.
dtmc
module M
s : [0..5] init 0;
[] s=0 -> 0.5: (s'=1) + 0.5: (s'=2);
[] s=1 -> 0.1: (s'=3) + 0.2: (s'=4) + 0.7: (s'=5);
[] s=2 -> 0.3: (s'=3) + 0.7: (s'=5);
[] s>2 -> true;
endmodule
label "target" = s=3 | s=4;
Note that (s=3 and s=4) and (s=1 and s=2) are bisimular, but s=1 and s=2 are split because 0.1+0.2==0.3 doesn't hold in double arithmethic. sparse-bisim with --bisimulation:tolerance 0 has the same problem.
sjunges
reviewed
Sep 12, 2026
| return indexToIdentifier[choiceIndex]; | ||
| } | ||
|
|
||
| std::vector<uint_fast64_t> const& ChoiceOrigins::getIdentifiers() const { |
Contributor
There was a problem hiding this comment.
i see how it is consistent :-)
Contributor
Author
There was a problem hiding this comment.
Yes, this was intentional because we take that vector by reference.
I'd rather keep it this way and globally replace all remaining fast64_t at a convenient time.
sjunges
reviewed
Sep 12, 2026
There was a problem hiding this comment.
🟡 Changes recommended
Critical issues remain in preprocessing, quotient valuation preservation, and tolerance handling.
Get a fresh assessment by requesting another Copilot review.
Review details
Suppressed comments (3)
src/storm/transformer/bisimulation/Bisimulation.cpp:117
- The advertised state/choice mappings are not exercised by the new bisimulation tests: none enables
createQuotientChoiceMappingor checks mappings after choice deduplication/approximate matching. Please add regression tests for deterministic and MDP quotients (including the representative-choice and non-representative-choice paths) so this public result cannot silently regress.
src/storm/transformer/bisimulation/Signatures.cpp:127 - The new comment misspells “divided”; please correct it to keep the explanatory documentation clear.
src/test/storm/transformer/bisimulation/PartitionTest.cpp:74 - This new test comment contains a duplicated space in “their remainder”; please remove the extra space.
- Files reviewed: 70/70 changed files
- Comments generated: 3
- Review effort level: Lite
There was a problem hiding this comment.
🟡 Changes recommended
Approximate choice mappings can be non-injective, preventing reliable quotient-scheduler translation for some equivalent states.
Get a fresh assessment by requesting another Copilot review.
Review details
- Files reviewed: 71/71 changed files
- Comments generated: 1
- Review effort level: Lite
…state) surjective. This is necessary to map quotient model schedulers to the original model.
There was a problem hiding this comment.
Copilot review overview
🔵 Needs a closer look
It replaces the core sparse bisimulation engine across multiple model types and removes the legacy implementation, requiring final human validation.
Review effort: Lite
Findings: None
Resolved since last review (1)
volkm
self-requested a review
September 22, 2026 08:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Completely revised sparse bisimulation implementation.
What's new
tolerance > 0), in particular for MDPs where choices might be "equivalent up to a tolerance".std::sortwas called on a non-total order induced by the ConstantsComparator. There is still an issue with RationalFunction which imo should be handled within carl.Where to start
performBisimulationMinimizationinBisimulation.cppserves as an entry point and goes through the three min steps of bisimulation minimization:Caveats
I deliberately did not port the "measure driven initial partitions", which lump together states with equal value (e.g. prob0/prob1 states for a
P=? [ F "target" ]query). While that could be useful in certain cases, I found that it made the entire procedure significantly more complicated—conceptually (qualitative model checking would be a subtask of bisimulation, which is a preprocessing for model checking...) and code-wise.The functionality has been moved into mergeEquivalentStatesForFormula which can be combined with bisimulation. Hence the combination
--merge-equivalent-states --bisimulationshould be equivalent to the old--bisimulation, except that the new one has to create an intermediate model. #91 is relevant.