merging of equivalent states as preprocessing by tquatmann · Pull Request #1016 · stormchecker/storm

tquatmann · 2026-08-14T20:58:49Z

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

Relates to #996

* 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

…merge # Conflicts: # src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp # src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp # src/storm/transformer/GoalStateMerger.cpp

…merge

Copilot

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 GoalStateMerger to merge equivalent states based on a supported input formula and expose it via API/CLI preprocessing.
Add a new CLI option --merge-equivalent-states and 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>

…merge

volkm

LGTM.

I only have minor mostly code-style comments. Feel free to ignore some of them.

volkm · 2026-09-08T07:42:55Z

 }

+/*!
+ * Identifies states of the given model and formula that are equivalent and merges them into a single state, yielding a (potentially smaller) model on which the


Suggested change

* Identifies states of the given model and formula that are equivalent and merges them into a single state, yielding a (potentially smaller) model on which the

* Identifies states of the given model that are equivalent w.r.t. to the given formula and merges them into a single state, yielding a (potentially smaller) model on which the

volkm · 2026-09-08T07:44:28Z

+template<typename ValueType>
+std::shared_ptr<storm::models::sparse::Model<ValueType>> mergeEquivalentStatesForFormula(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model,
+                                                                                         storm::logic::Formula const& formula) {
+    // storm::transformer::GoalStateMerger is only instantiated for double, rational number, and rational function value types.


If the instantiations are limited, maybe move the function to a cpp and explicitly instantiate it. This would avoid including RationalFunctionForward (which might be slightly better for build times?).

volkm · 2026-09-08T07:44:57Z

+        if (model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) ||
+            model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) {


Why not throw a NotSupportedException instead of returning a nullptr?

volkm · 2026-09-08T07:49:31Z

+        } else if (auto mergedModel = storm::api::mergeEquivalentStatesForFormula<ValueType>(result.first, *formulas.front())) {
+            STORM_LOG_INFO("Merged target/sink states relevant for the considered property '" << *formulas.front() << "'.");


I know this works, but I personally dislike assignments in conditions. Could we maybe explicitly check for the nullptr?

volkm · 2026-09-08T07:52:17Z

+ * * (if rewardModelName is given) the reward collected at the state is constant.
+ *
+ * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given).
+ * Labelings of eliminated states will be lost


This contradictory when elimination only happens if no state label is defined. Do you mean choice labels here?

volkm · 2026-09-08T08:28:00Z

+        bool const ok = modelVal == 0.0 ? mergedVal == 0 : std::abs((mergedVal - modelVal) / modelVal) <= 1e-6;
+        EXPECT_TRUE(ok) << "Relative difference between original model result (" << modelVal << ") and merged model result (" << mergedVal
+                        << ") is too high.\nFailed for model " << prismModelFile << " and formula " << *formulas.front()
+                        << " (dropUnreachableFromInit=" << dropUnreachableFromInit << ").";


You could also distinguish between modelVal == 0.0 and else, and then use EXPECT_NEAR(mergedVal, modelVal, 1e-6) (but this uses absolute precision)

volkm · 2026-09-08T08:33:08Z

+std::optional<uint64_t> representative(storm::storage::BitVector const& b) {
+    if (auto it = b.begin(); it != b.end()) {
+        return *it;
+    }


Maybe use getNextSetIndex(0)? Or check for empty and otherwise return b.begin()? The current versions is not immediately understandable.

volkm · 2026-09-08T08:35:43Z

+    if (originalModel.hasStateValuations()) {
+        std::vector<uint64_t> newToOldStateIndices(maybeStates.begin(), maybeStates.end());
+        if (result.first.targetState.has_value()) {
+            STORM_LOG_ASSERT(result.first.targetState.value() == newToOldStateIndices.size(), "unexpected position of target state.");


Suggested change

STORM_LOG_ASSERT(result.first.targetState.value() == newToOldStateIndices.size(), "unexpected position of target state.");

STORM_LOG_ASSERT(result.first.targetState.value() == newToOldStateIndices.size(), "Unexpected position of target state.");

volkm · 2026-09-08T08:35:53Z

+            newToOldStateIndices.push_back(representativeTargetState.value_or(*targetStates.begin()));
+        }
+        if (result.first.sinkState.has_value()) {
+            STORM_LOG_ASSERT(result.first.sinkState.value() == newToOldStateIndices.size(), "unexpected position of sink state.");


Suggested change

STORM_LOG_ASSERT(result.first.sinkState.value() == newToOldStateIndices.size(), "unexpected position of sink state.");

STORM_LOG_ASSERT(result.first.sinkState.value() == newToOldStateIndices.size(), "Unexpected position of sink state.");

volkm · 2026-09-08T08:39:03Z

+    std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
+    if (!originalModel.isNondeterministicModel()) {
+        statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, *phiStates, *psiStates);
+    } else if (std::optional<bool> const minimizing = isMinimizing(formula); !minimizing.has_value()) {


!isMinimizing(formula).has_value() would not work?

tquatmann commented Aug 14, 2026

View reviewed changes

Comment thread src/storm-pars/transformer/SparseParametricModelSimplifier.cpp Outdated

Fix unused variable.

588933c

tquatmann added this to the 1.15 milestone Aug 17, 2026

tquatmann added 2 commits September 4, 2026 16:42

Fix according to linusheck

bbdd452

Merge remote-tracking branch 'origin/master' into feature/goal-state-…

016abbd

…merge # Conflicts: # src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp # src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp # src/storm/transformer/GoalStateMerger.cpp

tquatmann added the ready for review label Sep 4, 2026

tquatmann added 2 commits September 4, 2026 17:31

Revised treatment of bounded until formula

1e5898d

Merge remote-tracking branch 'origin/master' into feature/goal-state-…

e05bc45

…merge

tquatmann requested a balanced review from Copilot September 4, 2026 18:02

Copilot AI reviewed Sep 4, 2026

View reviewed changes

Copilot started reviewing on behalf of tquatmann September 4, 2026 18:20 View session

tquatmann and others added 5 commits September 4, 2026 21:38

Update action rewards in reward model insertion

e0ec65f

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot Feedback.

b57ac20

Merge remote-tracking branch 'origin/master' into feature/goal-state-…

3cd1094

…merge

fix bracket.

fcfe5b2

Fixes from claude review

5eb1e3a

volkm approved these changes Sep 8, 2026

View reviewed changes

	* Identifies states of the given model and formula that are equivalent and merges them into a single state, yielding a (potentially smaller) model on which the
	* Identifies states of the given model that are equivalent w.r.t. to the given formula and merges them into a single state, yielding a (potentially smaller) model on which the

		if (model->isOfType(storm::models::ModelType::Dtmc) \|\| model->isOfType(storm::models::ModelType::Ctmc) \|\|
		model->isOfType(storm::models::ModelType::Mdp) \|\| model->isOfType(storm::models::ModelType::MarkovAutomaton)) {

		} else if (auto mergedModel = storm::api::mergeEquivalentStatesForFormula<ValueType>(result.first, *formulas.front())) {
		STORM_LOG_INFO("Merged target/sink states relevant for the considered property '" << *formulas.front() << "'.");

	STORM_LOG_ASSERT(result.first.targetState.value() == newToOldStateIndices.size(), "unexpected position of target state.");
	STORM_LOG_ASSERT(result.first.targetState.value() == newToOldStateIndices.size(), "Unexpected position of target state.");

	STORM_LOG_ASSERT(result.first.sinkState.value() == newToOldStateIndices.size(), "unexpected position of sink state.");
	STORM_LOG_ASSERT(result.first.sinkState.value() == newToOldStateIndices.size(), "Unexpected position of sink state.");

Uh oh!

Conversation

tquatmann commented Aug 14, 2026

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

volkm left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants