sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

OVI: Defaulting to M1/M2, changed CLI option for termination guarantee 

Adapted CLI option description
tempestpy_adaptions
Jan Erik Karuc 4 years ago
parent
48a3b5a927
commit
6c70b42549
5 changed files with 97 additions and 187 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm/environment/solver/OviSolverEnvironment.cpp
  2. 4
      src/storm/environment/solver/OviSolverEnvironment.h
  3. 8
      src/storm/settings/modules/OviSolverSettings.cpp
  4. 4
      src/storm/settings/modules/OviSolverSettings.h
  5. 262
      src/storm/solver/helper/OptimisticValueIterationHelper.h

6
src/storm/environment/solver/OviSolverEnvironment.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
relevantValuesForPrecisionUpdate = oviSettings.useRelevantValuesForPrecisionUpdate();
upperBoundGuessingFactor = storm::utility::convertNumber<storm::RationalNumber>(oviSettings.getUpperBoundGuessingFactor());
upperBoundOnlyIterations = oviSettings.getUpperBoundOnlyIterations();
terminationGuaranteedMinimumMethod = oviSettings.useTerminationGuaranteedMinimumMethod();
noTerminationGuaranteeMinimumMethod = oviSettings.useNoTerminationGuaranteeMinimumMethod();
}
OviSolverEnvironment::~OviSolverEnvironment() {
@ -41,8 +41,8 @@ namespace storm {
return upperBoundOnlyIterations;
}
bool OviSolverEnvironment::useTerminationGuaranteedMinimumMethod() const {
return terminationGuaranteedMinimumMethod;
bool OviSolverEnvironment::useNoTerminationGuaranteeMinimumMethod() const {
return noTerminationGuaranteeMinimumMethod;
}
}

4
src/storm/environment/solver/OviSolverEnvironment.h
View File

@ -17,7 +17,7 @@ namespace storm {
bool useRelevantValuesForPrecisionUpdate() const;
storm::RationalNumber getUpperBoundGuessingFactor() const;
uint64_t getUpperBoundOnlyIterations() const;
bool useTerminationGuaranteedMinimumMethod() const;
bool useNoTerminationGuaranteeMinimumMethod() const;
private:
storm::RationalNumber precisionUpdateFactor;
@ -25,7 +25,7 @@ namespace storm {
bool relevantValuesForPrecisionUpdate;
storm::RationalNumber upperBoundGuessingFactor;
uint64_t upperBoundOnlyIterations;
bool terminationGuaranteedMinimumMethod;
bool noTerminationGuaranteeMinimumMethod;
};
}

8
src/storm/settings/modules/OviSolverSettings.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
const std::string OviSolverSettings::useRelevantValuesForPrecisionUpdateOptionName = "use-relevant-values";
const std::string OviSolverSettings::upperBoundGuessingFactorOptionName = "upper-bound-factor";
const std::string OviSolverSettings::upperBoundOnlyIterationsOptionName = "check-upper-only-iter";
const std::string OviSolverSettings::useTerminationGuaranteedMinimumMethodOptionName = "termination-guarantee";
const std::string OviSolverSettings::useNoTerminationGuaranteeMinimumMethodOptionName = "no-termination-guarantee";
OviSolverSettings::OviSolverSettings() : ModuleSettings(moduleName) {
@ -31,7 +31,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, upperBoundOnlyIterationsOptionName, false, "Sets the max. iterations OVI will only iterate over the upper bound.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("iter", "The iterations.").setDefaultValueInteger(20000).addValidatorInteger(ArgumentValidatorFactory::createIntegerGreaterValidator(0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, useTerminationGuaranteedMinimumMethodOptionName, false, "Sets whether to perform calculations on element-wise minimum of iterated and old upper bound.").setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, useNoTerminationGuaranteeMinimumMethodOptionName, false, "Sets whether to perform element-wise minimum of iterated and old upper bound. If this option is set, that will be skipped, slightly increasing performance but giving no termination guarantee.").setShortName("ntg").setIsAdvanced().build());
}
double OviSolverSettings::getPrecisionUpdateFactor() const {
@ -54,8 +54,8 @@ namespace storm {
return this->getOption(upperBoundOnlyIterationsOptionName).getArgumentByName("iter").getValueAsInteger();
}
bool OviSolverSettings::useTerminationGuaranteedMinimumMethod() const {
return this->getOption(useTerminationGuaranteedMinimumMethodOptionName).getHasOptionBeenSet();
bool OviSolverSettings::useNoTerminationGuaranteeMinimumMethod() const {
return this->getOption(useNoTerminationGuaranteeMinimumMethodOptionName).getHasOptionBeenSet();
}
}

4
src/storm/settings/modules/OviSolverSettings.h
View File

@ -25,7 +25,7 @@ namespace storm {
uint64_t getUpperBoundOnlyIterations() const;
bool useTerminationGuaranteedMinimumMethod() const;
bool useNoTerminationGuaranteeMinimumMethod() const;
// The name of the module.
static const std::string moduleName;
@ -36,7 +36,7 @@ namespace storm {
static const std::string useRelevantValuesForPrecisionUpdateOptionName;
static const std::string upperBoundGuessingFactorOptionName;
static const std::string upperBoundOnlyIterationsOptionName;
static const std::string useTerminationGuaranteedMinimumMethodOptionName;
static const std::string useNoTerminationGuaranteeMinimumMethodOptionName;
};
}

262
src/storm/solver/helper/OptimisticValueIterationHelper.h
View File

@ -121,6 +121,8 @@ namespace storm {
ValueType two = storm::utility::convertNumber<ValueType>(2.0);
// Relative errors
bool relative = env.solver().minMax().getRelativeTerminationCriterion();
// Use no termination guaranteed upper bound iteration method
bool noTerminationGuarantee = env.solver().ovi().useNoTerminationGuaranteeMinimumMethod();
// Goal precision
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
// Desired max difference between upperX and lowerX
@ -135,142 +137,40 @@ namespace storm {
SolverStatus status = SolverStatus::InProgress;
if(env.solver().ovi().useTerminationGuaranteedMinimumMethod()) {
while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
// Perform value iteration until convergence
++valueIterationInvocations;
auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations);
lastValueIterationIterations = result.iterations;
overallIterations += result.iterations;
// Perform value iteration until convergence
++valueIterationInvocations;
auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations);
lastValueIterationIterations = result.iterations;
overallIterations += result.iterations;
if (result.status != SolverStatus::Converged) {
status = result.status;
} else {
bool intervalIterationNeeded = false;
currentVerificationIterations = 0;
if (relative) {
oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler);
} else {
oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision);
}
bool cancelGuess = false;
while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
++overallIterations;
++currentVerificationIterations;
// Perform value iteration stepwise for lower bound and guessed upper bound
// Upper bound iteration
singleIterationCallback(upperX, auxVector, overallIterations);
// At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones.
// Compare the new upper bound candidate with the old one
bool newUpperBoundAlwaysHigherEqual = true;
bool newUpperBoundAlwaysLowerEqual = true;
for (uint64_t i = 0; i < upperX->size(); ++i) {
if ((*upperX)[i] < (*auxVector)[i]) {
newUpperBoundAlwaysHigherEqual = false;
} else if ((*upperX)[i] != (*auxVector)[i]) {
newUpperBoundAlwaysLowerEqual = false;
std::swap((*upperX)[i], (*auxVector)[i]);
}
}
if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {
// 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) {
// 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;
if (relevantValues) {
reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative);
} else {
reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative);
}
if (reachedPrecision) {
status = SolverStatus::Converged;
break;
} else {
// From now on, we keep updating both bounds
intervalIterationNeeded = true;
}
}
// At this point, the old upper bounds (auxVector) are not needed anymore.
// Check whether we tried this guess for too long
ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
cancelGuess = true;
// In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision)
}
// Lower bound iteration (only if needed)
if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) {
singleIterationCallback(lowerX, auxVector, overallIterations);
// At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones.
// Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound.
bool valuesCrossed = false;
for (uint64_t i = 0; i < lowerX->size(); ++i) {
if ((*upperX)[i] < (*lowerX)[i]) {
valuesCrossed = true;
break;
}
}
if (cancelGuess || valuesCrossed) {
// A new guess is needed.
iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues);
break;
}
}
}
}
}
}
else {
while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
// Perform value iteration until convergence
++valueIterationInvocations;
auto result = valueIterationCallback(lowerX, auxVector, iterationPrecision, relative, overallIterations, maxOverallIterations);
lastValueIterationIterations = result.iterations;
overallIterations += result.iterations;
if (result.status != SolverStatus::Converged) {
status = result.status;
} else {
bool intervalIterationNeeded = false;
currentVerificationIterations = 0;
if (result.status != SolverStatus::Converged) {
status = result.status;
if (relative) {
oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler);
} else {
bool intervalIterationNeeded = false;
currentVerificationIterations = 0;
if (relative) {
oviinternal::guessUpperBoundRelative(*lowerX, *upperX, relativeBoundGuessingScaler);
} else {
oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision);
}
bool cancelGuess = false;
while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
++overallIterations;
++currentVerificationIterations;
// Perform value iteration stepwise for lower bound and guessed upper bound
oviinternal::guessUpperBoundAbsolute(*lowerX, *upperX, precision);
}
// Upper bound iteration
singleIterationCallback(upperX, auxVector, overallIterations);
bool cancelGuess = false;
while (status == SolverStatus::InProgress && overallIterations < maxOverallIterations) {
++overallIterations;
++currentVerificationIterations;
// Perform value iteration stepwise for lower bound and guessed upper bound
// At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones.
// Upper bound iteration
singleIterationCallback(upperX, auxVector, overallIterations);
// At this point,h auxVector contains the old values for the upper bound whereas upperX contains the new ones.
// Compare the new upper bound candidate with the old one
bool newUpperBoundAlwaysHigherEqual = true;
bool newUpperBoundAlwaysLowerEqual = true;
// Compare the new upper bound candidate with the old one
bool newUpperBoundAlwaysHigherEqual = true;
bool newUpperBoundAlwaysLowerEqual = true;
if(noTerminationGuarantee) {
bool cancelOuterScan = false;
for (uint64_t i = 0; i < upperX->size() &! cancelOuterScan; ++i) {
if ((*upperX)[i] < (*auxVector)[i]) {
@ -288,8 +188,8 @@ namespace storm {
newUpperBoundAlwaysLowerEqual = false;
++i;
while (i < upperX->size()) {
if ((*upperX)[i] > (*auxVector)[i]) {
newUpperBoundAlwaysLowerEqual = false;
if ((*upperX)[i] < (*auxVector)[i]) {
newUpperBoundAlwaysHigherEqual = false;
cancelOuterScan = true;
break;
}
@ -297,61 +197,71 @@ namespace storm {
}
}
}
if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {
// 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) {
// 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;
if (relevantValues) {
reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative);
} else {
reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative);
}
if (reachedPrecision) {
status = SolverStatus::Converged;
break;
} else {
// From now on, we keep updating both bounds
intervalIterationNeeded = true;
}
else {
for (uint64_t i = 0; i < upperX->size(); ++i) {
if ((*upperX)[i] < (*auxVector)[i]) {
newUpperBoundAlwaysHigherEqual = false;
} else if ((*upperX)[i] != (*auxVector)[i]) {
newUpperBoundAlwaysLowerEqual = false;
std::swap((*upperX)[i], (*auxVector)[i]);
}
}
// At this point, the old upper bounds (auxVector) are not needed anymore.
}
// Check whether we tried this guess for too long
ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
cancelGuess = true;
// In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision)
if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {
// 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) {
// 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;
if (relevantValues) {
reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, relevantValues.get(), doublePrecision, relative);
} else {
reachedPrecision = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, doublePrecision, relative);
}
if (reachedPrecision) {
status = SolverStatus::Converged;
break;
} else {
// From now on, we keep updating both bounds
intervalIterationNeeded = true;
}
}
// At this point, the old upper bounds (auxVector) are not needed anymore.
// Lower bound iteration (only if needed)
if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) {
singleIterationCallback(lowerX, auxVector, overallIterations);
// At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones.
// Check whether we tried this guess for too long
ValueType scaledIterationCount = storm::utility::convertNumber<ValueType>(currentVerificationIterations) * storm::utility::convertNumber<ValueType>(env.solver().ovi().getMaxVerificationIterationFactor());
if (!intervalIterationNeeded && scaledIterationCount >= storm::utility::convertNumber<ValueType>(lastValueIterationIterations)) {
cancelGuess = true;
// In this case we will make one more iteration on the lower bound (mainly to obtain a new iterationPrecision)
}
// Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound.
bool valuesCrossed = false;
for (uint64_t i = 0; i < lowerX->size(); ++i) {
if ((*upperX)[i] < (*lowerX)[i]) {
valuesCrossed = true;
break;
}
}
// Lower bound iteration (only if needed)
if (cancelGuess || intervalIterationNeeded || currentVerificationIterations > upperBoundOnlyIterations) {
singleIterationCallback(lowerX, auxVector, overallIterations);
// At this point, auxVector contains the old values for the lower bound whereas lowerX contains the new ones.
if (cancelGuess || valuesCrossed) {
// A new guess is needed.
iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues);
// Check whether the upper and lower bounds have crossed, i.e., the upper bound is smaller than the lower bound.
bool valuesCrossed = false;
for (uint64_t i = 0; i < lowerX->size(); ++i) {
if ((*upperX)[i] < (*lowerX)[i]) {
valuesCrossed = true;
break;
}
}
if (cancelGuess || valuesCrossed) {
// A new guess is needed.
iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *lowerX, relative, relevantValues);
break;
}
}
}
}

Write Preview
Loading…
Cancel
Save