merging of equivalent states as preprocessing - #1016
Merged
tquatmann merged 12 commits intoSep 11, 2026
Merged
Conversation
* extends the GoalStateMerger so that it can now merge states based on an input formula (e.g. all prob0/prob1 states * adds a CLI option --merge-equivalent-states to invoke that as a preprocessing * Simplifies SparseParametricModelSimplifier by calling the new GoalStateMerger
tquatmann
commented
Aug 14, 2026
…merge # Conflicts: # src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp # src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp # src/storm/transformer/GoalStateMerger.cpp
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Pull request overview
Extends goal/sink state merging to work as a formula-driven preprocessing step and consolidates parametric model simplification around the updated GoalStateMerger.
Changes:
- Generalize
GoalStateMergerto merge equivalent states based on a supported input formula and expose it via API/CLI preprocessing. - Add a new CLI option
--merge-equivalent-statesand wire it into the preprocessing pipeline. - Consolidate parametric DTMC/MDP simplifiers into
SparseParametricModelSimplifier, updating tests and call sites accordingly.
Reviewed changes
Copilot reviewed 29 out of 29 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| src/test/storm/transformer/GoalStateMergerTest.cpp | Adds regression tests validating formula-driven merging preserves results. |
| src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp | Switches to consolidated SparseParametricModelSimplifier. |
| src/storm/utility/graph.cpp | Adds missing template instantiation for performProb1A (rational reward model). |
| src/storm/transformer/GoalStateMerger.h | Refactors merger to be value-type based and adds mergeForFormula. |
| src/storm/transformer/GoalStateMerger.cpp | Implements formula-driven merging and model-component rebuild incl. valuations/labels/origins. |
| src/storm/settings/modules/TransformationSettings.h | Declares new merge-equivalent-states setting. |
| src/storm/settings/modules/TransformationSettings.cpp | Registers new CLI option and getter. |
| src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp | Adapts to new GoalStateMerger<ValueType> result model type. |
| src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp | Adapts to new GoalStateMerger<ValueType> result model type. |
| src/storm/api/transformation.h | Adds mergeEquivalentStatesForFormula API helper around GoalStateMerger. |
| src/storm-pars/transformer/SparseParametricModelSimplifier.h | Removes virtual interface pieces; consolidates simplifier roles. |
| src/storm-pars/transformer/SparseParametricModelSimplifier.cpp | Re-implements simplification pipeline using GoalStateMerger + eliminations. |
| src/storm-pars/transformer/SparseParametricMdpSimplifier.h | Removed (functionality consolidated). |
| src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp | Removed (functionality consolidated). |
| src/storm-pars/transformer/SparseParametricDtmcSimplifier.h | Removed (functionality consolidated). |
| src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp | Removed (functionality consolidated). |
| src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp | Uses consolidated simplifier instead of DTMC/MDP variants. |
| src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp | Uses consolidated simplifier instead of MDP variant. |
| src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp | Uses consolidated simplifier instead of DTMC variant. |
| src/storm-pars-cli/storm-pars.cpp | Uses consolidated simplifier in CLI model simplification path. |
| src/storm-pars-cli/sampling.h | Removes includes of removed DTMC/MDP simplifiers. |
| src/storm-cli-utilities/model-handling.h | Wires --merge-equivalent-states preprocessing before bisimulation. |
💡 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>
volkm
approved these changes
Sep 8, 2026
volkm
left a comment
volkm
left a comment
Contributor
There was a problem hiding this comment.
LGTM.
I only have minor mostly code-style comments. Feel free to ignore some of them.
Contributor
Author
|
Thanks for the review! I'm overusing init-statements in |
Contributor
|
Might also just be me not understanding two things in one line ;) |
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.
Relates to #996