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

1. Ensured that when doing policy iteration the underlying solver is at least as precise as the minmax solver. 

2. Fix for SolverGuarantees: They are only established if bounds were actually given.
tempestpy_adaptions
TimQu 7 years ago
parent
3458e42d05
commit
e46f4e154b
5 changed files with 77 additions and 20 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. 21
      src/storm/environment/solver/SolverEnvironment.cpp
  2. 2
      src/storm/environment/solver/SolverEnvironment.h
  3. 28
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  4. 25
      src/storm/solver/NativeLinearEquationSolver.cpp
  5. 21
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

21
src/storm/environment/solver/SolverEnvironment.cpp
View File

@ -87,15 +87,30 @@ namespace storm {
return linearEquationSolverTypeSetFromDefault;
}
boost::optional<storm::RationalNumber> SolverEnvironment::getPrecisionOfCurrentLinearEquationSolver() const {
switch (getLinearEquationSolverType()) {
case storm::solver::EquationSolverType::Gmmxx:
return gmmxx().getPrecision();
case storm::solver::EquationSolverType::Eigen:
return eigen().getPrecision();
case storm::solver::EquationSolverType::Native:
return native().getPrecision();
case storm::solver::EquationSolverType::Elimination:
return boost::none;
default:
STORM_LOG_ASSERT(false, "The selected solver type is unknown.");
}
}
void SolverEnvironment::setLinearEquationSolverPrecision(storm::RationalNumber const& value) {
STORM_LOG_ASSERT(getLinearEquationSolverType() == storm::solver::EquationSolverType::Native ||
getLinearEquationSolverType() == storm::solver::EquationSolverType::Gmmxx ||
getLinearEquationSolverType() == storm::solver::EquationSolverType::Eigen ||
getLinearEquationSolverType() == storm::solver::EquationSolverType::Elimination,
"The current solver type is not respected in this method.");
native().setPrecision(value);
gmmxx().setPrecision(value);
eigen().setPrecision(value);
native().setPrecision(value);
gmmxx().setPrecision(value);
eigen().setPrecision(value);
// Elimination solver does not have a precision
}

2
src/storm/environment/solver/SolverEnvironment.h
View File

