Extended number to replace infinities on rationals - #1040
Merged
Conversation
Several places used storm::utility::infinity<T>() -- which is the literal
100000000000 for the exact value types -- as a stand-in for something
structural rather than for a value: a fold over an empty set, a bound that
the formula does not have, or a marker on a row. None of them needs a
number, and all of them are wrong for exact types the moment a real value
grows past the sentinel.
* The CSL time-bounded helpers and their model checkers take
std::optional<ValueType> for the upper time bound instead of
synthesizing an infinite one when the formula has no bound, following
the precedent of LpSolver. computeBoundedUntilProbabilitiesImca now
rejects an absent upper bound instead of computing a step count from
the sentinel.
* AcyclicSolverHelper stores std::optional factors and skips the
multiplication for rows whose b entry must be zero. That row used to
compute one / (one - one) and multiply the entry by the result, which
is a division by zero for every exact type.
* The min/max folds in RobustParameterLifter and
GradientDescentInstantiationSearcher use Extremum and std::optional,
which also avoids constructing a large rational per fold.
* MenuGameRefiner's Dijkstra initialisation uses a finite distance that
no reachable state can attain instead of an infinite one.
* DftExplorationHeuristic and PreprocessingPomdpValueBoundsModelChecker
express "not computed yet" as std::optional and a BitVector.
* storm-pomdp's sizeThresholdInit used infinity<uint64_t>(), which is
numeric_limits<uint64_t>::infinity() and therefore zero. Zero is the
codebase's own "pick a heuristic default" value, so "no size limit"
was only half implemented: the over-approximation reinterpreted the
zero as max() and was accidentally right, while the under-
approximation fell through to a heuristic threshold. It now says
max().
With those gone, infinity<T>() is ill-formed for integral types and
isInfinity<T>() is false for them, so the class of bug above cannot
return. The two DdManager instantiations of getInfinity<uint_fast64_t>
had no callers and would have produced an ADD of zeros.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
storm::utility::infinity<T>() is the literal 100000000000 for every exact
type, and isInfinity is a comparison against it. That aliases a reward of
1e11 with infinity, is not absorbing under arithmetic, is not the maximum
of the order, and has no negative counterpart, so every place that needs
a signed infinity has invented its own encoding.
ExtendedNumber<T> is a tag {NegativeInfinity, Finite, PositiveInfinity}
next to a T. It has a total order in which the infinities really are the
extremes, absorbing arithmetic, and unary minus. The exact value types
have no NaN, so the forms that are undefined over the extended reals --
inf - inf, 0 * inf and inf / inf -- throw an InvalidOperationException
rather than producing a quiet junk value.
The operators are hidden friends, so a finite T converts implicitly on
either side of them and mixed expressions read as they did before.
NumberTraits and std::numeric_limits are specialized for the type, which
is what lets the generic storm::utility::infinity and isInfinity reach it
without a special case.
Nothing pays for this that does not use it. ExtendedValueType<T> is
std::conditional_t<NumberTraits<T>::HasInfinity, T, ExtendedNumber<T>>
so ExtendedValueType<double> is double: the floating point path keeps its
IEEE infinity and is unchanged, and only the exact types get the tag,
where it sits next to a heap pointer that already dominates it.
NumberTraits gains HasInfinity, which is exactly the is_iec559 test that
Extremum was already making through a proxy, so Extremum's behaviour is
unchanged. Its new getExtendedValue() is the total counterpart of
getOptionalValue(): an empty extremum is the infinity it stands for,
+infinity when minimizing and -infinity when maximizing.
The sentinel specializations stay in place for now; they can only be
removed once the last caller is migrated.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A reward or an expected time can be infinite, and until now the only way
a result vector could say so was the literal 100000000000 that
storm::utility::infinity yields for the exact value types. Every consumer
that wanted to know had to compare against that number, and any real
value that reached it was indistinguishable from infinity.
QuantitativeCheckResult now has an extended_value_type, which is
ExtendedValueType<ValueType>: unchanged for double, and ExtendedNumber
for the exact types. The explicit results hold their vector and their map
in it, and getMin, getMax, average and sum return it, as do the symbolic
and hybrid results. The result vector is therefore self-describing -- an
infinite entry is an infinite value, not a magic number the caller has to
recognise.
Nothing that computes changes type. The solvers, the matrices and the
solver hints keep operating on plain vectors of ValueType, which is where
the performance is, and infinity never enters an equation system: the
states that have it are excluded from the maybe states by construction.
Two bridges carry the parts that have not moved yet, and both are named
so that they can be removed with the sentinel:
* storm::utility::fromSentinel recognises the 100000000000 that the
reward and expected time helpers still write. It is applied where a
plain vector becomes a check result and where a decision diagram leaf
is read, so the boundary is honest even though the inside is not.
Probabilities are unaffected -- they live in [0,1].
* storm::utility::toSentinel goes the other way, for the interfaces
that are deliberately staying on the plain value type. It rejects
-infinity, which the sentinel cannot express at all.
For the consumers that have no representation for an infinite value there
is getFiniteValueVector, which asserts that there is none, and
getSentinelValueVector for the solver hints.
Where the type earns its keep, the hand-written case analysis goes away:
SparseParameterLiftingModelChecker used to carry two ternaries to move an
infinity across double -> RationalNumber -> CoefficientType, with a
comment conceding that the conversion would otherwise fail. Both are now
a plain convertNumber, and the region bounds -- which are already kept in
an Extremum -- hold the extended type.
JSON export writes an infinite value as "inf". It used to write the
sentinel for the exact types and null for double, neither of which is a
representation of infinity.
Tests that assert an infinite result now compare against a real infinity
rather than against the sentinel, and EXPECT_NEAR knows that an infinity
is within any distance of itself and of nothing else.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The sparse helpers computed a reward or an expected visiting time of infinity and wrote it as the sentinel that storm::utility::infinity yields, leaving the check result to reinterpret it. They now return the solution type extended with the infinities, so the value is infinite from the point where it is computed. Widened are the reachability reward, total reward, reachability time and conditional queries of the DTMC, MDP, CTMC and Markov automaton helpers, the expected visiting times helper, and the reward query of the elimination model checker. The equation systems are untouched: a solver still sees only finite values, and the states that are solved for are exactly the ones that have one. MDPSparseModelCheckingHelperReturnType gains a second type parameter so that the values it carries can be extended while the scheduler it carries is not. setVectorValues and SparseMdpEndComponentInformation::setValues accept a source whose element type differs from the target's, which is what widening a result while narrowing into a solver needs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A quantile in a dimension that needs no bound at all is infinite, and the quantile helper wrote that as the sentinel. It now hands back the extended value type, which means the Pareto curve that carries a multi-dimensional quantile has to hold one too, so ParetoCurveCheckResult's points are extended while its approximating polytopes stay in the plain value type: a polytope is a geometric object and has no infinity. The producers that cannot yield an infinite coordinate -- the multi-objective queries -- keep handing over plain points through a widening constructor. Adds storm::utility::widen, narrow and isFinite. narrow is what toSentinel should have been: it keeps the value where the plain type has an infinity of its own and throws where it has none, rather than inventing a number for it. equalModuloPrecision compares infinite values for equality instead of taking a difference that is not defined for them. QuantileQueryTest now expects a real infinity where it accepted 100000000000. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The bounds that belief exploration narrows start at the two infinities and stay infinite for an objective that is not achievable, so Result holds them in the extended value type and diff() treats an infinite gap as unbounded rather than subtracting values it cannot subtract. The exploration itself still computes in the plain value type, so the sentinel is interpreted where a bound enters the result -- the trivial bounds and the two update functions -- and nowhere else. That bridge goes away when the belief value bounds stop using the sentinel. BeliefExplorationPomdpModelCheckerTest now expects a real infinity where it accepted 100000000000, and its bound comparisons force the GMP expression to the value type before comparing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Building the extended result vector from a plain one cost two things that profiling showed to be larger than the widening itself: every element was deep-copied even where the caller had handed over a temporary, and each element was compared against a freshly constructed sentinel, which for a value type whose infinity is a number rather than a bit pattern allocates. fromSentinel gains a vector form that builds the sentinel once and moves the values over, and the check result gains the rvalue constructor that reaches it. On an exact until-probability query over 205k states this takes the extra allocations from 668k to 267k and removes an 11% model-checking regression. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The values that are handed to the equation solver were copied out of the extended vector one by one. They are taken over instead, which is what narrowFinite does: the counterpart of widen for a vector known to be finite. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A hint for a reward computation says of some states that they cannot reach the target at all, so it has to be able to hold an infinite value. It went through the sentinel instead: the instantiation checkers narrowed a result to the plain value type, wrote 100000000000 for the infinite entries, and the next check read that number back as an infinity. The hint now stores the extended value type, and the instantiation checkers hand it the result vector directly. The solvers keep working on the plain type, so the values are narrowed where they enter one. A hint may be stale -- the computation it came from may have found a state unable to reach the target where this one does not -- so an infinite entry falls back to the default starting value rather than being narrowed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The expected time until failure of a DFT that cannot fail is genuinely infinite. For the parametric value type that came out as 100000000000: the check result held a real infinity and DFTModelChecker narrowed it back to the sentinel on the way out, so a parametric MTTF query printed the literal number instead of an infinity. The DFT result type is now the extended value type, which the analysis API and the CLI pick up for free -- both already spell their return type as DFTModelChecker<ValueType>::dft_results, and printing goes through the visitor. A parametric PAND now reports inf rather than 100000000000; the double path is unchanged, since double had a real infinity all along. Modularisation keeps combining module results in the plain value type. It only handles probability formulas, so nothing infinite reaches it, and wrapping the fold would defeat the expression templates of the parametric types for no gain. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Both call sites bound the result of asExplicitQuantitativeCheckResult by value, so every monotonicity check and every assumption check deep-copied the entire value vector only to read it. Bind by const reference instead; the only use is the const getFiniteValueVector. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Parameter lifting knows exactly which states cannot reach the target -- it has an infinityStates bit vector -- and was writing 100000000000 into the result for them purely because the vector could not hold an infinity. The quantitative values are now the extended type, so the sentinel is gone from the region checkers and from the value bound the region records. The gradient descent seeds its search at the worst value there is, which was the sentinel too. That had turned an ordinary guard into a divergence between the value types: after two steps that both land outside the region, the tiny-change test computes oldValue - currentValue. For double this is inf - inf, so NaN, so the comparison fails and the search continues. For the sentinel it was 1e11 - 1e11, so zero, which counts as a tiny change and ends the search early. The test now requires both values to be finite, which is what double did all along. Order-based monotonicity keeps its plain vectors: it does arithmetic on them, and it only accepts probability formulas, so the values it is handed are finite by construction and are narrowed on the way in. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Sampling and the monotonicity check both read a result through getFiniteValueVector, which throws from inside the check result once any value is infinite -- naming neither the property nor the state. Both analyses sample whatever property was asked for, rewards included, so this is reachable. They now check finiteness first and report the property and the state. This also changes the double path, which getFiniteValueVector never guarded: an infinite value used to flow into the derivative checker and produce a NaN there. It now stops with the same message, so both value types behave alike. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Exporting a check result is the one user-visible behaviour that widening changed, and nothing covered it. The test checks a reward property with two unreachable states, exports it, and reads the file back: an infinite state must be the string "inf", a finite one a number equal to its value. It runs for double and for the exact type, since double had a real infinity all along and would not catch a regression here. Against the old behaviour the exact case exported 100000000000.0 and the double case exported null, since JSON has no infinity of its own. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
It assigns an extended vector straight into a plain one, which works only because bounded until is instantiated for double alone and double is its own extended type. Say so at both sites, so that whoever gives RationalNumber an exponential is not surprised. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Upstream's header split (stormchecker#1034) replaced the umbrella includes in DFTModelChecker.h at the same time as the extended value type added ExtendedNumber.h to that block, which is the only conflict in the merge. Resolved in favour of the fine-grained includes, keeping ours in place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
isFinite reported a NaN as finite, because a NaN is not an infinity. Every guard built on this predicate is there to keep a value that is not a number out of a computation, and at the double to exact seam a NaN does not merely give a bad answer: carl::rationalize asserts on it. The narrowing helpers only asserted that the value they were handed was finite. An infinite value carries a zero as its payload, so a release build turned an infinity into a zero and carried on. These are preconditions on data rather than invariants of the code, so they now throw. Writing a result out only recognised the positive infinity, so a negative one fell through to the finite payload -- exported as null for double and as an assertion failure for the exact types. Add the generic counterpart of isInfinity and use it here; print and writeToStream already had this right. The narrow and widen helpers had no tests at all, which is where the boundary lives. Cover them, along with the negative infinity arithmetic and the conversion that carries an infinity out of a double computation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The extremal value a region check hands around can now really be infinite, and asking for a relative guarantee multiplied the precision by it. With the precision the command line passes by default that is 0 * inf, and with any other precision the comparison that follows is inf - inf; both threw. There is no relative precision around an infinite value, so compare against it directly instead. The absolute case already coped. Take the two callbacks by const reference while here: they are called inside the refinement loop and each argument is a tag plus a GMP rational. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The values handed to the hint come out of getSentinelValueVector, so an infinite one among them is the sentinel rather than an infinity. Widening them took the sentinel at face value and produced a finite 10^11, which is what widen is supposed to do; fromSentinel is the one that translates it. The comment claimed the opposite of what the code did. Nothing reads a wrong answer out of this today -- the hint is a starting point for value iteration and the consumer that tests for an infinity is not reached on this path -- but the two value types had silently diverged, with double starting from zero where the exact types started from 10^11. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Comparing a plain value with an extended one converted the plain operand first, and that conversion copies it. For a GMP rational a copy is two heap allocations, so every such comparison allocated -- in value iteration, once per choice. Add the comparisons that read the payload instead. They are an exact match where the converting ones need a user defined conversion, so they win wherever they apply, and they are not viable at all when both operands are extended, so no existing comparison changes meaning. Measured over 3000 comparisons of a GMP rational against an extended value: 6000 allocations before, none after. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
An extremum kept the value it was given plus a flag saying whether it had been given one, except for a value type with its own infinity, which encoded the empty case as the infinity no value improves upon. Widening that condition from is_iec559 to NumberTraits::HasInfinity handed the second encoding to ExtendedNumber as well, and there it does not work: for that type an infinity is a value someone may legitimately contribute, so an extremum holding one became indistinguishable from an empty one. Rather than exclude ExtendedNumber, store every extremum in the type that extends its value type with the two infinities. That type is the plain one wherever it already has an infinity, so double keeps the exact layout it had. The empty case then stops being a case at all: the minimum over an empty set is +infinity and the maximum over one is -infinity, which is what those extrema are. getExtendedValue is total and is now the accessor to reach for. operator* keeps handing out the plain value, so the value iteration helpers are untouched, but its precondition is that the value is finite rather than that the extremum is non-empty -- a value type without an infinity has nothing to return for one. The region refinement loop reads its bounds through getExtendedValue accordingly, which is what it needed: an infinite bound is a bound, not a missing one. Comparisons against the stored value go through the mixed operators, so nothing is wrapped on the way in and the hot path allocates no more than it did. AnnotatedRegion goes back to holding the plain coefficient type, and the four ExtendedNumber instantiations of Extremum are no longer needed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The rational number type extended with the two infinities was spelled out at every use, in two different ways -- as the wrapper and as the alias that picks it -- which made the same type look like two. Name it once and use it. The RationalFunction instantiations keep the long spelling: this is the one name that was asked for, and adding a sibling is a separate call. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
# Conflicts: # src/storm-pars/derivative/GradientDescentInstantiationSearcher.cpp
The functions that only exist for as long as the sentinel does -- fromSentinel, toSentinel, and the infinity specialisations that return the literal 100000000000 -- now say so when they are reached. Storm builds with -Werror, so the [[deprecated]] attribute would turn every remaining use into a build failure rather than a warning; STORM_LOG_DEPRECATED reports the same thing at runtime, once per function, and only in a debug build. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AzQDTvuiaJqSGEVdpM4uYy
lukovdm
commented
Aug 28, 2026
lukovdm
left a comment
lukovdm
left a comment
Contributor
Author
There was a problem hiding this comment.
Partial review. Look at patterns in the review and apply them PR wide.
Name every alias for a value type extended with the infinities after the plain alias it is built from -- ExtendedValueType, ExtendedSolutionType, ExtendedCoefficientType, ExtendedConstantType, ExtendedPointType -- rather than the four spellings that were there before, and give the check results a class alias so that storm::utility::ExtendedValueType<ValueType> is not spelled out inside them. Write the type of a local instead of auto, and revert the files whose only change was that rewrite. SparseDtmcPrctlModelChecker and SparseCtmcCslModelChecker are back to upstream apart from the queries whose return type actually changed. Add narrowFinite overloads that take a const reference and that fall back to a given value, and use them where a check result or a stale solver hint was narrowed by hand. Let print and printRange deduce the type they are handed, which removes the explicit template arguments at their call sites, and move SparseMdpEndComponentInformation::setValues back into the .cpp with a single template parameter, widening the maybe state values at the one call site that needs it. Drop the comments that justify the change rather than describe the code. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AzQDTvuiaJqSGEVdpM4uYy
These were missed in the first pass over the review. The DFT model checker held its results in a result_value_type; it is now called ExtendedValueType like every other alias for a value type extended with the infinities, while approximation_result, dft_results and property_vector keep the names they had. The comments that justify where a value is held rather than describe the code are dropped here too. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AzQDTvuiaJqSGEVdpM4uYy
lukovdm
commented
Aug 28, 2026
The extremum stores its value directly rather than in a one member struct, and better gained the overload for an extended value, so betterThanStored and the StorageType alias are gone. The documentation says what a thing is rather than what it is not. narrowFinite for a vector with a fallback value takes its values over rather than copying them, which lets the two solver hints that narrowed state by state say so in one statement. The scalar form had no caller left and is dropped. getFiniteValues in storm-pars-cli only wrapped ExplicitQuantitativeCheckResult::getFiniteValueVector in a longer message, so its two callers use that directly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AzQDTvuiaJqSGEVdpM4uYy
The check result export test built its DTMC from a PRISM program that pins the initial state down. Storm enumerates the initial states of such a program with an SMT solver, so the test failed rather than skipped in the CI configuration that is built without Z3. Make every state initial instead, which takes the enumeration off the SMT path. That leaves what the test checks alone, since the check result and its export cover all states either way. The scalar fromSentinel takes a forwarding reference, which its constraint narrows to an rvalue. clang-tidy cannot see that and flags the std::move as a move of a forwarding reference; forward instead, which the constraint makes equivalent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NYYrpxGxxDTLqJo1TAYNML
A check result hands its values to print as the extended value type, but the test that decides whether to add the decimal approximation still recognised only the plain rational number. Every exact result therefore lost its "(approx. ...)" suffix, which a benchmark run over the QVBS exact set caught on all 17 of its rational instances. printRange had already been updated; print had not. Test both directions, since nothing covered the printed form of a check result before. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NYYrpxGxxDTLqJo1TAYNML
lukovdm
marked this pull request as ready for review
September 2, 2026 08:13
Contributor
Author
|
@volkm I cannot request a copilot review, but I heard you still can. Would you want to do one for this PR? |
Contributor
|
Sure, I have triggered it. I will also do some manual review sometime this week. |
There was a problem hiding this comment.
🟡 Changes recommended
Infinite aggregation and export paths plus deprecation logging still contain correctness or concurrency defects.
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Review details
Suppressed comments (2)
src/storm-pars-cli/solutionFunctions.cpp:70
- The CTMC export path also unconditionally narrows an extended result. Infinite expected rewards therefore abort export with
InvalidOperationException; pass the extended value through an infinity-aware exporter instead.
std::optional<ValueType> rationalFunction =
storm::utility::getFinite(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]);
src/storm-pars-cli/solutionFunctions.cpp:94
- For symbolic parametric results,
sum()can now return an extended infinity, but this call immediately requires it to be finite. Exporting an infinite symbolic solution therefore fails; the exporter needs to accept and serialize the extended result.
std::optional<ValueType> rationalFunction = storm::utility::getFinite(result->asSymbolicQuantitativeCheckResult<DdType, ValueType>().sum());
- Files reviewed: 106/106 changed files
- Comments generated: 4
- Review effort level: Balanced
tquatmann
reviewed
Sep 4, 2026
tquatmann
left a comment
tquatmann
left a comment
Contributor
There was a problem hiding this comment.
Great work on this decade old issue!
I made a manual review and things look good to me besides my minor comments.
Many Thanks!
Comment on lines
+24
to
+31
| #define STORM_LOG_DEPRECATED(message) \ | ||
| do { \ | ||
| static bool const storm_deprecation_reported = [&] { \ | ||
| STORM_LOG_WARN("Deprecated: " << message); \ | ||
| return true; \ | ||
| }(); \ | ||
| (void)storm_deprecation_reported; \ | ||
| } while (false) |
Contributor
There was a problem hiding this comment.
This PR also adds STORM_LOG_DEPRECATED which, in DEBUG mode, prints a deprecation warning once. In RELEASE mode, this macro does nothing.
(This looks good to me, I just found this change was a bit hidden and wanted to comment on this for visibility :)
tquatmann
reviewed
Sep 4, 2026
Contributor
|
Besides that minor comment, I believe we should merge this soon. |
Two conflicts, both between a rename on this branch and an unrelated change upstream, resolved by taking both sides: - GradientDescentInstantiationSearcher: oldValue stays ExtendedConstantType, the precision now comes from env.modelTolerance(). - RegionRefinementChecker: computeExtremalValueHelper keeps its extended signature, PartitioningProgress gets the show-progress delay. The getFinite and Extremum::operator* preconditions became assertions in 71b0931, so the tests that expected an exception from them are death tests now, following the pattern in BitVectorTest. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ABBG2rU3zjiTBnLc811Qbq
Contributor
Author
|
Then this should be done. |
lukovdm
added a commit
to lukovdm/storm
that referenced
this pull request
Sep 9, 2026
Resolve the conflict in SparseDtmcPrctlHelper::computeConditionalRewards: keep this branch's up-front reachability check on the condition (which replaces the `if (!conditionStates.empty())` guard), and take master's ExtendedSolutionType for the result and the reachability rewards vector. Adapt the new conditional tests to the extended-number representation introduced in stormchecker#1040: assert against positiveInfinity rather than infinity, which for rationals is now only a legacy placeholder value. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01218nYyRvf8TAGynDRXrtwa
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
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.
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 theValueTypeif it already supports infinity (doubles) and returnsExtendedValue<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
Extremumno longer has two ways to store the value but always goes through ExtendedValueType. This also solves the issue whereEtremum<ValueType>behaved differently onDoublesthen onRationalNumbers. 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:
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.
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.