|
|
@ -175,15 +175,15 @@ namespace storm { |
|
|
|
newUpperBoundAlwaysLowerEqual = false; |
|
|
|
} |
|
|
|
} |
|
|
|
if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) { |
|
|
|
// All values moved up or stayed the same (but are not the same) |
|
|
|
if (newUpperBoundAlwaysHigherEqual) { |
|
|
|
// All values moved up or stayed the same |
|
|
|
// That means the guess for an upper bound is actually a lower bound |
|
|
|
iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues); |
|
|
|
// We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound |
|
|
|
// Set lowerX to the upper bound candidate |
|
|
|
std::swap(lowerX, upperX); |
|
|
|
break; |
|
|
|
} else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) { |
|
|
|
} else if (newUpperBoundAlwaysLowerEqual) { |
|
|
|
// All values moved down or stayed the same and we have a maximum difference of twice the requested precision |
|
|
|
// We can safely use twice the requested precision, as we calculate the center of both vectors |
|
|
|
bool reachedPrecision; |
|
|
@ -199,9 +199,6 @@ namespace storm { |
|
|
|
// From now on, we keep updating both bounds |
|
|
|
intervalIterationNeeded = true; |
|
|
|
} |
|
|
|
} else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) { |
|
|
|
// All values stayed the same. For safety we guess above this value again and check, if all values move down |
|
|
|
break; |
|
|
|
} |
|
|
|
// At this point, the old upper bounds (auxVector) are not needed anymore. |
|
|
|
|
|
|
|