@ -1,6 +1,7 @@
#pragma once
#include<memory>
#include <boost/optional.hpp>
#include "storm/environment/Environment.h"
#include "storm/environment/SubEnvironment.h"
@ -40,6 +41,7 @@ namespace storm {
void setLinearEquationSolverType(storm::solver::EquationSolverType const& value);
bool isLinearEquationSolverTypeSetFromDefaultValue() const;
boost::optional<storm::RationalNumber> getPrecisionOfCurrentLinearEquationSolver() const;
void setLinearEquationSolverPrecision(storm::RationalNumber const& value);
void setLinearEquationSolverRelativeTerminationCriterion(bool value);

28
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -5,6 +5,7 @@
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/utility/KwekMehlhorn.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
@ -52,7 +53,7 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool result = false;
switch (getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value)) {
switch (getMethod(env, storm::NumberTraits<ValueType>::IsExact)) {
case MinMaxMethod::ValueIteration:
if (env.solver().isForceSoundness()) {
result = solveEquationsSoundValueIteration(env, dir, x, b);
@ -112,13 +113,20 @@ namespace storm {
// The solver that we will use throughout the procedure.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver;
// The linear equation solver should be at least as precise as this solver
std::unique_ptr<storm::Environment> environmentOfSolver;
boost::optional<storm::RationalNumber> precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver();
if (!storm::NumberTraits<ValueType>::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) {
environmentOfSolver = std::make_unique<storm::Environment>(env);
environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision());
}
SolverStatus status = SolverStatus::InProgress;
uint64_t iterations = 0;
this->startMeasureProgress();
do {
// Solve the equation system for the 'DTMC'.
solveInducedEquationSystem(env, solver, scheduler, x, subB, b);
solveInducedEquationSystem(environmentOfSolver ? *environmentOfSolver : env, solver, scheduler, x, subB, b);
// Go through the multiplication result and see whether we can improve any of the choices.
bool schedulerImproved = false;
@ -189,7 +197,7 @@ namespace storm {
// Start by copying the requirements of the linear equation solver.
MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env));
auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
if (method == MinMaxMethod::ValueIteration) {
if (env.solver().isForceSoundness()) {
// Interval iteration requires a unique solution and lower+upper bounds
@ -295,7 +303,15 @@ namespace storm {
if (this->hasInitialScheduler()) {
// Solve the equation system induced by the initial scheduler.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolver;
solveInducedEquationSystem(env, linEqSolver, this->getInitialScheduler(), x, *auxiliaryRowGroupVector, b);
// The linear equation solver should be at least as precise as this solver
std::unique_ptr<storm::Environment> environmentOfSolver;
boost::optional<storm::RationalNumber> precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver();
if (!storm::NumberTraits<ValueType>::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) {
environmentOfSolver = std::make_unique<storm::Environment>(env);
environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision());
}
solveInducedEquationSystem(environmentOfSolver ? *environmentOfSolver : env, linEqSolver, this->getInitialScheduler(), x, *auxiliaryRowGroupVector, b);
// If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes
// always less-or-equal (greater-or-equal) than the actual solution.
guarantee = maximize(dir) ? SolverGuarantee::LessOrEqual : SolverGuarantee::GreaterOrEqual;
@ -308,10 +324,10 @@ namespace storm {
guarantee = SolverGuarantee::GreaterOrEqual;
}
} else if (this->hasCustomTerminationCondition()) {
if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::LessOrEqual)) {
if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::LessOrEqual) && this->hasLowerBound()) {
this->createLowerBoundsVector(x);
guarantee = SolverGuarantee::LessOrEqual;
} else if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::GreaterOrEqual)) {
} else if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::GreaterOrEqual) && this->hasUpperBound()) {
this->createUpperBoundsVector(x);
guarantee = SolverGuarantee::GreaterOrEqual;
}

25
src/storm/solver/NativeLinearEquationSolver.cpp
View File

