Improvements for conditional bisection method #847
Conversation
tquatmann
commented
Dec 24, 2025
tquatmann
commented
- Use acyclic min max solver when possible
- enable caching of solver data to avoid some re-allocations
- More careful treatment of exact computations
* Use acyclic min max solver when possible * enable caching of solver data to avoid some re-allocations * More careful treatment of exact computations
| ++numDigits; | ||
| middle = storm::utility::kwek_mehlhorn::sharpen<SolutionType, SolutionType>(numDigits, exactMiddle); | ||
| } while (middle <= *lowerBound || middle >= *upperBound); | ||
| // Check if the rationalCandidate has been within the bounds for four iterations. |
There was a problem hiding this comment.
Do we also do this if we are just searching to bound the value, rather than computing an exact number?
There was a problem hiding this comment.
Good question, we don't seem to have a dedicated code path for thresholded properties.
@lukovdm do you already have something for that? If not, I can add it here.
There was a problem hiding this comment.
For stuff like VI, we do have terminationconditions, right? Would they be applicable here?
There was a problem hiding this comment.
With a bound value, we just need to invoke the WeightedReachabilityHelper once. I would probably write a dedicated method for that. Basically a stripped down variant of computeViaBisection.
We can and should use terminationconditions for the restart method, though.
Fortunately, we already pass the SolveGoal (which includes the bound) to the ConditionalHelper. So it is a relatively small change.
2 participants
