From 2d910b79ed9d6b508b1333c8f1133f67cead9982 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 Jan 2018 16:33:47 +0100 Subject: [PATCH] Introduced new topological min max solver --- src/storm/environment/SubEnvironment.cpp | 4 +- .../solver/MinMaxSolverEnvironment.cpp | 4 +- .../solver/MinMaxSolverEnvironment.h | 2 +- .../environment/solver/SolverEnvironment.cpp | 12 +- .../environment/solver/SolverEnvironment.h | 10 +- ...logicalLinearEquationSolverEnvironment.cpp | 37 -- ...pologicalLinearEquationSolverEnvironment.h | 24 - .../solver/TopologicalSolverEnvironment.cpp | 56 +++ .../solver/TopologicalSolverEnvironment.h | 31 ++ .../solver/MinMaxLinearEquationSolver.cpp | 2 + .../TopologicalLinearEquationSolver.cpp | 38 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 434 ++++++++++++++++++ .../TopologicalMinMaxLinearEquationSolver.h | 73 +++ .../DtmcPrctlModelCheckerTest.cpp | 4 +- .../modelchecker/MdpPrctlModelCheckerTest.cpp | 39 ++ .../storm/solver/LinearEquationSolverTest.cpp | 4 +- .../solver/MinMaxLinearEquationSolverTest.cpp | 4 + 17 files changed, 676 insertions(+), 102 deletions(-) delete mode 100644 src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.cpp delete mode 100644 src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h create mode 100644 src/storm/environment/solver/TopologicalSolverEnvironment.cpp create mode 100644 src/storm/environment/solver/TopologicalSolverEnvironment.h diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index 6227548e5..45c833110 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -5,7 +5,7 @@ #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/GameSolverEnvironment.h" -#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" namespace storm { @@ -41,7 +41,7 @@ namespace storm { template class SubEnvironment; template class SubEnvironment; template class SubEnvironment; - template class SubEnvironment; + template class SubEnvironment; } diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp index d44eac259..83ff18826 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp @@ -34,8 +34,8 @@ namespace storm { return methodSetFromDefault; } - void MinMaxSolverEnvironment::setMethod(storm::solver::MinMaxMethod value) { - methodSetFromDefault = false; + void MinMaxSolverEnvironment::setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault) { + methodSetFromDefault = isSetFromDefault; minMaxMethod = value; } diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index 999ed18bd..f7e0a24b1 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -16,7 +16,7 @@ namespace storm { storm::solver::MinMaxMethod const& getMethod() const; bool const& isMethodSetFromDefault() const; - void setMethod(storm::solver::MinMaxMethod value); + void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault = false); uint64_t const& getMaximalNumberOfIterations() const; void setMaximalNumberOfIterations(uint64_t value); storm::RationalNumber const& getPrecision() const; diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index b9635757c..5fc371072 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -5,7 +5,7 @@ #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/GameSolverEnvironment.h" -#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -68,11 +68,11 @@ namespace storm { return gameSolverEnvironment.get(); } - TopologicalLinearEquationSolverEnvironment& SolverEnvironment::topological() { + TopologicalSolverEnvironment& SolverEnvironment::topological() { return topologicalSolverEnvironment.get(); } - TopologicalLinearEquationSolverEnvironment const& SolverEnvironment::topological() const { + TopologicalSolverEnvironment const& SolverEnvironment::topological() const { return topologicalSolverEnvironment.get(); } @@ -88,8 +88,8 @@ namespace storm { return linearEquationSolverType; } - void SolverEnvironment::setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool assumeSetFromDefault) { - linearEquationSolverTypeSetFromDefault = assumeSetFromDefault; + void SolverEnvironment::setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool isSetFromDefault) { + linearEquationSolverTypeSetFromDefault = isSetFromDefault; linearEquationSolverType = value; } @@ -113,7 +113,7 @@ namespace storm { case storm::solver::EquationSolverType::Elimination: break; case storm::solver::EquationSolverType::Topological: - result = getPrecisionOfLinearEquationSolver(topological().getUnderlyingSolverType()); + result = getPrecisionOfLinearEquationSolver(topological().getUnderlyingEquationSolverType()); break; default: STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The selected solver type is unknown."); diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 614fd1d02..32c3cb648 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -16,7 +16,7 @@ namespace storm { class NativeSolverEnvironment; class MinMaxSolverEnvironment; class GameSolverEnvironment; - class TopologicalLinearEquationSolverEnvironment; + class TopologicalSolverEnvironment; class SolverEnvironment { public: @@ -34,14 +34,14 @@ namespace storm { MinMaxSolverEnvironment const& minMax() const; GameSolverEnvironment& game(); GameSolverEnvironment const& game() const; - TopologicalLinearEquationSolverEnvironment& topological(); - TopologicalLinearEquationSolverEnvironment const& topological() const; + TopologicalSolverEnvironment& topological(); + TopologicalSolverEnvironment const& topological() const; bool isForceSoundness() const; void setForceSoundness(bool value); storm::solver::EquationSolverType const& getLinearEquationSolverType() const; - void setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool assumeSetFromDefault = false); + void setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool isSetFromDefault = false); bool isLinearEquationSolverTypeSetFromDefaultValue() const; std::pair, boost::optional> getPrecisionOfLinearEquationSolver(storm::solver::EquationSolverType const& solverType) const; @@ -52,7 +52,7 @@ namespace storm { SubEnvironment gmmxxSolverEnvironment; SubEnvironment nativeSolverEnvironment; SubEnvironment gameSolverEnvironment; - SubEnvironment topologicalSolverEnvironment; + SubEnvironment topologicalSolverEnvironment; SubEnvironment minMaxSolverEnvironment; storm::solver::EquationSolverType linearEquationSolverType; diff --git a/src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.cpp b/src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.cpp deleted file mode 100644 index a0f3ac030..000000000 --- a/src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.cpp +++ /dev/null @@ -1,37 +0,0 @@ -#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" - -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/TopologicalEquationSolverSettings.h" -#include "storm/utility/macros.h" - -#include "storm/exceptions/InvalidArgumentException.h" - -namespace storm { - - TopologicalLinearEquationSolverEnvironment::TopologicalLinearEquationSolverEnvironment() { - auto const& topologicalSettings = storm::settings::getModule(); - underlyingSolverType = topologicalSettings.getUnderlyingEquationSolverType(); - underlyingSolverTypeSetFromDefault = topologicalSettings.isUnderlyingEquationSolverTypeSetFromDefaultValue(); - } - - TopologicalLinearEquationSolverEnvironment::~TopologicalLinearEquationSolverEnvironment() { - // Intentionally left empty - } - - storm::solver::EquationSolverType const& TopologicalLinearEquationSolverEnvironment::getUnderlyingSolverType() const { - return underlyingSolverType; - } - - bool const& TopologicalLinearEquationSolverEnvironment::isUnderlyingSolverTypeSetFromDefault() const { - return underlyingSolverTypeSetFromDefault; - } - - void TopologicalLinearEquationSolverEnvironment::setUnderlyingSolverType(storm::solver::EquationSolverType value) { - STORM_LOG_THROW(value != storm::solver::EquationSolverType::Topological, storm::exceptions::InvalidArgumentException, "Can not use the topological solver as underlying solver of the topological solver."); - underlyingSolverTypeSetFromDefault = false; - underlyingSolverType = value; - } - - - -} diff --git a/src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h b/src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h deleted file mode 100644 index b79ed66a9..000000000 --- a/src/storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h +++ /dev/null @@ -1,24 +0,0 @@ -#pragma once - -#include "storm/environment/solver/SolverEnvironment.h" - -#include "storm/solver/SolverSelectionOptions.h" - -namespace storm { - - class TopologicalLinearEquationSolverEnvironment { - public: - - TopologicalLinearEquationSolverEnvironment(); - ~TopologicalLinearEquationSolverEnvironment(); - - storm::solver::EquationSolverType const& getUnderlyingSolverType() const; - bool const& isUnderlyingSolverTypeSetFromDefault() const; - void setUnderlyingSolverType(storm::solver::EquationSolverType value); - - private: - storm::solver::EquationSolverType underlyingSolverType; - bool underlyingSolverTypeSetFromDefault; - }; -} - diff --git a/src/storm/environment/solver/TopologicalSolverEnvironment.cpp b/src/storm/environment/solver/TopologicalSolverEnvironment.cpp new file mode 100644 index 000000000..244adc1fa --- /dev/null +++ b/src/storm/environment/solver/TopologicalSolverEnvironment.cpp @@ -0,0 +1,56 @@ +#include "storm/environment/solver/TopologicalSolverEnvironment.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/TopologicalEquationSolverSettings.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + + TopologicalSolverEnvironment::TopologicalSolverEnvironment() { + auto const& topologicalSettings = storm::settings::getModule(); + underlyingEquationSolverType = topologicalSettings.getUnderlyingEquationSolverType(); + underlyingEquationSolverTypeSetFromDefault = topologicalSettings.isUnderlyingEquationSolverTypeSetFromDefaultValue(); + + std::cout << "Get topo env minmax from settings!!" << std::endl; + underlyingMinMaxMethod = storm::solver::MinMaxMethod::ValueIteration; + underlyingEquationSolverTypeSetFromDefault = false; + + } + + TopologicalSolverEnvironment::~TopologicalSolverEnvironment() { + // Intentionally left empty + } + + storm::solver::EquationSolverType const& TopologicalSolverEnvironment::getUnderlyingEquationSolverType() const { + return underlyingEquationSolverType; + } + + bool const& TopologicalSolverEnvironment::isUnderlyingEquationSolverTypeSetFromDefault() const { + return underlyingEquationSolverTypeSetFromDefault; + } + + void TopologicalSolverEnvironment::setUnderlyingEquationSolverType(storm::solver::EquationSolverType value) { + STORM_LOG_THROW(value != storm::solver::EquationSolverType::Topological, storm::exceptions::InvalidArgumentException, "Can not use the topological solver as underlying solver of the topological solver."); + underlyingEquationSolverTypeSetFromDefault = false; + underlyingEquationSolverType = value; + } + + storm::solver::MinMaxMethod const& TopologicalSolverEnvironment::getUnderlyingMinMaxMethod() const { + return underlyingMinMaxMethod; + } + + bool const& TopologicalSolverEnvironment::isUnderlyingMinMaxMethodSetFromDefault() const { + return underlyingMinMaxMethodSetFromDefault; + } + + void TopologicalSolverEnvironment::setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod value) { + STORM_LOG_THROW(value != storm::solver::MinMaxMethod::Topological, storm::exceptions::InvalidArgumentException, "Can not use the topological solver as underlying solver of the topological solver."); + underlyingMinMaxMethodSetFromDefault = false; + underlyingMinMaxMethod = value; + } + + + +} diff --git a/src/storm/environment/solver/TopologicalSolverEnvironment.h b/src/storm/environment/solver/TopologicalSolverEnvironment.h new file mode 100644 index 000000000..594dd3d86 --- /dev/null +++ b/src/storm/environment/solver/TopologicalSolverEnvironment.h @@ -0,0 +1,31 @@ +#pragma once + +#include "storm/environment/solver/SolverEnvironment.h" + +#include "storm/solver/SolverSelectionOptions.h" + +namespace storm { + + class TopologicalSolverEnvironment { + public: + + TopologicalSolverEnvironment(); + ~TopologicalSolverEnvironment(); + + storm::solver::EquationSolverType const& getUnderlyingEquationSolverType() const; + bool const& isUnderlyingEquationSolverTypeSetFromDefault() const; + void setUnderlyingEquationSolverType(storm::solver::EquationSolverType value); + + storm::solver::MinMaxMethod const& getUnderlyingMinMaxMethod() const; + bool const& isUnderlyingMinMaxMethodSetFromDefault() const; + void setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod value); + + private: + storm::solver::EquationSolverType underlyingEquationSolverType; + bool underlyingEquationSolverTypeSetFromDefault; + + storm::solver::MinMaxMethod underlyingMinMaxMethod; + bool underlyingMinMaxMethodSetFromDefault; + }; +} + diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 4a5066079..3c76d2f9e 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -199,6 +199,8 @@ namespace storm { auto method = env.solver().minMax().getMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { result = std::make_unique>(std::make_unique>()); + } else if (method == MinMaxMethod::Topological) { + result = std::make_unique>(); } else if (method == MinMaxMethod::TopologicalCuda) { result = std::make_unique>(); } else if (method == MinMaxMethod::LinearProgramming) { diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index 9f6dcdebf..83825d562 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -1,6 +1,6 @@ #include "storm/solver/TopologicalLinearEquationSolver.h" -#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" @@ -43,7 +43,7 @@ namespace storm { template storm::Environment TopologicalLinearEquationSolver::getEnvironmentForUnderlyingSolver(storm::Environment const& env, bool adaptPrecision) const { storm::Environment subEnv(env); - subEnv.solver().setLinearEquationSolverType(env.solver().topological().getUnderlyingSolverType(), env.solver().topological().isUnderlyingSolverTypeSetFromDefault()); + subEnv.solver().setLinearEquationSolverType(env.solver().topological().getUnderlyingEquationSolverType(), env.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault()); if (adaptPrecision) { STORM_LOG_ASSERT(this->longestSccChainSize, "Did not compute the longest SCC chain size although it is needed."); auto subEnvPrec = subEnv.solver().getPrecisionOfLinearEquationSolver(subEnv.solver().getLinearEquationSolverType()); @@ -54,14 +54,9 @@ namespace storm { template bool TopologicalLinearEquationSolver::internalSolveEquations(Environment const& env, std::vector& x, std::vector const& b) const { - //std::cout << "Solving equation system with fixpoint characterization " << std::endl; - //std::cout << *this->A << std::endl; - //std::cout << storm::utility::vector::toString(b) << std::endl; - //std::cout << "Initial solution vector: " << std::endl; - //std::cout << storm::utility::vector::toString(x) << std::endl; // For sound computations we need to increase the precision in each SCC - bool needAdaptPrecision = env.solver().isForceSoundness() && env.solver().getPrecisionOfLinearEquationSolver(env.solver().topological().getUnderlyingSolverType()).first.is_initialized(); + bool needAdaptPrecision = env.solver().isForceSoundness() && env.solver().getPrecisionOfLinearEquationSolver(env.solver().topological().getUnderlyingEquationSolverType()).first.is_initialized(); if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { STORM_LOG_TRACE("Creating SCC decomposition."); @@ -88,21 +83,21 @@ namespace storm { } // Handle the case where there is just one large SCC - if (this->sortedSccDecomposition->size() == 1) { - return solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b); - } - - storm::storage::BitVector sccAsBitVector(x.size(), false); bool returnValue = true; - for (auto const& scc : *this->sortedSccDecomposition) { - if (scc.isTrivial()) { - returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; - } else { - sccAsBitVector.clear(); - for (auto const& state : scc) { - sccAsBitVector.set(state, true); + if (this->sortedSccDecomposition->size() == 1) { + returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, x, b); + } else { + storm::storage::BitVector sccAsBitVector(x.size(), false); + for (auto const& scc : *this->sortedSccDecomposition) { + if (scc.isTrivial()) { + returnValue = solveTrivialScc(*scc.begin(), x, b) && returnValue; + } else { + sccAsBitVector.clear(); + for (auto const& state : scc) { + sccAsBitVector.set(state, true); + } + returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue; } - returnValue = solveScc(sccSolverEnvironment, sccAsBitVector, x, b) && returnValue; } } @@ -373,6 +368,7 @@ namespace storm { template void TopologicalLinearEquationSolver::clearCache() const { sortedSccDecomposition.reset(); + longestSccChainSize = boost::none; sccSolver.reset(); LinearEquationSolver::clearCache(); } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index e69de29bb..0e285c82e 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -0,0 +1,434 @@ +#include "storm/solver/TopologicalMinMaxLinearEquationSolver.h" + +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" + +#include "storm/utility/constants.h" +#include "storm/utility/vector.h" +#include "storm/exceptions/InvalidStateException.h" +#include "storm/exceptions/InvalidEnvironmentException.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/UnmetRequirementException.h" + +namespace storm { + namespace solver { + + template + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver() : localA(nullptr), A(nullptr) { + // Intentionally left empty. + } + + template + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : localA(nullptr), A(nullptr) { + this->setMatrix(A); + } + + template + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A) : localA(nullptr), A(nullptr) { + this->setMatrix(std::move(A)); + } + + template + void TopologicalMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { + localA.reset(); + this->A = &A; + clearCache(); + } + + template + void TopologicalMinMaxLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { + localA = std::make_unique>(std::move(A)); + this->A = localA.get(); + clearCache(); + } + + template + storm::Environment TopologicalMinMaxLinearEquationSolver::getEnvironmentForUnderlyingSolver(storm::Environment const& env, bool adaptPrecision) const { + storm::Environment subEnv(env); + subEnv.solver().minMax().setMethod(env.solver().topological().getUnderlyingMinMaxMethod(), env.solver().topological().isUnderlyingMinMaxMethodSetFromDefault()); + if (adaptPrecision) { + STORM_LOG_ASSERT(this->longestSccChainSize, "Did not compute the longest SCC chain size although it is needed."); + storm::RationalNumber subEnvPrec = subEnv.solver().minMax().getPrecision() / storm::utility::convertNumber(this->longestSccChainSize.get()); + subEnv.solver().minMax().setPrecision(subEnvPrec); + } + return subEnv; + } + + template + bool TopologicalMinMaxLinearEquationSolver::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + STORM_LOG_ASSERT(x.size() == this->A->getRowGroupCount(), "Provided x-vector has invalid size."); + STORM_LOG_ASSERT(b.size() == this->A->getRowCount(), "Provided b-vector has invalid size."); + + //std::cout << "Solving equation system with fixpoint characterization " << std::endl; + //std::cout << *this->A << std::endl; + //std::cout << storm::utility::vector::toString(b) << std::endl; + //std::cout << "Initial solution vector: " << std::endl; + //std::cout << storm::utility::vector::toString(x) << std::endl; + + // For sound computations we need to increase the precision in each SCC + bool needAdaptPrecision = env.solver().isForceSoundness(); + + if (!this->sortedSccDecomposition || (needAdaptPrecision && !this->longestSccChainSize)) { + STORM_LOG_TRACE("Creating SCC decomposition."); + createSortedSccDecomposition(needAdaptPrecision); + } + + //std::cout << "Sorted SCC decomposition: " << std::endl; + //for (auto const& scc : *this->sortedSccDecomposition) { + //std::cout << "SCC: "; + // for (auto const& row : scc) { + //std::cout << row << " "; + // } + //std::cout << std::endl; + //} + + // We do not need to adapt the precision if all SCCs are trivial (i.e., the system is acyclic) + needAdaptPrecision = needAdaptPrecision && (this->sortedSccDecomposition->size() != this->A->getRowGroupCount()); + + storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision); + + std::cout << "Found " << this->sortedSccDecomposition->size() << "SCCs. Average size is " << static_cast(this->A->getRowGroupCount()) / static_cast(this->sortedSccDecomposition->size()) << "." << std::endl; + if (this->longestSccChainSize) { + std::cout << "Longest SCC chain size is " << this->longestSccChainSize.get() << std::endl; + } + + bool returnValue = true; + if (this->sortedSccDecomposition->size() == 1) { + // Handle the case where there is just one large SCC + returnValue = solveFullyConnectedEquationSystem(sccSolverEnvironment, dir, x, b); + } else { + if (this->isTrackSchedulerSet()) { + if (this->schedulerChoices) { + this->schedulerChoices.get().resize(x.size()); + } else { + this->schedulerChoices = std::vector(x.size()); + } + } + storm::storage::BitVector sccRowGroupsAsBitVector(x.size(), false); + storm::storage::BitVector sccRowsAsBitVector(b.size(), false); + for (auto const& scc : *this->sortedSccDecomposition) { + if (scc.isTrivial()) { + returnValue = solveTrivialScc(*scc.begin(), dir, x, b) && returnValue; + } else { + sccRowGroupsAsBitVector.clear(); + sccRowsAsBitVector.clear(); + for (auto const& group : scc) { + sccRowGroupsAsBitVector.set(group, true); + for (uint64_t row = this->A->getRowGroupIndices()[group]; row < this->A->getRowGroupIndices()[group + 1]; ++row) { + sccRowsAsBitVector.set(row, true); + } + } + returnValue = solveScc(sccSolverEnvironment, dir, sccRowGroupsAsBitVector, sccRowsAsBitVector, x, b) && returnValue; + } + } + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + if (!auxiliaryRowGroupVector) { + auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); + } + this->schedulerChoices = std::vector(this->A->getRowGroupCount()); + this->A->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get()); + } + } + + if (!this->isCachingEnabled()) { + clearCache(); + } + + return returnValue; + } + + template + void TopologicalMinMaxLinearEquationSolver::createSortedSccDecomposition(bool needLongestChainSize) const { + // Obtain the scc decomposition + auto sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*this->A); + + // Get a mapping from matrix row to the corresponding scc + STORM_LOG_THROW(sccDecomposition.size() < std::numeric_limits::max(), storm::exceptions::UnexpectedException, "The number of SCCs is too large."); + std::vector sccIndices(this->A->getRowCount(), std::numeric_limits::max()); + uint32_t sccIndex = 0; + for (auto const& scc : sccDecomposition) { + for (auto const& row : scc) { + sccIndices[row] = sccIndex; + } + ++sccIndex; + } + + // Prepare the resulting set of sorted sccs + this->sortedSccDecomposition = std::make_unique>(); + std::vector& sortedSCCs = *this->sortedSccDecomposition; + sortedSCCs.reserve(sccDecomposition.size()); + + // Find a topological sort via DFS. + storm::storage::BitVector unsortedSCCs(sccDecomposition.size(), true); + std::vector sccStack, chainSizes; + if (needLongestChainSize) { + chainSizes.resize(sccDecomposition.size(), 1u); + } + uint32_t longestChainSize = 0; + uint32_t const token = std::numeric_limits::max(); + std::set successorSCCs; + + for (uint32_t firstUnsortedScc = 0; firstUnsortedScc < unsortedSCCs.size(); firstUnsortedScc = unsortedSCCs.getNextSetIndex(firstUnsortedScc + 1)) { + + sccStack.push_back(firstUnsortedScc); + while (!sccStack.empty()) { + uint32_t currentSccIndex = sccStack.back(); + if (currentSccIndex != token) { + // Check whether the SCC is still unprocessed + if (unsortedSCCs.get(currentSccIndex)) { + // Explore the successors of the scc. + storm::storage::StronglyConnectedComponent const& currentScc = sccDecomposition.getBlock(currentSccIndex); + // We first push a token on the stack in order to recognize later when all successors of this SCC have been explored already. + sccStack.push_back(token); + // Now add all successors that are not already sorted. + // Successors should only be added once, so we first prepare a set of them and add them afterwards. + successorSCCs.clear(); + for (auto const& row : currentScc) { + for (auto const& entry : this->A->getRow(row)) { + auto const& successorSCC = sccIndices[entry.getColumn()]; + if (successorSCC != currentSccIndex && unsortedSCCs.get(successorSCC)) { + successorSCCs.insert(successorSCC); + } + } + } + sccStack.insert(sccStack.end(), successorSCCs.begin(), successorSCCs.end()); + + } + } else { + // all successors of the current scc have already been explored. + sccStack.pop_back(); // pop the token + + currentSccIndex = sccStack.back(); + storm::storage::StronglyConnectedComponent& scc = sccDecomposition.getBlock(currentSccIndex); + + // Compute the longest chain size for this scc + if (needLongestChainSize) { + uint32_t& currentChainSize = chainSizes[currentSccIndex]; + for (auto const& row : scc) { + for (auto const& entry : this->A->getRow(row)) { + auto const& successorSCC = sccIndices[entry.getColumn()]; + if (successorSCC != currentSccIndex) { + currentChainSize = std::max(currentChainSize, chainSizes[successorSCC] + 1); + } + } + } + longestChainSize = std::max(longestChainSize, currentChainSize); + } + + unsortedSCCs.set(currentSccIndex, false); + sccStack.pop_back(); // pop the current scc index + sortedSCCs.push_back(std::move(scc)); + } + } + } + + if (longestChainSize > 0) { + this->longestSccChainSize = longestChainSize; + } + } + + template + bool TopologicalMinMaxLinearEquationSolver::solveTrivialScc(uint64_t const& sccState, OptimizationDirection dir, std::vector& globalX, std::vector const& globalB) const { + ValueType& xi = globalX[sccState]; + bool firstRow = true; + uint64_t bestRow; + + for (uint64_t row = this->A->getRowGroupIndices()[sccState]; row < this->A->getRowGroupIndices()[sccState + 1]; ++row) { + ValueType rowValue = globalB[sccState]; + bool hasDiagonalEntry = false; + ValueType denominator; + for (auto const& entry : this->A->getRow(sccState)) { + if (entry.getColumn() == sccState) { + STORM_LOG_ASSERT(!storm::utility::isOne(entry.getValue()), "Diagonal entry of fix point system has value 1."); + hasDiagonalEntry = true; + denominator = storm::utility::one() - entry.getValue(); + } else { + rowValue += entry.getValue() * globalX[entry.getColumn()]; + } + } + if (hasDiagonalEntry) { + rowValue /= denominator; + } + if (firstRow) { + xi = std::move(rowValue); + bestRow = row; + firstRow = false; + } else { + if (minimize(dir)) { + if (rowValue < xi) { + xi = std::move(rowValue); + bestRow = row; + } + } else { + if (rowValue > xi) { + xi = std::move(rowValue); + bestRow = row; + } + } + } + } + if (this->isTrackSchedulerSet()) { + this->schedulerChoices.get()[sccState] = bestRow - this->A->getRowGroupIndices()[sccState]; + } + //std::cout << "Solved trivial scc " << sccState << " with result " << globalX[sccState] << std::endl; + return true; + } + + template + bool TopologicalMinMaxLinearEquationSolver::solveFullyConnectedEquationSystem(storm::Environment const& sccSolverEnvironment, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + if (!this->sccSolver) { + this->sccSolver = GeneralMinMaxLinearEquationSolverFactory().create(sccSolverEnvironment); + this->sccSolver->setCachingEnabled(true); + } + this->sccSolver->setMatrix(*this->A); + this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution()); + this->sccSolver->setBoundsFromOtherSolver(*this); + this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet()); + if (this->hasInitialScheduler()) { + auto choices = this->getInitialScheduler(); + this->sccSolver->setInitialScheduler(std::move(choices)); + } + auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); + if (req.requiresUpperBounds() && this->hasUpperBound()) { + req.clearUpperBounds(); + } + if (req.requiresLowerBounds() && this->hasLowerBound()) { + req.clearLowerBounds(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met."); + + bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, x, b); + if (this->isTrackSchedulerSet()) { + this->schedulerChoices = this->sccSolver->getSchedulerChoices(); + } + return res; + } + + template + bool TopologicalMinMaxLinearEquationSolver::solveScc(storm::Environment const& sccSolverEnvironment, OptimizationDirection dir, storm::storage::BitVector const& sccRowGroups, storm::storage::BitVector const& sccRows, std::vector& globalX, std::vector const& globalB) const { + + // Set up the SCC solver + if (!this->sccSolver) { + this->sccSolver = GeneralMinMaxLinearEquationSolverFactory().create(sccSolverEnvironment); + this->sccSolver->setCachingEnabled(true); + } + this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution()); + this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet()); + + // Requirements + auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); + if (req.requiresUpperBounds() && this->hasUpperBound()) { + req.clearUpperBounds(); + } + if (req.requiresLowerBounds() && this->hasLowerBound()) { + req.clearLowerBounds(); + } + if (req.requiresValidInitialScheduler() && this->hasInitialScheduler()) { + req.clearValidInitialScheduler(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met."); + + // SCC Matrix + storm::storage::SparseMatrix sccA = this->A->getSubmatrix(true, sccRowGroups, sccRowGroups); + this->sccSolver->setMatrix(std::move(sccA)); + + // x Vector + auto sccX = storm::utility::vector::filterVector(globalX, sccRowGroups); + + // b Vector + std::vector sccB; + sccB.reserve(sccRows.getNumberOfSetBits()); + for (auto const& row : sccRows) { + ValueType bi = globalB[row]; + for (auto const& entry : this->A->getRow(row)) { + if (!sccRowGroups.get(entry.getColumn())) { + bi += entry.getValue() * globalX[entry.getColumn()]; + } + } + sccB.push_back(std::move(bi)); + } + + // initial scheduler + if (this->hasInitialScheduler()) { + auto sccInitChoices = storm::utility::vector::filterVector(this->getInitialScheduler(), sccRowGroups); + this->sccSolver->setInitialScheduler(std::move(sccInitChoices)); + } + + // lower/upper bounds + if (this->hasLowerBound(storm::solver::AbstractEquationSolver::BoundType::Global)) { + this->sccSolver->setLowerBound(this->getLowerBound()); + } else if (this->hasLowerBound(storm::solver::AbstractEquationSolver::BoundType::Local)) { + this->sccSolver->setLowerBounds(storm::utility::vector::filterVector(this->getLowerBounds(), sccRowGroups)); + } + if (this->hasUpperBound(storm::solver::AbstractEquationSolver::BoundType::Global)) { + this->sccSolver->setUpperBound(this->getUpperBound()); + } else if (this->hasUpperBound(storm::solver::AbstractEquationSolver::BoundType::Local)) { + this->sccSolver->setUpperBounds(storm::utility::vector::filterVector(this->getUpperBounds(), sccRowGroups)); + } + + // Invoke scc solver + bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, sccX, sccB); + //std::cout << "rhs is " << storm::utility::vector::toString(sccB) << std::endl; + //std::cout << "x is " << storm::utility::vector::toString(sccX) << std::endl; + + // Set Scheduler choices + if (this->isTrackSchedulerSet()) { + storm::utility::vector::setVectorValues(this->schedulerChoices.get(), sccRowGroups, this->sccSolver->getSchedulerChoices()); + } + + // Set solution + storm::utility::vector::setVectorValues(globalX, sccRowGroups, sccX); + + return res; + } + + template + void TopologicalMinMaxLinearEquationSolver::repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector& x, std::vector const* b, uint_fast64_t n) const { + + storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env); + + // Set up the SCC solver + if (!this->sccSolver) { + this->sccSolver = GeneralMinMaxLinearEquationSolverFactory().create(sccSolverEnvironment); + this->sccSolver->setCachingEnabled(true); + } + this->sccSolver->setMatrix(*this->A); + this->sccSolver->repeatedMultiply(sccSolverEnvironment, d, x, b, n); + + if (!this->isCachingEnabled()) { + clearCache(); + } + } + + template + MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { + // Return the requirements of the underlying solver + return GeneralMinMaxLinearEquationSolverFactory().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), direction, assumeNoInitialScheduler); + } + + template + void TopologicalMinMaxLinearEquationSolver::clearCache() const { + sortedSccDecomposition.reset(); + longestSccChainSize = boost::none; + sccSolver.reset(); + auxiliaryRowGroupVector.reset(); + MinMaxLinearEquationSolver::clearCache(); + } + + template + std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(Environment const& env) const { + return std::make_unique>(); + } + + // Explicitly instantiate the min max linear equation solver. + template class TopologicalMinMaxLinearEquationSolver; + template class TopologicalMinMaxLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL + template class TopologicalMinMaxLinearEquationSolver; + template class TopologicalMinMaxLinearEquationSolverFactory; +#endif + } +} diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index e69de29bb..d1ad36e4a 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -0,0 +1,73 @@ +#pragma once + +#include "storm/solver/MinMaxLinearEquationSolver.h" + +#include "storm/solver/SolverSelectionOptions.h" +#include "storm/storage/StronglyConnectedComponentDecomposition.h" + +namespace storm { + + class Environment; + + namespace solver { + + template + class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { + public: + TopologicalMinMaxLinearEquationSolver(); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A); + + virtual void setMatrix(storm::storage::SparseMatrix const& A) override; + virtual void setMatrix(storm::storage::SparseMatrix&& A) override; + + + virtual void clearCache() const override; + + virtual void repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override ; + + protected: + + virtual bool internalSolveEquations(storm::Environment const& env, OptimizationDirection d, std::vector& x, std::vector const& b) const override; + + private: + storm::Environment getEnvironmentForUnderlyingSolver(storm::Environment const& env, bool adaptPrecision = false) const; + + // Creates an SCC decomposition and sorts the SCCs according to a topological sort. + void createSortedSccDecomposition(bool needLongestChainSize) const; + + // Solves the SCC with the given index + // ... for the case that the SCC is trivial + bool solveTrivialScc(uint64_t const& sccState, OptimizationDirection d, std::vector& globalX, std::vector const& globalB) const; + // ... for the case that there is just one large SCC + bool solveFullyConnectedEquationSystem(storm::Environment const& sccSolverEnvironment, OptimizationDirection d, std::vector& x, std::vector const& b) const; + // ... for the remaining cases (1 < scc.size() < x.size()) + bool solveScc(storm::Environment const& sccSolverEnvironment, OptimizationDirection d, storm::storage::BitVector const& sccRowGroups, storm::storage::BitVector const& sccRows, std::vector& globalX, std::vector const& globalB) const; + + // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted + // when the solver is destructed. + std::unique_ptr> localA; + + // A pointer to the original sparse matrix given to this solver. If the solver takes posession of the matrix + // the pointer refers to localA. + storm::storage::SparseMatrix const* A; + + // cached auxiliary data + mutable std::unique_ptr> sortedSccDecomposition; + mutable boost::optional longestSccChainSize; + mutable std::unique_ptr> sccSolver; + mutable std::unique_ptr> auxiliaryRowGroupVector; // A.rowGroupCount() entries + }; + + template + class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { + public: + using MinMaxLinearEquationSolverFactory::create; + + virtual std::unique_ptr> create(Environment const& env) const override; + + }; + + } +} diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index 0040dd81f..bb569e5a5 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -25,7 +25,7 @@ #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" -#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" namespace { @@ -266,7 +266,7 @@ namespace { static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological); - env.solver().topological().setUnderlyingSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen); env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); return env; } diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index 99cf434f6..668a94796 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -19,6 +19,7 @@ #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/logic/Formulas.h" #include "storm/storage/jani/Property.h" @@ -71,6 +72,42 @@ namespace { return env; } }; + + class SparseDoubleTopologicalValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); + env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + env.solver().minMax().setRelativeTerminationCriterion(false); + return env; + } + }; + + class SparseDoubleTopologicalSoundValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); + env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); + return env; + } + }; + class SparseRationalPolicyIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models @@ -300,6 +337,8 @@ namespace { SparseDoubleValueIterationEnvironment, SparseDoubleSoundValueIterationEnvironment, SparseDoubleQuickValueIterationEnvironment, + SparseDoubleTopologicalValueIterationEnvironment, + SparseDoubleTopologicalSoundValueIterationEnvironment, SparseRationalPolicyIterationEnvironment, SparseRationalRationalSearchEnvironment, HybridCuddDoubleValueIterationEnvironment, diff --git a/src/test/storm/solver/LinearEquationSolverTest.cpp b/src/test/storm/solver/LinearEquationSolverTest.cpp index 0ab4c1a55..f1ef97220 100644 --- a/src/test/storm/solver/LinearEquationSolverTest.cpp +++ b/src/test/storm/solver/LinearEquationSolverTest.cpp @@ -6,7 +6,7 @@ #include "storm/environment/solver/NativeSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/EigenSolverEnvironment.h" -#include "storm/environment/solver/TopologicalLinearEquationSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" #include "storm/utility/vector.h" namespace { @@ -273,7 +273,7 @@ namespace { static storm::Environment createEnvironment() { storm::Environment env; env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological); - env.solver().topological().setUnderlyingSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen); env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); return env; } diff --git a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp index 3caf14699..e34cf6a31 100644 --- a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp @@ -6,6 +6,7 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/environment/solver/NativeSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" #include "storm/solver/SolverSelectionOptions.h" #include "storm/storage/SparseMatrix.h" @@ -34,6 +35,7 @@ namespace { return env; } }; + class DoubleTopologicalViEnvironment { public: typedef double ValueType; @@ -41,10 +43,12 @@ namespace { static storm::Environment createEnvironment() { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); + env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); return env; } }; + class DoubleTopologicalCudaViEnvironment { public: typedef double ValueType;