@ -4,6 +4,7 @@
#include "storm/utility/ConstantsComparator.h"
#include "storm/utility/KwekMehlhorn.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/constants.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/InvalidStateException.h"
@ -312,7 +313,7 @@ namespace storm {
// Now check for termination.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative);
terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual);
terminate = this->terminateNow(*currentX, guarantee);
// Potentially show progress.
this->showProgressIterative(iterations);
@ -332,7 +333,6 @@ namespace storm {
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsPower(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Power)");
// Prepare the solution vectors.
@ -340,12 +340,22 @@ namespace storm {
this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
}
std::vector<ValueType>* currentX = &x;
SolverGuarantee guarantee = SolverGuarantee::None;
if (this->hasCustomTerminationCondition()) {
if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::LessOrEqual) && this->hasLowerBound()) {
this->createLowerBoundsVector(*currentX);
guarantee = SolverGuarantee::LessOrEqual;
} else if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::GreaterOrEqual) && this->hasUpperBound()) {
this->createUpperBoundsVector(*currentX);
guarantee = SolverGuarantee::GreaterOrEqual;
}
}
std::vector<ValueType>* newX = this->cachedRowVector.get();
// Forward call to power iteration implementation.
this->startMeasureProgress();
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().native().getPrecision());
PowerIterationResult result = this->performPowerIteration(currentX, newX, b, precision, env.solver().native().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, 0, env.solver().native().getMaximalNumberOfIterations(), env.solver().native().getPowerMethodMultiplicationStyle());
PowerIterationResult result = this->performPowerIteration(currentX, newX, b, precision, env.solver().native().getRelativeTerminationCriterion(), guarantee, 0, env.solver().native().getMaximalNumberOfIterations(), env.solver().native().getPowerMethodMultiplicationStyle());
// Swap the result in place.
if (currentX == this->cachedRowVector.get()) {
@ -387,11 +397,10 @@ namespace storm {
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundPower(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires lower bound, but none was given.");
STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (SoundPower)");
std::vector<ValueType>* lowerX = &x;
this->createLowerBoundsVector(*lowerX);
this->createUpperBoundsVector(this->cachedRowVector, this->getMatrixRowCount());
@ -833,7 +842,7 @@ namespace storm {
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
switch(getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value)) {
switch(getMethod(env, storm::NumberTraits<ValueType>::IsExact)) {
case NativeLinearEquationSolverMethod::SOR:
return this->solveEquationsSOR(env, x, b, storm::utility::convertNumber<ValueType>(env.solver().native().getSorOmega()));
case NativeLinearEquationSolverMethod::GaussSeidel:
@ -911,7 +920,7 @@ namespace storm {
template<typename ValueType>
LinearEquationSolverProblemFormat NativeLinearEquationSolver<ValueType>::getEquationProblemFormat(Environment const& env) const {
auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::RationalSearch) {
return LinearEquationSolverProblemFormat::FixedPointSystem;
} else {
@ -922,7 +931,7 @@ namespace storm {
template<typename ValueType>
LinearEquationSolverRequirements NativeLinearEquationSolver<ValueType>::getRequirements(Environment const& env) const {
LinearEquationSolverRequirements requirements;
auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
auto method = getMethod(env, storm::NumberTraits<ValueType>::IsExact);
if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) {
requirements.requireBounds();
} else if (method == NativeLinearEquationSolverMethod::RationalSearch) {

21
src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
View File

@ -241,7 +241,14 @@ namespace storm {
} else {
// If we were given an initial scheduler, we take its solution as the starting point.
if (this->hasInitialScheduler()) {
localX = solveEquationsWithScheduler(env, this->getInitialScheduler(), x, b);
// The linear equation solver should be at least as precise as this solver
std::unique_ptr<storm::Environment> environmentOfSolver;
boost::optional<storm::RationalNumber> precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver();
if (!storm::NumberTraits<ValueType>::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) {
environmentOfSolver = std::make_unique<storm::Environment>(env);
environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision());
}
localX = solveEquationsWithScheduler(environmentOfSolver ? *environmentOfSolver : env, this->getInitialScheduler(), x, b);
} else {
localX = this->getLowerBoundsVector();
}
@ -301,13 +308,21 @@ namespace storm {
storm::dd::Bdd<DdType> scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : this->A.sumAbstract(this->columnMetaVariables).maxAbstractRepresentative(this->choiceVariables);
// Initialize linear equation solver.
std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> linearEquationSolver = linearEquationSolverFactory->create(env, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
// It should be at least as precise as this solver.
std::unique_ptr<storm::Environment> environmentOfSolver;
boost::optional<storm::RationalNumber> precOfSolver = env.solver().getPrecisionOfCurrentLinearEquationSolver();
if (!storm::NumberTraits<ValueType>::IsExact && precOfSolver && precOfSolver.get() > env.solver().minMax().getPrecision()) {
environmentOfSolver = std::make_unique<storm::Environment>(env);
environmentOfSolver->solver().setLinearEquationSolverPrecision(env.solver().minMax().getPrecision());
}
std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> linearEquationSolver = linearEquationSolverFactory->create(environmentOfSolver ? *environmentOfSolver : env, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
this->forwardBounds(*linearEquationSolver);
// Iteratively solve and improve the scheduler.
uint64_t maxIter = env.solver().minMax().getMaximalNumberOfIterations();
while (!converged && iterations < maxIter) {
storm::dd::Add<DdType, ValueType> schedulerX = solveEquationsWithScheduler(env, *linearEquationSolver, scheduler, currentSolution, b, diagonal);
storm::dd::Add<DdType, ValueType> schedulerX = solveEquationsWithScheduler(environmentOfSolver ? *environmentOfSolver : env, *linearEquationSolver, scheduler, currentSolution, b, diagonal);
// Policy improvement step.
storm::dd::Add<DdType, ValueType> choiceValues = this->A.multiplyMatrix(schedulerX.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b;

Write Preview
Loading…
Cancel
Save