Revised POMDP belief exploration - #1004
Draft
AlexBork wants to merge 31 commits into
Draft
Conversation
Contributor
|
What besides SAYNT may depend on the old one? I understand the desire to treat carefully, but I also think it may simplify the merging process significantly if we do hard cut. People that want the old version will need to work with 1.14 and as long as it is clear what features we are loosing, that all seems fine to me. |
Contributor
Author
|
I can't think of anything that depends on the old one besides SAYNT. Featurewise, I think the only significant omission currently is the automated refinement loop for the approximations. I think that needs some conceptual reworking before implementation, so I have omitted it for now. All in all, I would be fine with completely removing the old implementation. As we are reworking SAYNT, there should be no reason for keeping it. |
Contributor
|
Would it make sense to split this PR into one that touches storm and one that only touches storm-pomdp? Also, within storm-pomdp, I was wondering whether some parts of the CLI should actually be moved into their own header/cpp (pomdp-handling.h) or so such that it is a bit clearer where it is just cli handling and where it is configuring the algorithm? |
Contributor
Author
|
I'll split the PR. That definitely makes things more manageable. |
# Conflicts: # src/storm-pomdp/builder/BeliefMdpExplorer.cpp # src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp # src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp # src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp
# Conflicts: # src/storm/logic/BoundedUntilFormula.cpp
tquatmann
pushed a commit
that referenced
this pull request
Sep 4, 2026
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
lukovdm
added a commit
that referenced
this pull request
Sep 7, 2026
In storm infinities in rational numbers are currently encoded as 10^11 (the sentinel). To get rid of this we introduce `ExtendedValue<ValueType>` which contains a value and flags to denote positive and negative infinity. We also introduce a `ExtendedValueType<ValueType>` which gives the `ValueType` if it already supports infinity (doubles) and returns `ExtendedValue<ValueType>` if it does not. This ExtendedValueType is used in any location where it is neccesary to calculate with infinities or on outside facing API endpoints. This mean that for example CheckResults return a vector of ExtendedValueType. Several other ways to store infinities in storm have also been consolidated into ExtendedValueType, the most prominent being `Extremum<ValueType>`. This PR also adds STORM_LOG_DEPRECATED which, in DEBUG mode, prints a deprecation warning once. In RELEASE mode, this macro does nothing. - Tim ## Extremum `Extremum` no longer has two ways to store the value but always goes through ExtendedValueType. This also solves the issue where `Etremum<ValueType>` behaved differently on `Doubles` then on `RationalNumbers`. On doubles if you assign infinity to a just constructed extremum it would still be considerd empty. On rational numbers if you assign "infinity" (think 10^11) to an extremum it would no longer be empty. The old double semantics now work for all value types extremum is instantiated with. **I tried to test and review this but would appreciate an extra set of eyes on this.** ## Performance After running experiments both on multiple areas of storm and more detailed using a reduced set of experiments from the revised practitioners guide no changes more then +1% where found and those were also within the precision of the tests. ## Reviewing I have reviewed all code myself already however I have less understanding of several parts of Storm most importantly: - storm-dft - storm-pars These could use some extra attention during the review. ## Still using the sentinel Several locations have not been done yet. This PR is waiting for #1004 to be merged such that this work can also be applied there. Also I have net been able to figure out how to make ExtendedRational work in the sylvan storm c wrapper. - Decision diagram leaves (all engines: symbolic, hybrid, game-based). The sentinel is written into an ADD constant and compared out of one. DdManager.cpp:68 (getInfinity()), SymbolicDtmcPrctlHelper.cpp:195,204,240, SymbolicMdpPrctlHelper.cpp:320,358, HybridDtmcPrctlHelper.cpp:297,375,379, HybridMdpPrctlHelper.cpp:611,770,774, SymbolicMinMaxLinearEquationSolver.cpp:37, SymbolicGameSolver.cpp:26,28, AbstractAbstractionRefinementModelChecker.cpp:904. Blocked on Sylvan leaf payloads; CUDD is double-only and unaffected. - storm-pomdp belief exploration. Computes with the sentinel rather than only passing it through: BeliefExplorationPomdpModelChecker.cpp:1087,1208,1221,1237,1264,1354,1374,1414. ExtremePOMDPValueBound also carries a parallel isInfinite BitVector (BeliefExplorationBounds.h:56, threaded through BeliefManager.h:97,108). Left alone pending #1004. ## Bridges that exist only until the above are gone When all locations that still use the old sentinel way are gone these methods can be removed. - toSentinel — ExplicitQuantitativeCheckResult.cpp:189 (inside getSentinelValueVector), HybridMdpPrctlModelChecker.cpp:186. - fromSentinel — DD result reads in SymbolicQuantitativeCheckResult.cpp:135,150,177,182,192 and HybridQuantitativeCheckResult.cpp:161,163,181,195,234,237,245,248,256,258; POMDP in BeliefExplorationPomdpModelChecker.cpp:59,70,165,166 and BeliefMdpExplorer.cpp:1089. - getSentinelValueVector — 5 callers in PreprocessingPomdpValueBoundsModelChecker.cpp:104,140,182,203,337 and BeliefMdpExplorer.cpp:923. Returns by value; the calls it replaced could move.
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
2 participants
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.
This PR contains the revised POMDP belief exploration implementation.
The revised implementation is more modular, making it easier to add extensions.
In addition, it is more performant than the old one.
This PR also adds the functionality to analyse reward-bounded reachability properties on POMDP, as described in https://proceedings.mlr.press/v286/bork25a.html
In the long-term, the revised implementation is supposed to fully replace the current one.
In partiucular, the plan is to not immediately port over all functionality, but to check which features we want to keep.
Thus, the current implementation is deprecated, but not removed.
Changes outside of Storm-POMDP are part of separate PR #1028