Browse Source

solvers updated, constants updated

Former-commit-id: 011251c695
main
sjunges 9 years ago
parent
commit
051ad702a7
  1. 4
      src/solver/EliminationLinearEquationSolver.cpp
  2. 2
      src/solver/EliminationLinearEquationSolver.h
  3. 13
      src/solver/GmmxxLinearEquationSolver.h
  4. 214
      src/solver/GmmxxMinMaxLinearEquationSolver.cpp
  5. 4
      src/solver/NativeLinearEquationSolver.cpp
  6. 222
      src/solver/NativeMinMaxLinearEquationSolver.cpp
  7. 16
      src/solver/Smt2SmtSolver.cpp
  8. 24
      src/solver/StandardMinMaxLinearEquationSolver.cpp
  9. 6
      src/solver/StandardMinMaxLinearEquationSolver.h
  10. 8
      src/solver/TopologicalMinMaxLinearEquationSolver.cpp
  11. 2
      src/solver/TopologicalMinMaxLinearEquationSolver.h
  12. 13
      src/utility/constants.cpp

4
src/solver/EliminationLinearEquationSolver.cpp

@ -56,7 +56,7 @@ namespace storm {
}
template<typename ValueType>
void EliminationLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool EliminationLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// FIXME: This solver will not work for all input systems. More concretely, the current implementation will
// not work for systems that have a 0 on the diagonal. This is not a restriction of this technique in general
// but arbitrary matrices require pivoting, which is not currently implemented.
@ -108,6 +108,8 @@ namespace storm {
if (localA) {
localA->convertToEquationSystem();
};
return true;
}
template<typename ValueType>

2
src/solver/EliminationLinearEquationSolver.h

@ -32,7 +32,7 @@ namespace storm {
virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& A) override;
virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& A) override;
virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual bool solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
EliminationLinearEquationSolverSettings<ValueType>& getSettings();

13
src/solver/GmmxxLinearEquationSolver.h

@ -102,18 +102,7 @@ namespace storm {
virtual bool deallocateAuxMemory(LinearEquationSolverOperation operation) const override;
virtual bool reallocateAuxMemory(LinearEquationSolverOperation operation) const override;
virtual bool hasAuxMemory(LinearEquationSolverOperation operation) const override;
virtual void setPrecision(double precision) override{
this->precision = precision;
}
virtual void setIterations(uint_fast64_t maximalNumberOfIterations) override{
this->maximalNumberOfIterations = maximalNumberOfIterations;
}
virtual void setRelative(bool relative) override{
this->relative = relative;
}
private:
/*!

214
src/solver/GmmxxMinMaxLinearEquationSolver.cpp

@ -1,214 +0,0 @@
#include "src/solver/GmmxxMinMaxLinearEquationSolver.h"
#include <utility>
#include "src/settings/SettingsManager.h"
#include "src/adapters/GmmxxAdapter.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/storage/TotalScheduler.h"
#include "src/utility/vector.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
namespace storm {
namespace solver {
template<typename ValueType>
GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) :
MinMaxLinearEquationSolver<ValueType>(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()) {
// Intentionally left empty.
}
template<typename ValueType>
GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver<ValueType>(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()) {
// Intentionally left empty.
}
template<typename ValueType>
void GmmxxMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
if (this->useValueIteration) {
// Set up the environment for the power method. If scratch memory was not provided, we need to create it.
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(b.size());
multiplyResultMemoryProvided = false;
}
std::vector<ValueType>* currentX = &x;
bool xMemoryProvided = true;
if (newX == nullptr) {
newX = new std::vector<ValueType>(x.size());
xMemoryProvided = false;
}
uint_fast64_t iterations = 0;
bool converged = false;
// Keep track of which of the vectors for x is the auxiliary copy.
std::vector<ValueType>* copyX = newX;
// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
// of iterations.
while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
// Compute x' = A*x + b.
gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult);
gmm::add(b, *multiplyResult);
// Reduce the vector x by applying min/max over all nondeterministic choices.
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices);
// Determine whether the method converged.
converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative);
// Update environment variables.
std::swap(currentX, newX);
++iterations;
}
// Check if the solver converged and issue a warning otherwise.
if (converged) {
STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
// is currently stored in currentX, but x is the output vector.
if (currentX == copyX) {
std::swap(x, *currentX);
}
if(this->trackScheduler){
if(iterations==0){ //may happen due to early termination. Then we need to compute x'= A*x+b
gmm::mult(*gmmxxMatrix, x, *multiplyResult);
gmm::add(b, *multiplyResult);
}
std::vector<uint_fast64_t> choices(x.size());
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, rowGroupIndices, &(choices));
this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(choices));
}
if (!xMemoryProvided) {
delete copyX;
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
} else {
// We will use Policy Iteration to solve the given system.
// We first guess an initial choice resolution which will be refined after each iteration.
std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupIndices().size() - 1);
// Create our own multiplyResult for solving the deterministic sub-instances.
std::vector<ValueType> deterministicMultiplyResult(rowGroupIndices.size() - 1);
std::vector<ValueType> subB(rowGroupIndices.size() - 1);
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(b.size());
multiplyResultMemoryProvided = false;
}
std::vector<ValueType>* currentX = &x;
bool xMemoryProvided = true;
if (newX == nullptr) {
newX = new std::vector<ValueType>(x.size());
xMemoryProvided = false;
}
uint_fast64_t iterations = 0;
bool converged = false;
// Keep track of which of the vectors for x is the auxiliary copy.
std::vector<ValueType>* copyX = newX;
// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
// of iterations.
while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
// Take the sub-matrix according to the current choices
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
submatrix.convertToEquationSystem();
GmmxxLinearEquationSolver<ValueType> gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Ilu, this->relative, 50);
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, rowGroupIndices, b);
// Copy X since we will overwrite it
std::copy(currentX->begin(), currentX->end(), newX->begin());
// Solve the resulting linear equation system
gmmLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult);
// Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration.
gmm::mult(*gmmxxMatrix, *newX, *multiplyResult);
gmm::add(b, *multiplyResult);
// Reduce the vector x by applying min/max over all nondeterministic choices.
// Here, we capture which choice was taken in each state, thereby refining our initial guess.
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(scheduler));
// Determine whether the method converged.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
// Update environment variables.
std::swap(currentX, newX);
++iterations;
}
// Check if the solver converged and issue a warning otherwise.
if (converged) {
STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) {
this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
}
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
// is currently stored in currentX, but x is the output vector.
if (currentX == copyX) {
std::swap(x, *currentX);
}
if (!xMemoryProvided) {
delete copyX;
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
}
}
template<typename ValueType>
void GmmxxMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(gmmxxMatrix->nr);
multiplyResultMemoryProvided = false;
}
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
for (uint_fast64_t i = 0; i < n; ++i) {
gmm::mult(*gmmxxMatrix, x, *multiplyResult);
if (b != nullptr) {
gmm::add(*b, *multiplyResult);
}
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, rowGroupIndices);
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
}
// Explicitly instantiate the solver.
template class GmmxxMinMaxLinearEquationSolver<double>;
} // namespace solver
} // namespace storm

4
src/solver/NativeLinearEquationSolver.cpp

@ -102,7 +102,7 @@ namespace storm {
template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool allocatedAuxStorage = !this->hasAuxMemory(LinearEquationSolverOperation::SolveEquations);
if (allocatedAuxStorage) {
this->allocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
@ -174,7 +174,7 @@ namespace storm {
if (allocatedAuxStorage) {
this->deallocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
}
return converged;
return iterationCount < this->getSettings().getMaximalNumberOfIterations();
}

222
src/solver/NativeMinMaxLinearEquationSolver.cpp

@ -1,222 +0,0 @@
#include "src/solver/NativeMinMaxLinearEquationSolver.h"
#include <utility>
#include "src/storage/TotalScheduler.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/utility/vector.h"
#include "src/solver/NativeLinearEquationSolver.h"
namespace storm {
namespace solver {
template<typename ValueType>
NativeMinMaxLinearEquationSolver<ValueType>::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) : MinMaxLinearEquationSolver<ValueType>(A, storm::settings::nativeEquationSolverSettings().getPrecision(), storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique) {
// Intentionally left empty.
}
template<typename ValueType>
NativeMinMaxLinearEquationSolver<ValueType>::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver<ValueType>(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech) {
// Intentionally left empty.
}
template<typename ValueType>
void NativeMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
if (this->useValueIteration) {
// Set up the environment for the power method. If scratch memory was not provided, we need to create it.
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(this->A.getRowCount());
multiplyResultMemoryProvided = false;
}
std::vector<ValueType>* currentX = &x;
bool xMemoryProvided = true;
if (newX == nullptr) {
newX = new std::vector<ValueType>(x.size());
xMemoryProvided = false;
}
uint_fast64_t iterations = 0;
bool converged = false;
// Keep track of which of the vectors for x is the auxiliary copy.
std::vector<ValueType>* copyX = newX;
// Proceed with the iterations as long as the method did not converge or reach the
// user-specified maximum number of iterations.
while (!converged && iterations < this->maximalNumberOfIterations && (!this->hasCustomTerminationCondition() || this->getTerminationCondition().terminateNow(*currentX))) {
// Compute x' = A*x + b.
this->A.multiplyWithVector(*currentX, *multiplyResult);
storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices());
// Determine whether the method converged.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
// Update environment variables.
std::swap(currentX, newX);
++iterations;
}
// Check if the solver converged and issue a warning otherwise.
if (converged) {
STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
// is currently stored in currentX, but x is the output vector.
if (currentX == copyX) {
std::swap(x, *currentX);
}
if(this->trackScheduler){
if(iterations==0){ //may happen due to early termination. Then we need to compute x'= A*x+b
this->A.multiplyWithVector(x, *multiplyResult);
storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
}
std::vector<uint_fast64_t> choices(x.size());
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices(), &(choices));
this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(choices));
}
if (!xMemoryProvided) {
delete copyX;
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
} else {
// We will use Policy Iteration to solve the given system.
// We first guess an initial choice resolution which will be refined after each iteration.
std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupIndices().size() - 1);
// Create our own multiplyResult for solving the deterministic sub-instances.
std::vector<ValueType> deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1);
std::vector<ValueType> subB(this->A.getRowGroupIndices().size() - 1);
// Check whether intermediate storage was provided and create it otherwise.
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(b.size());
multiplyResultMemoryProvided = false;
}
std::vector<ValueType>* currentX = &x;
bool xMemoryProvided = true;
if (newX == nullptr) {
newX = new std::vector<ValueType>(x.size());
xMemoryProvided = false;
}
uint_fast64_t iterations = 0;
bool converged = false;
// Keep track of which of the vectors for x is the auxiliary copy.
std::vector<ValueType>* copyX = newX;
// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
// of iterations.
while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
// Take the sub-matrix according to the current choices
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
submatrix.convertToEquationSystem();
NativeLinearEquationSolver<ValueType> nativeLinearEquationSolver(submatrix);
storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
// Copy X since we will overwrite it
std::copy(currentX->begin(), currentX->end(), newX->begin());
// Solve the resulting linear equation system of the sub-instance for x under the current choices
nativeLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult);
// Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration.
this->A.multiplyWithVector(*newX, *multiplyResult);
storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
// Reduce the vector x by applying min/max over all nondeterministic choices.
// Here, we capture which choice was taken in each state, thereby refining our initial guess.
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(scheduler));
// Determine whether the method converged.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
// Update environment variables.
std::swap(currentX, newX);
++iterations;
}
// Check if the solver converged and issue a warning otherwise.
if (converged) {
STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) {
this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
}
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
// is currently stored in currentX, but x is the output vector.
if (currentX == copyX) {
std::swap(x, *currentX);
}
if (!xMemoryProvided) {
delete copyX;
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
}
}
template<typename ValueType>
void NativeMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// If scratch memory was not provided, we need to create it.
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(this->A.getRowCount());
multiplyResultMemoryProvided = false;
}
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
for (uint_fast64_t i = 0; i < n; ++i) {
this->A.multiplyWithVector(x, *multiplyResult);
// Add b if it is non-null.
if (b != nullptr) {
storm::utility::vector::addVectors(*multiplyResult, *b, *multiplyResult);
}
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices());
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
}
// Explicitly instantiate the solver.
template class NativeMinMaxLinearEquationSolver<double>;
template class NativeMinMaxLinearEquationSolver<float>;
} // namespace solver
} // namespace storm

16
src/solver/Smt2SmtSolver.cpp

@ -91,7 +91,7 @@ namespace storm {
void Smt2SmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) {
STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions");
//if some of the occurring variables are not declared yet, we will have to.
std::set<storm::Variable> variables;
std::set<storm::RationalFunctionVariable> variables;
leftHandSide.gatherVariables(variables);
rightHandSide.gatherVariables(variables);
std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
@ -107,7 +107,7 @@ namespace storm {
void Smt2SmtSolver::add(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
//if some of the occurring variables are not declared yet, we will have to.
std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
for (auto declaration : varDeclarations){
writeCommand(declaration, true);
@ -118,7 +118,7 @@ namespace storm {
void Smt2SmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint){
STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool.");
//if some of the occurring variables are not declared yet, we will have to (including the guard!).
std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
variables.insert(guard);
std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
for (auto declaration : varDeclarations){
@ -130,7 +130,7 @@ namespace storm {
void Smt2SmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){
STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable.");
std::set<storm::Variable> variableSet;
std::set<storm::RationalFunctionVariable> variableSet;
variableSet.insert(variable);
std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variableSet);
for (auto declaration : varDeclarations){
@ -184,7 +184,7 @@ namespace storm {
#endif
void Smt2SmtSolver::init() {
if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){
if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isSolverCommandSet()){
#ifdef WINDOWS
STORM_LOG_WARN("opening a thread for the smt solver is not implemented on Windows. Hence, no actual solving will be done")
#else
@ -193,7 +193,7 @@ namespace storm {
//for executing the solver we will need the path to the executable file as well as the arguments as a char* array
//where the first argument is the path to the executable file and the last is NULL
const std::string cmdString = storm::settings::smt2SmtSolverSettings().getSolverCommand();
const std::string cmdString = storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getSolverCommand();
std::vector<std::string> solverCommandVec;
boost::split(solverCommandVec, cmdString, boost::is_any_of("\t "));
char** solverArgs = new char* [solverCommandVec.size()+1];
@ -243,9 +243,9 @@ namespace storm {
STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done");
}
if (storm::settings::smt2SmtSolverSettings().isExportSmtLibScriptSet()){
if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isExportSmtLibScriptSet()){
STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file");
commandFile.open(storm::settings::smt2SmtSolverSettings().getExportSmtLibScriptPath(), std::ios::trunc);
commandFile.open(storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getExportSmtLibScriptPath(), std::ios::trunc);
isCommandFileOpen=commandFile.is_open();
STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
}

24
src/solver/StandardMinMaxLinearEquationSolver.cpp

@ -84,15 +84,17 @@ namespace storm {
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
switch (this->getSettings().getSolutionMethod()) {
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration: solveEquationsValueIteration(dir, x, b); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: solveEquationsPolicyIteration(dir, x, b); break;
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration:
return solveEquationsValueIteration(dir, x, b);
case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
return solveEquationsPolicyIteration(dir, x, b);
}
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool StandardMinMaxLinearEquationSolver<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->A.getRowGroupCount());
@ -163,6 +165,12 @@ namespace storm {
if (this->isTrackSchedulerSet()) {
this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
}
if(status == Status::Converged || status == Status::TerminatedEarly) {
return true;
} else{
return false;
}
}
template<typename ValueType>
@ -181,7 +189,7 @@ namespace storm {
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory->create(A);
bool allocatedAuxMemory = !this->hasAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations);
if (allocatedAuxMemory) {
@ -225,6 +233,12 @@ namespace storm {
if (allocatedAuxMemory) {
this->deallocateAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations);
}
if(status == Status::Converged || status == Status::TerminatedEarly) {
return true;
} else{
return false;
}
}
template<typename ValueType>

6
src/solver/StandardMinMaxLinearEquationSolver.h

@ -38,7 +38,7 @@ namespace storm {
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
virtual void solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const override;
StandardMinMaxLinearEquationSolverSettings<ValueType> const& getSettings() const;
@ -49,8 +49,8 @@ namespace storm {
virtual bool hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const override;
private:
void solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
void solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;

8
src/solver/TopologicalMinMaxLinearEquationSolver.cpp

@ -33,7 +33,7 @@ namespace storm {
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
#ifdef GPU_USE_FLOAT
#define __FORCE_FLOAT_CALCULATION true
@ -49,12 +49,12 @@ namespace storm {
std::vector<float> new_x = storm::utility::vector::toValueType<float>(x);
std::vector<float> const new_b = storm::utility::vector::toValueType<float>(b);
newSolver.solveEquations(dir, new_x, new_b);
bool callConverged = newSolver.solveEquations(dir, new_x, new_b);
for (size_t i = 0, size = new_x.size(); i < size; ++i) {
x.at(i) = new_x.at(i);
}
return;
return callConverged;
}
// For testing only
@ -280,6 +280,8 @@ namespace storm {
} else {
STORM_LOG_WARN("Iterative solver did not converged after " << currentMaxLocalIterations << " iterations.");
}
return converged;
}
}

2
src/solver/TopologicalMinMaxLinearEquationSolver.h

@ -32,7 +32,7 @@ namespace storm {
*/
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
virtual void solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const override;

13
src/utility/constants.cpp

@ -50,12 +50,7 @@ namespace storm {
bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a);
}
template<>
storm::RationalNumber infinity() {
// FIXME: this should be treated more properly.
return storm::RationalNumber(-1);
}
template<>
bool isOne(storm::RationalFunction const& a) {
@ -277,7 +272,7 @@ namespace storm {
template bool isOne(storm::RationalNumber const& value);
template bool isZero(storm::RationalNumber const& value);
template bool isConstant(storm::RationalNumber const& value);
template storm::RationalNumber one();
template storm::RationalNumber zero();
template storm::RationalNumber infinity();
@ -308,10 +303,6 @@ namespace storm {
template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
template RationalNumber one();
template RationalNumber zero();
template RationalNumber infinity();
template Polynomial one();
template Polynomial zero();

Loading…
Cancel
Save