diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 90f858756..6b6ff0fa1 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -86,7 +86,6 @@ namespace storm { } std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); - solver->allocateAuxMemory(storm::solver::MinMaxLinearEquationSolverOperation::SolveEquations); // Perform the actual value iteration // * loop until the step bound has been reached diff --git a/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 09806882c..728736d34 100644 --- a/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -307,7 +307,6 @@ namespace storm { result->solver = minMaxSolverFactory.create(PS.toPS); result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); result->solver->setTrackScheduler(true); - result->solver->allocateAuxMemory(storm::solver::MinMaxLinearEquationSolverOperation::SolveEquations); result->b.resize(PS.getNumberOfChoices()); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 9b7d65ff9..9c35a8a29 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -80,19 +80,10 @@ namespace storm { } template - bool MinMaxLinearEquationSolver::allocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const { - return false; - } - - template - bool MinMaxLinearEquationSolver::deallocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const { - return false; + void MinMaxLinearEquationSolver::resetAuxiliaryData() const { + // Intentionally left empty. } - template - bool MinMaxLinearEquationSolver::hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const { - return false; - } template MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(bool trackScheduler) : trackScheduler(trackScheduler) { diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 14457e778..c17aa269c 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -22,10 +22,6 @@ namespace storm { namespace solver { - enum class MinMaxLinearEquationSolverOperation { - SolveEquations, MultiplyRepeatedly - }; - /*! * A class representing the interface that all min-max linear equation solvers shall implement. */ @@ -132,31 +128,10 @@ namespace storm { */ virtual bool getRelative() const = 0; - // Methods related to allocating/freeing auxiliary storage. - - /*! - * Allocates auxiliary storage that can be used to perform the provided operation. Repeated calls to the - * corresponding function can then be run without allocating/deallocating this storage repeatedly. - * Note: Since the allocated storage is fit to the currently selected options of the solver, they must not - * be changed any more after allocating the auxiliary storage until the storage is deallocated again. - * - * @return True iff auxiliary storage was allocated. - */ - virtual bool allocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const; - - /*! - * Destroys previously allocated auxiliary storage for the provided operation. - * - * @return True iff auxiliary storage was deallocated. - */ - virtual bool deallocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const; - - /*! - * Checks whether the solver has allocated auxiliary storage for the provided operation. - * - * @return True iff auxiliary storage was previously allocated (and not yet deallocated). + /* + * Resets the auxiliary data that has been stored during previous calls of this solver */ - virtual bool hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const; + virtual void resetAuxiliaryData() const; protected: diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp index 714356b91..360146bf2 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp @@ -98,8 +98,11 @@ namespace storm { // Create the initial scheduler. std::vector scheduler(this->A.getRowGroupCount()); - // Create a vector for storing the right-hand side of the inner equation system. - std::vector subB(this->A.getRowGroupCount()); + // Get a vector for storing the right-hand side of the inner equation system. + if(!auxiliaryData.rowGroupVector) { + auxiliaryData.rowGroupVector = std::make_unique>(this->A.getRowGroupCount()); + } + std::vector& subB = *auxiliaryData.rowGroupVector; // Resolve the nondeterminism according to the current scheduler. storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); @@ -107,7 +110,7 @@ namespace storm { storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. - solver = linearEquationSolverFactory->create(std::move(submatrix)); + auto solver = linearEquationSolverFactory->create(std::move(submatrix)); solver->allocateAuxMemory(LinearEquationSolverOperation::SolveEquations); Status status = Status::InProgress; @@ -166,8 +169,6 @@ namespace storm { this->scheduler = std::make_unique(std::move(scheduler)); } - solver.reset(); - if(status == Status::Converged || status == Status::TerminatedEarly) { return true; } else{ @@ -204,16 +205,21 @@ namespace storm { template bool StandardMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - if(solver == nullptr) { - solver = linearEquationSolverFactory->create(A); + if(!auxiliaryData.linEqSolver) { + auxiliaryData.linEqSolver = linearEquationSolverFactory->create(A); } - bool allocatedAuxMemory = !this->hasAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations); - if (allocatedAuxMemory) { - this->allocateAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations); + + if (!auxiliaryData.rowVector.get()) { + auxiliaryData.rowVector = std::make_unique>(A.getRowCount()); + } + std::vector& multiplyResult = *auxiliaryData.rowVector; + + if (!auxiliaryData.rowGroupVector.get()) { + auxiliaryData.rowGroupVector = std::make_unique>(A.getRowGroupCount()); } + std::vector* newX = auxiliaryData.rowGroupVector.get(); std::vector* currentX = &x; - std::vector* newX = auxiliarySolvingVectorMemory.get(); // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations. uint64_t iterations = 0; @@ -221,10 +227,10 @@ namespace storm { Status status = Status::InProgress; while (status == Status::InProgress) { // Compute x' = A*x + b. - solver->multiply(*currentX, &b, *auxiliarySolvingMultiplyMemory); + auxiliaryData.linEqSolver->multiply(*currentX, &b, multiplyResult); // Reduce the vector x' by applying min/max for all non-deterministic choices. - storm::utility::vector::reduceVectorMinOrMax(dir, *auxiliarySolvingMultiplyMemory, *newX, this->A.getRowGroupIndices()); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices()); // Determine whether the method converged. if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) { @@ -242,27 +248,20 @@ namespace storm { // 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 == auxiliarySolvingVectorMemory.get()) { + if (currentX == auxiliaryData.rowGroupVector.get()) { std::swap(x, *currentX); } // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { if(iterations==0){ //may happen due to custom termination condition. Then we need to compute x'= A*x+b - solver->multiply(x, &b, *auxiliarySolvingMultiplyMemory); + auxiliaryData.linEqSolver->multiply(x, &b, multiplyResult); } std::vector choices(this->A.getRowGroupCount()); // Reduce the multiplyResult and keep track of the choices made - storm::utility::vector::reduceVectorMinOrMax(dir, *auxiliarySolvingMultiplyMemory, x, this->A.getRowGroupIndices(), &choices); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &choices); this->scheduler = std::make_unique(std::move(choices)); } - // If we allocated auxiliary memory, we need to dispose of it now. - if (allocatedAuxMemory) { - this->deallocateAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations); - } - - - if(status == Status::Converged || status == Status::TerminatedEarly) { return true; @@ -273,26 +272,21 @@ namespace storm { template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n) const { - bool allocatedAuxMemory = !this->hasAuxMemory(MinMaxLinearEquationSolverOperation::MultiplyRepeatedly); - if (allocatedAuxMemory) { - this->allocateAuxMemory(MinMaxLinearEquationSolverOperation::MultiplyRepeatedly); + if(!auxiliaryData.linEqSolver) { + auxiliaryData.linEqSolver = linearEquationSolverFactory->create(A); } - if(solver == nullptr) { - solver = linearEquationSolverFactory->create(A); + if (!auxiliaryData.rowVector.get()) { + auxiliaryData.rowVector = std::make_unique>(A.getRowCount()); } + std::vector& multiplyResult = *auxiliaryData.rowVector; for (uint64_t i = 0; i < n; ++i) { - solver->multiply(x, b, *auxiliaryRepeatedMultiplyMemory); + auxiliaryData.linEqSolver->multiply(x, 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, *auxiliaryRepeatedMultiplyMemory, x, this->A.getRowGroupIndices()); - } - - // If we allocated auxiliary memory, we need to dispose of it now. - if (allocatedAuxMemory) { - this->deallocateAuxMemory(MinMaxLinearEquationSolverOperation::MultiplyRepeatedly); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices()); } } @@ -325,77 +319,17 @@ namespace storm { } template - StandardMinMaxLinearEquationSolverSettings& StandardMinMaxLinearEquationSolver::getSettings() { - return settings; + void StandardMinMaxLinearEquationSolver::setSettings(StandardMinMaxLinearEquationSolverSettings const& newSettings) { + settings = newSettings; } template - bool StandardMinMaxLinearEquationSolver::allocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const { - bool result = false; - if (operation == MinMaxLinearEquationSolverOperation::SolveEquations) { - if (this->getSettings().getSolutionMethod() == StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { - if (!auxiliarySolvingMultiplyMemory) { - result = true; - auxiliarySolvingMultiplyMemory = std::make_unique>(this->A.getRowCount()); - } - if (!auxiliarySolvingVectorMemory) { - result = true; - auxiliarySolvingVectorMemory = std::make_unique>(this->A.getRowGroupCount()); - } - } else if (this->getSettings().getSolutionMethod() == StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { - // Nothing to do in this case. - } else { - STORM_LOG_ASSERT(false, "Cannot allocate aux storage for this method."); - } - } else { - if (!auxiliaryRepeatedMultiplyMemory) { - result = true; - auxiliaryRepeatedMultiplyMemory = std::make_unique>(this->A.getRowCount()); - } - } - return result; + void StandardMinMaxLinearEquationSolver::resetAuxiliaryData() const { + auxiliaryData.linEqSolver.reset(); + auxiliaryData.rowVector.reset(); + auxiliaryData.rowGroupVector.reset(); } - - template - bool StandardMinMaxLinearEquationSolver::deallocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const { - bool result = false; - if (operation == MinMaxLinearEquationSolverOperation::SolveEquations) { - if (this->getSettings().getSolutionMethod() == StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { - if (auxiliarySolvingMultiplyMemory) { - result = true; - auxiliarySolvingMultiplyMemory.reset(); - } - if (auxiliarySolvingVectorMemory) { - result = true; - auxiliarySolvingVectorMemory.reset(); - } - } else if (this->getSettings().getSolutionMethod() == StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { - // Nothing to do in this case. - } else { - STORM_LOG_ASSERT(false, "Cannot allocate aux storage for this method."); - } - } else { - if (auxiliaryRepeatedMultiplyMemory) { - result = true; - auxiliaryRepeatedMultiplyMemory.reset(); - } - } - return result; - } - - template - bool StandardMinMaxLinearEquationSolver::hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const { - if (operation == MinMaxLinearEquationSolverOperation::SolveEquations) { - if (this->getSettings().getSolutionMethod() == StandardMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { - return auxiliarySolvingMultiplyMemory && auxiliarySolvingVectorMemory; - } else { - return false; - } - } else { - return static_cast(auxiliaryRepeatedMultiplyMemory); - } - } - + template StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(bool trackScheduler) : MinMaxLinearEquationSolverFactory(trackScheduler), linearEquationSolverFactory(nullptr) { // Intentionally left empty. diff --git a/src/solver/StandardMinMaxLinearEquationSolver.h b/src/solver/StandardMinMaxLinearEquationSolver.h index 86a960694..d460887be 100644 --- a/src/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/solver/StandardMinMaxLinearEquationSolver.h @@ -11,6 +11,8 @@ namespace storm { public: StandardMinMaxLinearEquationSolverSettings(); + StandardMinMaxLinearEquationSolverSettings& operator=(StandardMinMaxLinearEquationSolverSettings const& other) = default; + enum class SolutionMethod { ValueIteration, PolicyIteration }; @@ -42,11 +44,9 @@ namespace storm { virtual void repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector* b, uint_fast64_t n) const override; StandardMinMaxLinearEquationSolverSettings const& getSettings() const; - StandardMinMaxLinearEquationSolverSettings& getSettings(); + void setSettings(StandardMinMaxLinearEquationSolverSettings const& newSettings); - virtual bool allocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const override; - virtual bool deallocateAuxMemory(MinMaxLinearEquationSolverOperation operation) const override; - virtual bool hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const override; + virtual void resetAuxiliaryData() const override; virtual ValueType getPrecision() const override; virtual bool getRelative() const override; @@ -59,6 +59,14 @@ namespace storm { enum class Status { Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress }; + + struct AuxiliaryData { + std::unique_ptr> linEqSolver; + std::unique_ptr> rowVector; // A.rowCount() entries + std::unique_ptr> rowGroupVector; // A.rowGroupCount() entries + }; + + mutable AuxiliaryData auxiliaryData; Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; void reportStatus(Status status, uint64_t iterations) const; @@ -68,7 +76,6 @@ namespace storm { /// The factory used to obtain linear equation solvers. std::unique_ptr> linearEquationSolverFactory; - mutable std::unique_ptr> solver; // 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. @@ -78,12 +85,6 @@ namespace storm { // the reference refers to localA. storm::storage::SparseMatrix const& A; - // Auxiliary memory for equation solving. - mutable std::unique_ptr> auxiliarySolvingMultiplyMemory; - mutable std::unique_ptr> auxiliarySolvingVectorMemory; - - // Auxiliary memory for repeated matrix-vector multiplication. - mutable std::unique_ptr> auxiliaryRepeatedMultiplyMemory; }; template