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

Fixed cases where a solver guarantee was not established although it was needed by the termination condition

tempestpy_adaptions
TimQu 7 years ago
parent
117d1b5c99
commit
d85a845b7d
4 changed files with 79 additions and 53 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. 94
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  2. 2
      src/storm/solver/IterativeMinMaxLinearEquationSolver.h
  3. 20
      src/storm/solver/TerminationCondition.cpp
  4. 16
      src/storm/solver/TerminationCondition.h

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

@ -146,40 +146,56 @@ namespace storm {
}
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Create the initial scheduler.
std::vector<storm::storage::sparse::state_type> scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : std::vector<storm::storage::sparse::state_type>(this->A->getRowGroupCount());
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveInducedEquationSystem(std::unique_ptr<LinearEquationSolver<ValueType>>& linearEquationSolver, std::vector<uint64_t> const& scheduler, std::vector<ValueType>& x, std::vector<ValueType>& subB, std::vector<ValueType> const& originalB) const {
assert(subB.size() == x.size());
// Get a vector for storing the right-hand side of the inner equation system.
if (!auxiliaryRowGroupVector) {
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
}
std::vector<ValueType>& subB = *auxiliaryRowGroupVector;
// Resolve the nondeterminism according to the current scheduler.
// Resolve the nondeterminism according to the given scheduler.
bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(scheduler, convertToEquationSystem);
if (convertToEquationSystem) {
submatrix.convertToEquationSystem();
}
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A->getRowGroupIndices(), b);
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A->getRowGroupIndices(), originalB);
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
auto solver = this->linearEquationSolverFactory->create(std::move(submatrix));
if (this->lowerBound) {
solver->setLowerBound(this->lowerBound.get());
// Check whether the linear equation solver is already initialized
if (!linearEquationSolver) {
// Initialize the equation solver
linearEquationSolver = this->linearEquationSolverFactory->create(std::move(submatrix));
if (this->lowerBound) { // TODO
linearEquationSolver->setLowerBound(this->lowerBound.get());
}
if (this->upperBound) {
solver->setUpperBound(this->upperBound.get());
linearEquationSolver->setUpperBound(this->upperBound.get());
}
linearEquationSolver->setCachingEnabled(true);
} else {
// If the equation solver is already initialized, it suffices to update the matrix
linearEquationSolver->setMatrix(std::move(submatrix));
}
// Solve the equation system for the 'DTMC' and return true upon success
return linearEquationSolver->solveEquations(x, subB);
}
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Create the initial scheduler.
std::vector<storm::storage::sparse::state_type> scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : std::vector<storm::storage::sparse::state_type>(this->A->getRowGroupCount());
// Get a vector for storing the right-hand side of the inner equation system.
if (!auxiliaryRowGroupVector) {
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
}
solver->setCachingEnabled(true);
std::vector<ValueType>& subB = *auxiliaryRowGroupVector;
// The solver that we will use throughout the procedure.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver;
SolverStatus status = SolverStatus::InProgress;
uint64_t iterations = 0;
this->startMeasureProgress();
do {
// Solve the equation system for the 'DTMC'.
solver->solveEquations(x, subB);
solveInducedEquationSystem(solver, scheduler, x, subB, b);
// Go through the multiplication result and see whether we can improve any of the choices.
bool schedulerImproved = false;
@ -212,14 +228,6 @@ namespace storm {
// If the scheduler did not improve, we are done.
if (!schedulerImproved) {
status = SolverStatus::Converged;
} else {
// Update the scheduler and the solver.
submatrix = this->A->selectRowsFromRowGroups(scheduler, true);
if (convertToEquationSystem) {
submatrix.convertToEquationSystem();
}
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A->getRowGroupIndices(), b);
solver->setMatrix(std::move(submatrix));
}
// Update environment variables.
@ -376,37 +384,25 @@ namespace storm {
SolverGuarantee guarantee = SolverGuarantee::None;
if (this->hasInitialScheduler()) {
// Resolve the nondeterminism according to the initial scheduler.
bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), convertToEquationSystem);
if (convertToEquationSystem) {
submatrix.convertToEquationSystem();
}
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->getInitialScheduler(), this->A->getRowGroupIndices(), b);
// Solve the resulting equation system.
auto submatrixSolver = this->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);
// Solve the equation system induced by the initial scheduler.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolver;
solveInducedEquationSystem(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.
if (dir == storm::OptimizationDirection::Maximize) {
guarantee = maximize(dir) ? SolverGuarantee::LessOrEqual : SolverGuarantee::GreaterOrEqual;
} else if (!this->hasUniqueSolution()) {
if (maximize(dir)) {
this->createLowerBoundsVector(x);
guarantee = SolverGuarantee::LessOrEqual;
} else {
this->createUpperBoundsVector(x);
guarantee = SolverGuarantee::GreaterOrEqual;
}
} else if (!this->hasUniqueSolution()) {
if (dir == storm::OptimizationDirection::Maximize) {
} else if (this->hasCustomTerminationCondition()) {
if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::LessOrEqual)) {
this->createLowerBoundsVector(x);
guarantee = SolverGuarantee::LessOrEqual;
} else {
} else if (this->getTerminationCondition().requiresGuarantee(SolverGuarantee::GreaterOrEqual)) {
this->createUpperBoundsVector(x);
guarantee = SolverGuarantee::GreaterOrEqual;
}

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

@ -67,12 +67,12 @@ namespace storm {
virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
private:
bool solveInducedEquationSystem(std::unique_ptr<LinearEquationSolver<ValueType>>& linearEquationSolver, std::vector<uint64_t> const& scheduler, std::vector<ValueType>& x, std::vector<ValueType>& subB, std::vector<ValueType> const& originalB) const;
bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
bool solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool solveEquationsSoundValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool solveEquationsAcyclic(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool solveEquationsRationalSearch(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
template<typename RationalType, typename ImpreciseType>

20
src/storm/solver/TerminationCondition.cpp
View File

@ -13,6 +13,11 @@ namespace storm {
return false;
}
template<typename ValueType>
bool NoTerminationCondition<ValueType>::requiresGuarantee(SolverGuarantee const&) const {
return false;
}
template<typename ValueType>
TerminateIfFilteredSumExceedsThreshold<ValueType>::TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict) : threshold(threshold), filter(filter), strict(strict) {
// Intentionally left empty.
@ -29,6 +34,11 @@ namespace storm {
return strict ? currentThreshold > this->threshold : currentThreshold >= this->threshold;
}
template<typename ValueType>
bool TerminateIfFilteredSumExceedsThreshold<ValueType>::requiresGuarantee(SolverGuarantee const& guarantee) const {
return guarantee == SolverGuarantee::LessOrEqual;
}
template<typename ValueType>
TerminateIfFilteredExtremumExceedsThreshold<ValueType>::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) {
// Intentionally left empty.
@ -45,6 +55,11 @@ namespace storm {
return this->strict ? currentValue > this->threshold : currentValue >= this->threshold;
}
template<typename ValueType>
bool TerminateIfFilteredExtremumExceedsThreshold<ValueType>::requiresGuarantee(SolverGuarantee const& guarantee) const {
return guarantee == SolverGuarantee::LessOrEqual;
}
template<typename ValueType>
TerminateIfFilteredExtremumBelowThreshold<ValueType>::TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold<ValueType>(filter, threshold, strict), useMinimum(useMinimum) {
// Intentionally left empty.
@ -61,6 +76,11 @@ namespace storm {
return this->strict ? currentValue < this->threshold : currentValue <= this->threshold;
}
template<typename ValueType>
bool TerminateIfFilteredExtremumBelowThreshold<ValueType>::requiresGuarantee(SolverGuarantee const& guarantee) const {
return guarantee == SolverGuarantee::GreaterOrEqual;
}
template class TerminateIfFilteredSumExceedsThreshold<double>;
template class TerminateIfFilteredExtremumExceedsThreshold<double>;
template class TerminateIfFilteredExtremumBelowThreshold<double>;

16
src/storm/solver/TerminationCondition.h
View File

@ -14,12 +14,19 @@ namespace storm {
* Retrieves whether the guarantee provided by the solver for the current result is sufficient to terminate.
*/
virtual bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const = 0;
/*!
* Retrieves whether the termination criterion requires the given guarantee in order to decide termination.
* @return
*/
virtual bool requiresGuarantee(SolverGuarantee const& guarantee) const = 0;
};
template<typename ValueType>
class NoTerminationCondition : public TerminationCondition<ValueType> {
public:
virtual bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const override;
virtual bool requiresGuarantee(SolverGuarantee const& guarantee) const override;
};
template<typename ValueType>
@ -27,7 +34,8 @@ namespace storm {
public:
TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict);
bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
bool terminateNow(std::vector<ValueType> const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const override;
virtual bool requiresGuarantee(SolverGuarantee const& guarantee) const override;
protected:
ValueType threshold;
@ -40,7 +48,8 @@ namespace storm {
public:
TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum);
bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const override;
virtual bool requiresGuarantee(SolverGuarantee const& guarantee) const override;
protected:
bool useMinimum;
@ -51,7 +60,8 @@ namespace storm {
public:
TerminateIfFilteredExtremumBelowThreshold(storm::storage::BitVector const& filter, bool strict, ValueType const& threshold, bool useMinimum);
bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const;
bool terminateNow(std::vector<ValueType> const& currentValue, SolverGuarantee const& guarantee = SolverGuarantee::None) const override;
virtual bool requiresGuarantee(SolverGuarantee const& guarantee) const override;
protected:
bool useMinimum;

Write Preview
Loading…
Cancel
Save