Changes to Storm for revised belief exploration by AlexBork · Pull Request #1028 · stormchecker/storm

AlexBork · 2026-08-18T14:05:55Z

This PR contains changes to Storm outside Storm-POMDP for the revised belief exploration implementation, see PR #1004.

Transformer for transition-based to action-based rewards by inserting intermediate states
Transformer for ValueTypes of sparse models
Getter for optional time bound in BoundedUntilFormula

# Conflicts: # src/storm/logic/BoundedUntilFormula.cpp

sjunges · 2026-08-25T19:43:23Z

+    }
+    switch (inputModel->getType()) {
+        case storm::models::ModelType::Dtmc:
+            return std::make_shared<storm::models::sparse::Dtmc<double>>(storm::models::sparse::Dtmc<double>(convertedComponents));


this swtich case is extremely ugly. Is this the standard way to do this? @tquatmann ?

There is buildModelFromComponents in storm/utility/builder.h.

We still need some switch case like this for the model-specific components (exit rates for MAs, player data for SMG etc

sjunges · 2026-08-25T19:45:39Z

Thanks for the changes. I have two more nitpicky comments and would love to get @tquatmann input on the case black.

AlexBork · 2026-08-26T14:35:06Z

I added instantiations for interval models in the transformer; this required a rework of how the different, unique reward vectors are stored and identified. I decided to to implement a potentially slower, but more readable solution. I don't think this should be a bottleneck.

tquatmann

Thanks! After looking into my comments, this PR should be good to go imo.

tquatmann · 2026-09-04T08:47:35Z

+        if (!convertedComponents.transitionMatrix.isProbabilistic(precision)) {
+            convertedComponents.transitionMatrix.divideRowsInPlace(convertedComponents.transitionMatrix.getRowSumVector());
+        }


imo, this should rather go through each row individually, compute the row sum and (if necessary) scale the matrix values.

Currently, this unnecessarily allocates memory for the entire rowSumVector and also touches matrix rows that are actually precise enough.

tquatmann · 2026-09-04T08:51:43Z

+            std::vector<double> resultVector;
+            resultVector.reserve(rewardModel.getStateRewardVector().size());
+            for (auto const& oldValue : rewardModel.getStateRewardVector()) {
+                resultVector.push_back(storm::utility::convertNumber<double>(oldValue));
+            }
+            optionalStateRewardVector = resultVector;


Can be simplified to

Suggested change

std::vector<double> resultVector;

resultVector.reserve(rewardModel.getStateRewardVector().size());

for (auto const& oldValue : rewardModel.getStateRewardVector()) {

resultVector.push_back(storm::utility::convertNumber<double>(oldValue));

}

optionalStateRewardVector = resultVector;

optionalStateRewardVector = storm::utility::vector::convertNumericVector<double>(rewardModel.getStateRewardVector());

(same below)

tquatmann · 2026-09-04T08:55:34Z

+    }
+    switch (inputModel->getType()) {
+        case storm::models::ModelType::Dtmc:
+            return std::make_shared<storm::models::sparse::Dtmc<double>>(storm::models::sparse::Dtmc<double>(convertedComponents));


There is buildModelFromComponents in storm/utility/builder.h.

We still need some switch case like this for the model-specific components (exit rates for MAs, player data for SMG etc

tquatmann · 2026-09-04T09:39:02Z

+            std::vector<double> resultVector;
+            resultVector.reserve(ctmc->getExitRateVector().size());
+            for (auto const& oldValue : ctmc->getExitRateVector()) {
+                resultVector.push_back(storm::utility::convertNumber<double>(oldValue));
+            }
+            convertedComponents.exitRates = resultVector;


Suggested change

std::vector<double> resultVector;

resultVector.reserve(ctmc->getExitRateVector().size());

for (auto const& oldValue : ctmc->getExitRateVector()) {

resultVector.push_back(storm::utility::convertNumber<double>(oldValue));

}

convertedComponents.exitRates = resultVector;

We provide the rates in the transition matrix. A dedicated exit rate vector should not be set and will be ignored in this case.
We do need to set rateTransitions = true to indicate that the transitionMatrix contains rates, not probabilities.

tquatmann · 2026-09-04T09:50:06Z

+                models::sparse::StochasticTwoPlayerGame<double>(convertedComponents));
+        }
+        default:
+            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException,


Suggested change

STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException,

STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,

IllegalArgumentTypeException is more of a storm::settings thing.

tquatmann · 2026-09-04T10:01:13Z

+                if (oldRewardModel.hasStateRewards()) {
+                    rewValue += oldRewardModel.getStateReward(oldState);
+                }


For continuous time models, state rewards are earned over time. Collapsing them together with the action rewards like this is usually incorrect. However, for discrete-time models, it's probably convenient to merge the rewards.

I suggest this change here:

Suggested change

if (oldRewardModel.hasStateRewards()) {

rewValue += oldRewardModel.getStateReward(oldState);

}

if (originalModel->isDiscreteTimeModel() && oldRewardModel.hasStateRewards()) {

rewValue += oldRewardModel.getStateReward(oldState);

}

and below something like

std::optional<std::vector<ValueType>> newStateRewards; if (originalModel->isContinuousTimeModel() && oldRewardModel.hasStateRewards()) { newStateRewards.emplace(numStates, storm::utility::zero<ValueType>()) for (uint64_t origState = 0; origState < originalModel->getNumberOfStates(); ++origState) { uint64_t const newState = originalToNewIndex[origState]; newStateRewards.value()[newState] = oldRewardModel.getStateReward(oldState); } } RewardModelType newRewardModel(newStateRewards, std::move(newActionRewardVector));

tquatmann · 2026-09-04T10:05:13Z

+    auto const& transitions = originalModel->getTransitionMatrix();
+    for (uint64_t row = 0; row < transitions.getRowCount(); ++row) {
+        rewardTransitionIterator.forEachRowEntry(
+            row, true, [&incomingRewards](uint64_t column, RewardValueType, detail::MultiRewardVector<RewardValueType> const& rewards) {


Suggested change

row, true, [&incomingRewards](uint64_t column, RewardValueType, detail::MultiRewardVector<RewardValueType> const& rewards) {

row, true, [&incomingRewards](uint64_t column, ValueType, detail::MultiRewardVector<RewardValueType> const& rewards) {

AlexBork · 2026-09-04T12:22:38Z

Thanks for the comments, I have now added the requested changes. For the switch-case in the ToDoubleTransformer, I use a single buildModelFromComponents now, but opted to still include all cases explicitly. This way, if new model types are added, the default is to throw an exception instead of silently accepting it, which may lead to erroneous behaviour.

tquatmann

LGTM! Just a very small nitpick.

Changes to Storm for revised belief exploration

562198b

AlexBork mentioned this pull request Aug 18, 2026

Revised POMDP belief exploration #1004

Draft

AlexBork added this to the 1.15 milestone Aug 18, 2026

AlexBork added the ready for review label Aug 19, 2026

sjunges reviewed Aug 19, 2026

View reviewed changes

Comment thread src/storm/logic/BoundedUntilFormula.cpp Outdated

sjunges reviewed Aug 19, 2026

View reviewed changes

Comment thread src/storm/transformer/SparseModelValueTypeTransformer.h Outdated

sjunges reviewed Aug 19, 2026

View reviewed changes

Comment thread src/storm/transformer/TransitionToActionRewardTransformer.h

AlexBork added 10 commits August 20, 2026 12:39

Change boost::optional to std::optional in BoundedUntilFormula

9461797

Add comment about conversion to std::optional

51f9fd0

Merge branch 'bounded-until-optional' into revbel-storm

89a1fb5

Adjust get*BoundAsOptionalTimeBound

7351f26

Change valuetype transformer to only rational-to-double

9adb1f1

Add potential normalisation

f31dd95

Change precision to be an input parameter

d3d2ce4

Add tests

aac224e

Merge branch 'master' into revbel-storm

6573133

# Conflicts: # src/storm/logic/BoundedUntilFormula.cpp

Remove normalisation test

8347494

sjunges reviewed Aug 25, 2026

View reviewed changes

Comment thread src/storm/transformer/TransitionToActionRewardTransformer.cpp

Add interval instantiations

c5ea70e

Add test cases for intervals

8a42f9d

tquatmann reviewed Sep 4, 2026

View reviewed changes

incorporate review comments

ea847c1

tquatmann approved these changes Sep 4, 2026

View reviewed changes

Comment thread src/storm/transformer/TransitionToActionRewardTransformer.cpp Outdated

Fix state rewards initialization in transformer

73fcfd4

tquatmann mentioned this pull request Sep 4, 2026

merging of equivalent states as preprocessing #1016

Open

tquatmann merged commit 9429df0 into stormchecker:master Sep 4, 2026
23 checks passed

	STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException,
	STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,

	row, true, [&incomingRewards](uint64_t column, RewardValueType, detail::MultiRewardVector<RewardValueType> const& rewards) {
	row, true, [&incomingRewards](uint64_t column, ValueType, detail::MultiRewardVector<RewardValueType> const& rewards) {

Uh oh!

Conversation

AlexBork commented Aug 18, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

sjunges commented Aug 25, 2026

Uh oh!

AlexBork commented Aug 26, 2026

Uh oh!

tquatmann 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!

AlexBork commented Sep 4, 2026

Uh oh!

tquatmann left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants