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

implemented linear equation solver restarts when a scheduler hint is given (to assert that equalModuloPrecision(Ax+b, x) holds.

tempestpy_adaptions
TimQu 8 years ago
parent
24bc53549c
commit
e88b215dbc
4 changed files with 121 additions and 6 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. 56
      src/storm/solver/GameSolver.cpp
  2. 65
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  3. 2
      src/storm/solver/StandardMinMaxLinearEquationSolver.h
  4. 4
      src/storm/storage/geometry/NativePolytope.cpp

56
src/storm/solver/GameSolver.cpp
View File

@ -6,6 +6,12 @@
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/solver/GmmxxLinearEquationSolver.h"
#include "storm/solver/EigenLinearEquationSolver.h"
#include "storm/solver/NativeLinearEquationSolver.h"
#include "storm/solver/EliminationLinearEquationSolver.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace solver {
template <typename ValueType>
@ -37,16 +43,62 @@ namespace storm {
auto const& pl1Row = player1Matrix.getRow(pl1State, this->player1SchedulerHint->getChoice(pl1State));
STORM_LOG_ASSERT(pl1Row.getNumberOfEntries()==1, "We assume that rows of player one have one entry.");
uint_fast64_t pl2State = pl1Row.begin()->getColumn();
selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + this->player2SchedulerHint->getChoice(pl1State);
selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + this->player2SchedulerHint->getChoice(pl2State);
}
//Get the matrix and the vector induced by this selection
auto inducedMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true);
inducedMatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(tmpResult, selectedRows, b);
// Solve the resulting equation system.
// Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.
auto submatrixSolver = storm::solver::GeneralLinearEquationSolverFactory<ValueType>().create(std::move(inducedMatrix));
submatrixSolver->setCachingEnabled(true);
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
submatrixSolver->solveEquations(x, tmpResult);
ValueType linEqPrecision = this->getPrecision();
uint_fast64_t hintIterations = 0;
std::vector<ValueType> otherTmpResult(tmpResult.size());
bool vectorsNotEqual = false;
do {
vectorsNotEqual = false;
// Set the precision of the underlying solver
auto* gmmSolver = dynamic_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(submatrixSolver.get());
auto* nativeSolver = dynamic_cast<storm::solver::NativeLinearEquationSolver<ValueType>*>(submatrixSolver.get());
auto* eigenSolver = dynamic_cast<storm::solver::EigenLinearEquationSolver<ValueType>*>(submatrixSolver.get());
auto* eliminationSolver = dynamic_cast<storm::solver::EliminationLinearEquationSolver<ValueType>*>(submatrixSolver.get());
if (gmmSolver) {
auto newSettings = gmmSolver->getSettings();
newSettings.setPrecision(linEqPrecision);
gmmSolver->setSettings(newSettings);
} else if (nativeSolver) {
auto newSettings = nativeSolver->getSettings();
newSettings.setPrecision(linEqPrecision);
nativeSolver->setSettings(newSettings);
} else if (eigenSolver) {
eigenSolver->getSettings().setPrecision(linEqPrecision);
} else if (eliminationSolver) {
// elimination solver does not consider a precision so nothing to do
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Changing the precision for the given linear equation solver type is not implemented");
}
// invoke the solver
submatrixSolver->solveEquations(x, tmpResult);
submatrixSolver->multiply(x, nullptr, otherTmpResult);
linEqPrecision *= storm::utility::convertNumber<ValueType>(0.5);
++hintIterations;
auto otherTmpResIt = otherTmpResult.begin();
auto xIt = x.begin();
for(auto tmpResIt = tmpResult.begin(); tmpResIt != tmpResult.end(); ++tmpResIt) {
if (!storm::utility::vector::equalModuloPrecision(*tmpResIt + *xIt, *otherTmpResIt + *xIt, this->getPrecision(), this->getRelative())) {
vectorsNotEqual = true;
break;
}
++otherTmpResIt; ++xIt;
}
} while (vectorsNotEqual);
STORM_LOG_WARN_COND(hintIterations == 1, "required " << hintIterations << " linear equation solver invokations to apply the scheduler hints in GameSolver");
}
// Now perform the actual value iteration.

