Conversation
(cherry picked from commit a428484)
(cherry picked from commit 6e304c5)
(cherry picked from commit 68f0d73)
… available states in vector. (cherry picked from commit 5a6f464)
… 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 (cherry picked from commit 5632fd1)
The out-parameter that the interval and optimistic 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_01TfkAUfVqCKnSCRm3fAwJzL
…value. (cherry picked from commit 16668e4)
Constructing a check result from a plain vector of values scanned every entry for the sentinel that storm::utility::infinity yields, which for rationals is the literal 100000000000. On an exact reachability probability that is a comparison against a fake infinity for every state, and it made "P=? [F ...] --exact" report two deprecation warnings about a sentinel that path never produces. These constructors now widen instead, applying to the values the rule that already governs the bounds: what arrives in the plain type is finite, and a computation that can produce an infinity says so by handing over the extended type. Every sparse path that can produce one does -- the reachability reward, total reward and expected visiting time helpers all return extended vectors -- so nothing is lost. Verified that an unreachable target still reports [inf, inf] in both the exact and the floating point case. The remaining callers of fromSentinel are the symbolic and hybrid results, whose helpers do still fill ADDs with the sentinel. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit 6b71f2f17394f2b0f6e6419debf459cb1f7f3ad0)
A side that was never proven was printed as the infinity that bounds anything, so a probability computed by a procedure that certified only one side read as [0.3828117384, inf] -- which says the value might be arbitrarily large about a number that cannot exceed one. The reader cannot tell that apart from a genuinely infinite bound, which is a statement the tool does make: a state that cannot reach the target has an expected reward of exactly [inf, inf]. Both are now distinct. A missing side prints as "-", and "inf" is reserved for a bound that really is infinite. The JSON export already omitted the key for a missing side and is unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
…nclose the answer
Nothing asserted the one thing the bounds claim. This adds a suite that checks,
for each of the two configurations that produce them, that
lower <= exact <= upper and lower <= reported value <= upper
on properties whose answer is known in closed form: the Knuth-Yao die and the two
process consensus protocol, as until probabilities on a DTMC and on an MDP.
The configurations are listed as ones that must report both bounds, so a path that
quietly stops reporting fails rather than passing vacuously.
The tolerance of 1e-12, far below the solver precision the configurations ask for,
is there because a bound computed in doubles can land an ulp on the far side of an
answer that doubles cannot represent.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
lukovdm
changed the title
lukovdm
force-pushed
the
soundresults-algorithms
branch
from
September 10, 2026 13:32
30ed498 to
64bb76c
Compare
Comments that restate the code or a member name are removed, as are notes about work that is not done. What is left states a reason the code does not: why copying the result vector supplies the values outside the maybe states, why the two bounds are swapped when complementing, and why an unverified guess is not an upper bound. The convention for the two optional sides is stated once, on SolutionBounds, rather than repeated with examples at each use. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
lukovdm
force-pushed
the
soundresults-algorithms
branch
from
September 10, 2026 14:32
64bb76c to
1a31f4c
Compare
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 (cherry picked from commit c7bb8a4)
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 (cherry picked from commit 4ab503b)
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 (cherry picked from commit c29ce70)
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 (cherry picked from commit 03f5d08)
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 (cherry picked from commit a932f8a)
The value iteration and sound value iteration helpers gained their bounds out-parameter as a raw pointer, matching what interval and optimistic value iteration had before those were converted. This brings them into line, so that every helper in this directory hands the bounds back the same way. One site needed more than a mechanical edit: the MinMax value iteration builds the reference conditionally, since the direction certificate is only sound for a unique fixpoint, and OptionalRef deliberately has no assignment operator. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
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 (cherry picked from commit a3d6dc4)
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 (cherry picked from commit a656808)
Until probabilities, reachability times, reachability rewards and total rewards on a CTMC are all reductions to the corresponding query on the embedded DTMC, so the linear equation solver was producing bounds on them already and the CTMC helper was dropping them on the floor. The four now return the same type the DTMC helper does and hand what they get straight through. That return type is no longer DTMC-specific, so it is renamed to DeterministicSparseModelCheckingHelperReturnType: it fits both models exactly, as neither has nondeterminism for a scheduler to resolve. It stays next to the MDP one, which is likewise used from the CSL helpers. Bounded until keeps taking only the values. It reduces to unbounded reachability only for the interval [0, inf] and otherwise goes through uniformization, which produces no bounds, so reporting them for the one case would be inconsistent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit d07454ff76093d8b1c9572fa0515c785afb2bb11)
filter(min, ...) and its siblings collapsed a result to a single number and threw the enclosure away, so the one place where a property asks a question of several states at once reported less than the per-state output right next to it. QuantitativeCheckResult gains an aggregate(FilterType), which reports the aggregate of the values together with the aggregate of each bound that is known. Every aggregation on offer is monotone in each individual value, so applying it to the lower resp. upper bounds bounds the aggregate of the values. The default implementation reports no bounds, which is right for the results that cannot carry any, so the symbolic and hybrid results need no change. The explicit result aggregates a bound by wrapping it in a result of its own and calling the very methods that aggregate the values, so the two kinds of aggregate cannot drift apart. average() is now defined through sum() rather than repeating its loop. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit d0d4c002e590aedb1e29fe8be71adaa9e25e023b)
The aggregating filters print the aggregate of each bound next to the aggregate of the values, so they follow the same convention the per-state output already uses: a side that was never proven prints as "-", and "inf" is kept for a bound that really is infinite. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
There was no coverage of the bounds at all: nothing anywhere asserted the one
thing they claim. This adds a suite that checks, for every solver configuration
that is supposed to produce them, that
lower <= exact <= upper and lower <= reported value <= upper
on properties whose answer is known in closed form -- the Knuth-Yao die, the two
process consensus protocol, and two small CTMCs -- across until probabilities,
reachability rewards and reachability times on DTMCs, MDPs and CTMCs.
The configurations are listed as ones that must report both bounds, so a path
that quietly stops reporting fails rather than passing vacuously. Checked by
temporarily adding an unsound power iteration configuration, which fails all
seven model checking cases.
Three things the suite pins down beyond the enclosure itself: the exact
procedures must report the answer as both bounds rather than merely around it;
an aborted sound value iteration still encloses, and does so more loosely than a
converged one, which is the property that makes these bounds worth reporting at
all; and the aggregating filters carry the aggregate of each bound, checked on a
hand built result so that the arithmetic is exact rather than whatever enclosure
a solver happened to produce.
Inexact configurations are given a tolerance of 1e-12, far below their own solver
precision. It is needed because a bound computed in doubles can land an ulp on
the far side of an answer that doubles cannot represent: interval iteration
reports 3.6666666666666661 as the upper bound on the 11/3 expected coin flips of
the die.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
A property whose every state is decided by the qualitative preprocessing never reaches an equation solver, so nothing set any bounds and a result that is known exactly was reported with no bound at all. P=? [F "a"] on a model where the target is reached almost surely is the plain case: the answer is 1 and it was being reported as though nothing were known about it. Where the maybe states come out empty there is no equation system, no placeholder is written anywhere, and every entry of the result comes from the graph analysis, so the values bound themselves from either side. All four helpers that build a result out of qualitative state sets now say so. Reward infinity is included: a state that cannot reach the target reports [inf, inf]. Nothing changes where maybe states remain. In particular no attempt is made to report the qualitative entries when the solver bounds the maybe states but the solver reports nothing, since bounds are held per result rather than per state and the maybe entries would have to be filled with something meaningless. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit cf526abc37bc5dfc508b40d2eb28a793a6847699) (cherry picked from commit b381d5c)
Reachability on an interval DTMC is handed to the very MinMax solvers the MDP helper uses, so those solvers were producing bounds and computeRobustValuesForMaybeStates was returning only the values. It now hands the bounds back as well, and the two callers place them the same way they place the values: the probability path takes them over whole, since for interval models the result for the maybe states covers every state, while the reward path embeds them over the maybe states into the qualitative entries the result already holds. Only the reward path reports today, and that is the gate working rather than a gap. For interval models every method falls back to robust value iteration, whose bound is the direction certificate, and that is claimed only where the caller asserts a unique fixpoint -- which this helper does for rewards, on the strength of the graph-preservation check, and not for probabilities. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL (cherry picked from commit 848679e991f073b8168d8c7a73ca3336f3539231) (cherry picked from commit 30ed498)
Same pass as on the first change: comments that restate the code or a member name are removed, as are notes about work that is not done, and the ones that remain say in one or two sentences what the code cannot. The value iteration argument, the topological precision argument and the policy iteration one are the three worth keeping at length, and each is now about half of what it was. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TfkAUfVqCKnSCRm3fAwJzL
lukovdm
force-pushed
the
soundresults-algorithms
branch
from
September 11, 2026 08:38
1a31f4c to
0a22a52
Compare
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017n6Z1D3qCc4kFkU1moVg5L
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017n6Z1D3qCc4kFkU1moVg5L
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
1 participant
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.
Builds on top of #1031.
This PR adds bounds for the following algorithms:
This is the ones I have tackled so far, I am not entirely certain these bounds are correct, but they all seem logical to me and when possible I tried to read the papers to find if they claim a bound. Please suggest other algorithms I can report bounds for.