Bounded MC support for IDTMCs + Bugfixes + Unification of bounded MC logic#916
Conversation
…fixed computation of exact bounds + unified code for deterministic and non-deterministic models
plindnercs
changed the title
plindnercs
changed the title
| @@ -0,0 +1,198 @@ | |||
| #include "SparseStepBoundedHorizonHelper.h" | |||
There was a problem hiding this comment.
| #include "SparseStepBoundedHorizonHelper.h" | |
| #include "storm/modelchecker/helper/finitehorizon/SparseStepBoundedHorizonHelper.h" |
| @@ -0,0 +1,198 @@ | |||
| #include "SparseStepBoundedHorizonHelper.h" | |||
| #include "storm/adapters/IntervalAdapter.h" | |||
| #include "storm/adapters/IntervalForward.h" | |||
There was a problem hiding this comment.
| #include "storm/adapters/IntervalForward.h" |
The *Forward headers don't need to be included when the actual header is included, too.
Same for RationalNumberForward below.
| #include "storm/adapters/RationalNumberAdapter.h" | ||
| #include "storm/adapters/RationalNumberForward.h" | ||
| #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" | ||
| #include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h" |
There was a problem hiding this comment.
| #include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h" |
| #include "storm/utility/macros.h" | ||
| #include "storm/utility/vector.h" | ||
|
|
||
| #include "storm/environment/solver/MinMaxSolverEnvironment.h" |
There was a problem hiding this comment.
| #include "storm/environment/solver/MinMaxSolverEnvironment.h" |
| if (lowerBound == 0) { | ||
| maybeStates &= ~psiStates; | ||
| } | ||
|
|
||
| if constexpr (storm::IsIntervalType<ValueType>) { | ||
| maybeStates &= ~psiStates; | ||
| } |
There was a problem hiding this comment.
Why are we always excluding psiStates for interval models?
Also, this avoids potentially excluding them twice :)
| if (lowerBound == 0) { | |
| maybeStates &= ~psiStates; | |
| } | |
| if constexpr (storm::IsIntervalType<ValueType>) { | |
| maybeStates &= ~psiStates; | |
| } | |
| if (storm::IsIntervalType<ValueType> || lowerBound == 0) { | |
| maybeStates &= ~psiStates; | |
| } |
| // For the 'maybeStates' we definitely have to compute the values. | ||
| storm::storage::BitVector maybeStates = computeMaybeStates(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, lowerBound, upperBound, hint); | ||
| storm::storage::BitVector makeZeroColumns; | ||
|
|
There was a problem hiding this comment.
Add a comment here that explains the procedure for lowerbound!=0 and/or interval types
|
Thanks for your feedback @tquatmann! I was able to simplify the logic of computing the 'maybeStates' a bit and added some comments for further clarification. |
|
I had some trouble following the code in the SparseStepBoundedHorizonHelper (both, interval and non-interval code). Of course, this has been an issue already before this PR. Anyway, I have spent some effort to (hopefully) simplify the computations and streamline the different cases. Would be good if someone can have a short look at |
|
|
||
| // We identify states that must have probability 0 of reaching the target states to exclude them in the further analysis. | ||
| storm::storage::BitVector const probGreater0States = | ||
| detail::computeProbGreater0States<ValueType, SolutionType>(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, upperBound, hint); |
There was a problem hiding this comment.
Should one do this analysis also in two phases, as in, first look for upperBound-lowerBound, as that is a smaller number it may be quicker and more states will be zero, which is good for the first phase, and for the second phase, we can then use the actual zeros from the first phase with again a reduced number of iterations.
I do think the current implementation is also correct, just potentially a bit slower (caching effects may also invalidate anything i said)...
There was a problem hiding this comment.
Indeed, this could work, and would probably be a bit faster in cases where the bounds are small compared to the number of states. Not sure how common this case is.
However, I think I will merge this PR for now, so that we have a correct implementation in master.
|
LGTM! Many thanks both. |
4 participants
This pull request includes:
and thus resolves #914.