65
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -12,6 +12,7 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace solver {
@ -112,6 +113,7 @@ namespace storm {
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
auto solver = linearEquationSolverFactory->create(std::move(submatrix));
setPrecisionRelativeOfLinearEquationSolver(solver, this->getPrecision(), this->getRelative());
if (this->lowerBound) {
solver->setLowerBound(this->lowerBound.get());
}
@ -231,15 +233,42 @@ namespace storm {
}
if(this->schedulerHint) {
// Resolve the nondeterminism according to the scheduler hint and solve the resulting equation system.
// Resolve the nondeterminism according to the scheduler hint
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->schedulerHint->getChoices(), true);
submatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->schedulerHint->getChoices(), this->A.getRowGroupIndices(), b);
// Solve the resulting equation system.
// Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.
auto submatrixSolver = linearEquationSolverFactory->create(std::move(submatrix));
submatrixSolver->setCachingEnabled(true);
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
ValueType linEqPrecision = this->getPrecision();
// Temporarily shrink the auxiliary row vector
auxiliaryRowVector->resize(A.getRowGroupCount());
auxiliaryRowVector->reserve(A.getRowCount());
uint_fast64_t hintIterations = 0;
bool vectorsNotEqual = false;
do {
vectorsNotEqual = false;
setPrecisionRelativeOfLinearEquationSolver(submatrixSolver, linEqPrecision, this->getRelative());
submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
submatrixSolver->multiply(x, nullptr, *auxiliaryRowVector);
linEqPrecision *= storm::utility::convertNumber<ValueType>(0.5);
++hintIterations;
auto otherTmpResIt = auxiliaryRowVector->begin();
auto xIt = x.begin();
for(auto tmpResIt = auxiliaryRowGroupVector->begin(); tmpResIt != auxiliaryRowGroupVector->end(); ++tmpResIt) {
if (!storm::utility::vector::equalModuloPrecision(*tmpResIt + *xIt, *otherTmpResIt + *xIt, this->getPrecision(), this->getRelative())) {
vectorsNotEqual = true;
break;
}
++otherTmpResIt; ++xIt;
}
} while (vectorsNotEqual);
STORM_LOG_WARN_COND(hintIterations == 1, "required " << hintIterations << " linear equation solver invokations to apply the scheduler hint");
auxiliaryRowVector->resize(A.getRowCount());
}
std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
@ -348,6 +377,38 @@ namespace storm {
}
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, ValueType precision, bool relative) const {
auto* gmmSolver = dynamic_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(linEqSolver.get());
auto* nativeSolver = dynamic_cast<storm::solver::NativeLinearEquationSolver<ValueType>*>(linEqSolver.get());
auto* eigenSolver = dynamic_cast<storm::solver::EigenLinearEquationSolver<ValueType>*>(linEqSolver.get());
auto* eliminationSolver = dynamic_cast<storm::solver::EliminationLinearEquationSolver<ValueType>*>(linEqSolver.get());
if (gmmSolver) {
auto newSettings = gmmSolver->getSettings();
newSettings.setPrecision(precision);
newSettings.setRelativeTerminationCriterion(relative);
gmmSolver->setSettings(newSettings);
} else if (nativeSolver) {
auto newSettings = nativeSolver->getSettings();
newSettings.setPrecision(precision);
newSettings.setRelativeTerminationCriterion(relative);
nativeSolver->setSettings(newSettings);
} else if (eigenSolver) {
eigenSolver->getSettings().setPrecision(precision);
// no relative flag for eigen solver
} else if (eliminationSolver) {
// elimination solver does not consider a precision so nothing to do
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Changing the precision for the given linear equation solver type is not implemented");
}
}
template<>
void StandardMinMaxLinearEquationSolver<storm::RationalNumber>::setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalNumber>>& linEqSolver, storm::RationalNumber precision, bool relative) const {
// Intentionally left empty
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings<ValueType> const& StandardMinMaxLinearEquationSolver<ValueType>::getSettings() const {
return settings;

2
src/storm/solver/StandardMinMaxLinearEquationSolver.h
View File

@ -66,6 +66,8 @@ namespace storm {
Status updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations) const;
void reportStatus(Status status, uint64_t iterations) const;
void setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, ValueType precision, bool relative) const;
/// The settings of this solver.
StandardMinMaxLinearEquationSolverSettings<ValueType> settings;

4
src/storm/storage/geometry/NativePolytope.cpp
View File

@ -3,7 +3,7 @@
#include "storm/utility/macros.h"
#include "storm/utility/solver.h"
#include "storm/solver/Z3LPSolver.h"
#include "storm/solver/Z3LpSolver.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/geometry/nativepolytopeconversion/QuickHull.h"
#include "storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.h"
@ -42,7 +42,7 @@ namespace storm {
} else {
std::vector<EigenVector> eigenPoints;
eigenPoints.reserve(points.size());
for(auto const& p : points){
for (auto const& p : points){
eigenPoints.emplace_back(storm::adapters::EigenAdapter::toEigenVector(p));
}

Write Preview
Loading…
Cancel
Save