Add upper and lowerbounds to check results.

[lukovdm]

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.

[volkm]

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?

[lukovdm]

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.

[volkm]

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.

[sjunges]

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.

[volkm]

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.

[lukovdm]

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]

I dont know whehter this should be part of this PR, but this could be a good moment to replace boost::variant here with std::variant?

[sjunges]

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.

[volkm]

Is there a difference between infinity and undefined or can they be considered the same?
For example, a conditional probability should throw an exception if the condition is not reachable but one could also set the result to undefined. There could also be a difference between not calculating the upper bound (undefined) and calculating it but getting infinity (for example in reward queries)? But I am not sure whether there is actually a distinction to be made.