|
@ -422,13 +422,6 @@ namespace storm { |
|
|
uint64_t currentVerificationIterations = 0; |
|
|
uint64_t currentVerificationIterations = 0; |
|
|
uint64_t valueIterationInvocations = 0; |
|
|
uint64_t valueIterationInvocations = 0; |
|
|
|
|
|
|
|
|
//DEBUG
|
|
|
|
|
|
uint64_t up_occur = 0; |
|
|
|
|
|
uint64_t cross_occur = 0; |
|
|
|
|
|
uint64_t down_occur = 0; |
|
|
|
|
|
uint64_t no_case_occur = 0; |
|
|
|
|
|
//DEBUG END
|
|
|
|
|
|
|
|
|
|
|
|
if (!this->multiplierA) { |
|
|
if (!this->multiplierA) { |
|
|
this->multiplierA = storm::solver::MultiplierFactory<ValueType>().create(env, *this->A); |
|
|
this->multiplierA = storm::solver::MultiplierFactory<ValueType>().create(env, *this->A); |
|
|
} |
|
|
} |
|
@ -541,7 +534,6 @@ namespace storm { |
|
|
std::swap(currentUpperBound, newUpperBound); |
|
|
std::swap(currentUpperBound, newUpperBound); |
|
|
|
|
|
|
|
|
if (newUpperBoundAlwaysHigherEqual & ! newUpperBoundAlwaysLowerEqual) { |
|
|
if (newUpperBoundAlwaysHigherEqual & ! newUpperBoundAlwaysLowerEqual) { |
|
|
++up_occur; |
|
|
|
|
|
iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); |
|
|
iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); |
|
|
// Not all values moved up or stayed the same
|
|
|
// Not all values moved up or stayed the same
|
|
|
// If we have a single fixed point, we can safely set the new lower bound, to the wrongly guessed upper bound
|
|
|
// If we have a single fixed point, we can safely set the new lower bound, to the wrongly guessed upper bound
|
|
@ -550,12 +542,10 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
break; |
|
|
break; |
|
|
} else if (valuesCrossed) { |
|
|
} else if (valuesCrossed) { |
|
|
++cross_occur; |
|
|
|
|
|
STORM_LOG_ASSERT(false, "Cross case occurred."); |
|
|
STORM_LOG_ASSERT(false, "Cross case occurred."); |
|
|
iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); |
|
|
iterationPrecision = updateIterationPrecision(env, *currentX, *newX, relative, relevantValues); |
|
|
break; |
|
|
break; |
|
|
} else if (newUpperBoundAlwaysLowerEqual) { |
|
|
} else if (newUpperBoundAlwaysLowerEqual) { |
|
|
++down_occur; |
|
|
|
|
|
// All values moved down or stayed the same and we have a maximum difference of twice the requested precision
|
|
|
// 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
|
|
|
// We can safely use twice the requested precision, as we calculate the center of both vectors
|
|
|
// We can use max_if instead of computeMaxAbsDiff, as x is definitely a lower bound and ub is larger in all elements
|
|
|
// We can use max_if instead of computeMaxAbsDiff, as x is definitely a lower bound and ub is larger in all elements
|
|
@ -584,9 +574,6 @@ namespace storm { |
|
|
intervalIterationNeeded = true; |
|
|
intervalIterationNeeded = true; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
else { |
|
|
|
|
|
++no_case_occur; |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor()); |
|
|
ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor()); |
|
|
if (scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) { |
|
|
if (scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) { |
|
@ -609,10 +596,6 @@ namespace storm { |
|
|
std::swap(x, *currentX); |
|
|
std::swap(x, *currentX); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
// DEBUG
|
|
|
|
|
|
std::cout << "Up mov: " << up_occur << ", Cross: " << cross_occur << ", Down mov: " << down_occur << ", None: " << no_case_occur << std::endl; |
|
|
|
|
|
// DEBUG END
|
|
|
|
|
|
|
|
|
|
|
|
reportStatus(status, overallIterations); |
|
|
reportStatus(status, overallIterations); |
|
|
|
|
|
|
|
|
// If requested, we store the scheduler for retrieval.
|
|
|
// If requested, we store the scheduler for retrieval.
|
|
|