Add upper and lowerbounds to check results. - #1031
Draft
lukovdm wants to merge 13 commits into
Draft
Conversation
volkm
reviewed
Aug 20, 2026
volkm
reviewed
Aug 20, 2026
|
|
||
| // The values of the quantitative check result. These are estimates of the actual values, which lie within | ||
| // the bounds below but carry no further guarantee. | ||
| boost::variant<vector_type, map_type> values; |
Contributor
There was a problem hiding this comment.
I would have thought that the values itself would now incorporate the type SolutionBounds to already include the lower and upper bounds.
Why are separate lower/upper bounds the better approach?
Contributor
Author
There was a problem hiding this comment.
Several of the methods producing bounds currently do so in the form of a vector of lower bounds and a vector of upper bounds. This is also the format they are usually consumed in. I first tried incorporating the bounds in the value, but that led to a lot of rebuilding of vectors from the boundvalues. I thought this was ineligent and it looked slow.
I would like a better way to bundle soundess results of modelchecking that is more universal, but every CheckResult has a slightly different (justified) way of handling its values and thus I did not see a good way to do this.
Contributor
There was a problem hiding this comment.
I see that the bare-bone methods return vectors. I would have thought that at the CheckResult stage, the result is somewhat stable and will not change anymore. So this could be good point to go to the SolutionBounds?
I think the general discussion is at what level we want to introduce the SolutionBounds. For me, I would for example already find them useful in some of the helper methods such as Fox-Glynn.
Contributor
There was a problem hiding this comment.
Are you suggesting to have vectors of pairs instead of a pair of vectors? I am not sure I would agree with that, from an algorithm perspective.
Contributor
There was a problem hiding this comment.
I would keep the pair of vectors. I agree that this is more performant.
In the current version using SolutionBounds = std::optional<std::pair<std::vector<ValueType>, std::vector<ValueType>>>; so it would should already fit. I would just use these new type to make sure we have a consistent handling of the bounds.
Contributor
Author
There was a problem hiding this comment.
The ExplicitQualitativeCheckResult also supports maps of values instead of vectors of values. Which is used in filtered results and methods which only produce a value for the initial state. But I did not add this as a variant to the SolutionBounds, as that would require supporting maps everywhere.
Contributor
Author
|
I will do a pass over the code and clean up any weird AI smells, this draft is mostly so I can have early feedback on the architecture. |
sjunges
reviewed
Aug 24, 2026
Contributor
|
What if we dont have upper bounds? We could of course then have a vector of infinities, but is that better than not having the vector?
… On 24 Aug 2026, at 16:25, Matthias Volk ***@***.***> wrote:
@volkm commented on this pull request.
In src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h <#1031 (comment)>:
> @@ -85,9 +115,26 @@ class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType
return t == typeid(ValueType);
}
- // The values of the quantitative check result.
+ /*!
+ * Asserts that the given bounds have the same shape as the values.
+ */
+ void assertBoundsShape(boost::variant<vector_type, map_type> const& bounds) const;
+
+ /*!
+ * Writes the value of the given state, followed by its bounds if any are known.
+ */
+ void printValue(std::ostream& out, storm::storage::sparse::state_type state) const;
+
+ // The values of the quantitative check result. These are estimates of the actual values, which lie within
+ // the bounds below but carry no further guarantee.
boost::variant<vector_type, map_type> values;
I would keep the pair of vectors. I agree that this is more performant.
In the current version using SolutionBounds = std::optional<std::pair<std::vector<ValueType>, std::vector<ValueType>>>; so it would should already fit. I would just use these new type to make sure we have a consistent handling of the bounds.
—
Reply to this email directly, view it on GitHub <#1031?email_source=notifications&email_token=ADH67DEJPZ5B7V6MZSHU3K35LRF4HA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBQHA4TAMBTG4ZKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLDGN5XXIZLSL5RWY2LDNM#discussion_r3844377461>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADH67DGPWG5TA7POLSFVIID5LRF4HAVCNFSNUABEKJSXA33TNF2G64TZHM3TCMZZGU2TANB3JFZXG5LFHM2TEMBTGQ4DMMRXG2QXMAQ>.
Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/ADH67DFXCQZQYPAHHOSEK6L5LRF4HA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBQHA4TAMBTG4ZKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJKTGN5XXIZLSL5UW64Y> and Android <https://github.com/notifications/mobile/android/ADH67DBQMNA44YIDJS6UDFT5LRF4HA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTKMBQHA4TAMBTG4ZKM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLTGN5XXIZLSL5QW4ZDSN5UWI>. Download it today!
You are receiving this because you commented.
|
Contributor
|
Is there a difference between infinity and undefined or can they be considered the same? |
Contributor
Author
|
I guess there is a difference between I tied to find an upperbound as this is the best I came up with and I did not even try to find one. That would be the difference between infinite and undefined. But not trying is usually for all states while infinite could be for some states. |
Contributor
Author
|
This PR now includes moving away from a map in the ExplicitQua(nt/l)itativeCheckResults. This allows for using the |
lukovdm
force-pushed
the
soundresults
branch
2 times, most recently
from
September 7, 2026 13:31
7005af6 to
ad219bb
Compare
… available states in vector.
Value iteration now certifies its own solution bound: while iterating it tracks whether the sequence is monotonically approaching the solution from one side and, if so, reports the final iterate as a sound bound in that direction. NativeLinearEquationSolver::solveEquationsPower and IterativeMinMaxLinearEquationSolver::solveEquationsValueIteration pass that through to the solution bounds of the solver. The topological solvers instead derive bounds from the precision they were asked to achieve. A sound topological solve hands every SCC a precision of eps divided by the length of the longest SCC chain, and the deviation an SCC inherits from its predecessors enters its own solution as a convex combination of the values at the exits, i.e. without amplification. The per-SCC deviations therefore add up to at most eps along any chain, so eps bounds the error of the overall solution and [x - d, x + d] is sound. The shared conversion from a precision to such an interval, including the relative criterion and the tightening with any a priori bounds, lives in the new AbstractEquationSolver::setSolutionBoundsFromPrecision. Nothing is claimed when soundness was not requested: an unsound solver only reports that its iteration stopped moving, which is no statement about the distance to the solution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011oamBujHwK891QqnAYZ6Wr
lukovdm
force-pushed
the
soundresults
branch
from
September 7, 2026 14:14
ad219bb to
c7bb8a4
Compare
… sentinel The check result stores its bounds in the extended value type so that a single interface serves every algorithm, whether or not it can bound a value by infinity. Bounds that arrive in the plain value type are therefore widened, and they are taken to be finite throughout while doing so: nothing hands bounds around by sentinel, and an algorithm that has an infinite bound to report says so by handing over the extended type in the first place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011oamBujHwK891QqnAYZ6Wr
The direction of an iteration is learned by comparing the new value of an entry against the one it overwrites. That is the previous iterate only when the operand is updated in place: with a regular multiplication the two operands alternate, so the entry being overwritten holds the iterate from two steps ago, and in the first iteration it holds whatever the auxiliary vector was left with by an earlier solve. Neither says anything about the direction of the step that was just taken, so an iteration that in fact decreased some entries could be reported as a lower bound, which is not merely loose but inverted. The convergence criterion reads the same entry and is unaffected, since across two steps of a monotone sequence it is a stricter test that stops later rather than earlier. A direction is not a distance, so it gets no such reprieve, and nothing is claimed unless the iteration ran in place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
The two directions were tested as alternatives, so an iteration in which the operator reproduced its operand reported only that the operand lies below the solution. Such an iteration establishes both sides at once: the operand is the fixed point, and the equation systems handed to this helper have only one, so it bounds itself from either side. Testing the two directions independently reports that as the point interval it is. Whether the iterates stopped moving because the system was solved outright or because the arithmetic ran out of precision is not distinguished, in keeping with the bounds being sound up to floating point throughout. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
Both procedures keep the solution enclosed between two vectors in every iteration, which is the property they are named for, and both then collapse that enclosure into a single point estimate before returning. The enclosure is now read out first and reported as the bounds on the solution, as interval iteration already did. Neither needs to have converged for this: sound value iteration bounds the solution by its two scaling factors as soon as both are known, and guessing value iteration only ever writes a guess back once it has verified it, so the vectors it hands out enclose the solution throughout. An aborted run therefore reports a wider enclosure rather than none. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
Some procedures do not approach the solution but arrive at it: state elimination, an LU factorization, a single topologically ordered sweep over an acyclic system, and rational search once it has verified a sharpened candidate to be a fixed point. Each of those now reports its result as both the lower and the upper bound through the new AbstractEquationSolver::setSolutionBoundsExact, which is the strongest statement a solver can make about what it computed. Policy iteration is not among them. Its own termination says that the scheduler is optimal, not how accurately the values under that scheduler were computed, so it forwards whatever the last solve of the induced equation system established instead of claiming anything itself. That makes it exact when the inner solver is and silent when the inner solver is silent. Left out are the iterative Eigen methods, which stop at a tolerance like any other iteration, and the LP-based solver, whose backend may be an inexact one with a simplex tolerance that is a different thing from rounding. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
The out-parameter that the value iteration helpers use to hand back the bounds they maintain was a raw pointer defaulting to nullptr. Storm has a type for exactly this, storm::OptionalRef, whose own documentation names optional function arguments as its use case, and which is already used in this way elsewhere in the core library. Using it here keeps the callers from spelling out an address-of and gives the parameter a name that says it does not own anything. The pointer form remains the prevailing idiom for other optional out-parameters in this directory (Multiplier, GameSolver, LpMinMaxLinearEquationSolver); those are left alone, as changing them has nothing to do with the bounds. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
computeValuesForMaybeStates is shared between the probability and the reward paths and has been collecting the solver's bounds for both all along, but computeReachabilityRewardsHelper read only the values out of it, so every R=? query on an MDP dropped them. Embed them over the qualitative state sets the same way the until-probabilities path does: outside the maybe states the reward is exactly zero or exactly infinity, so the entries the result vector already holds bound those states from either side. computeTotalRewards may solve on an end component quotient and map the values back afterwards; the bounds get the same treatment, which is sound because all states of an eliminated end component share the value of their quotient state. Note that this is only claimed where the solver claims it: minimizing expected rewards does not give a unique solution unless the maybe states are free of end components, so plain value iteration keeps quiet there, while it does report for the maximizing direction. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
Unlike the probability paths, which return a DTMCSparseModelCheckingHelperReturnType, the reward paths returned a bare vector and so had nowhere to put the bounds the linear equation solver produces; they never asked for them. Return the same type from computeReachabilityRewards, computeReachabilityTimes and computeTotalRewards, and read the bounds out where the values are read, embedding them over the states whose reward is qualitatively zero or infinity. Two callers only take the values, both because the bounds would need work that this commit does not do: - computeConditionalRewards solves on the Baier-transformed model, so the bounds it gets back are indexed by transformed states. - SparseCtmcCslHelper returns plain vectors of its own, so carrying the bounds further would mean changing the CSL helpers and their model checker too. That is the natural next step for CTMC reward queries. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZPHMTb2xEncinYBJX3sjh
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
3 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.
Added optional upper and lower bound vectors to ExplicitQuantitativeCheckResult.
Added a solution bounds field to the AbstractEquationSolver which is populated by the solvers.
Currently II and OVI return their bounds through the native and iterative-min-max solver for DTMCs and MDPs.
This was done for until and globally formula.