From cd34e3d67eb7a03fccd9adb02200cecb4222103a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 2 Dec 2017 13:08:14 +0100 Subject: [PATCH] fixed issue in rational search preventing convergence in many cases --- src/storm/solver/NativeLinearEquationSolver.cpp | 4 ++-- .../solver/SymbolicMinMaxLinearEquationSolver.cpp | 8 +++++--- .../solver/SymbolicNativeLinearEquationSolver.cpp | 10 ++++++---- src/storm/storage/dd/Add.cpp | 6 +++++- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 7 +++++++ src/storm/storage/dd/cudd/InternalCuddAdd.h | 5 +++++ src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp | 7 +++++++ src/storm/storage/dd/sylvan/InternalSylvanAdd.h | 2 ++ 8 files changed, 39 insertions(+), 10 deletions(-) diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index c9974a700..d6de61266 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -776,9 +776,9 @@ namespace storm { template template bool NativeLinearEquationSolver::sharpen(uint64_t precision, storm::storage::SparseMatrix const& A, std::vector const& x, std::vector const& b, std::vector& tmp) { - for (uint64_t p = 0; p <= precision; ++p) { + for (uint64_t p = 1; p <= precision; ++p) { storm::utility::kwek_mehlhorn::sharpen(p, x, tmp); - + if (NativeLinearEquationSolver::isSolution(A, tmp, b)) { return true; } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index b92ed6d9d..b1501fd32 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -142,9 +142,10 @@ namespace storm { template storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(Environment const& env, OptimizationDirection dir, SymbolicMinMaxLinearEquationSolver const& rationalSolver, SymbolicMinMaxLinearEquationSolver const& impreciseSolver, storm::dd::Add const& rationalB, storm::dd::Add const& x, storm::dd::Add const& b) const { - // Storage for the rational sharpened vector. + // Storage for the rational sharpened vector and the power iteration intermediate vector. storm::dd::Add sharpenedX; - + storm::dd::Add currentX = x; + // The actual rational search. uint64_t overallIterations = 0; uint64_t valueIterationInvocations = 0; @@ -153,7 +154,7 @@ namespace storm { bool relative = env.solver().minMax().getRelativeTerminationCriterion(); SolverStatus status = SolverStatus::InProgress; while (status == SolverStatus::InProgress && overallIterations < maxIter) { - typename SymbolicMinMaxLinearEquationSolver::ValueIterationResult viResult = impreciseSolver.performValueIteration(dir, x, b, storm::utility::convertNumber(precision), relative, maxIter); + typename SymbolicMinMaxLinearEquationSolver::ValueIterationResult viResult = impreciseSolver.performValueIteration(dir, currentX, b, storm::utility::convertNumber(precision), relative, maxIter); ++valueIterationInvocations; STORM_LOG_TRACE("Completed " << valueIterationInvocations << " value iteration invocations, the last one with precision " << precision << " completed in " << viResult.iterations << " iterations."); @@ -170,6 +171,7 @@ namespace storm { if (isSolution) { status = SolverStatus::Converged; } else { + currentX = viResult.values; precision /= storm::utility::convertNumber(10); } } diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 760683bf5..4252b1483 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -174,10 +174,10 @@ namespace storm { storm::dd::Add sharpenedX; - for (uint64_t p = 1; p < precision; ++p) { + for (uint64_t p = 1; p <= precision; ++p) { sharpenedX = x.sharpenKwekMehlhorn(p); + isSolution = rationalSolver.isSolutionFixedPoint(sharpenedX, rationalB); - if (isSolution) { break; } @@ -190,8 +190,9 @@ namespace storm { template storm::dd::Add SymbolicNativeLinearEquationSolver::solveEquationsRationalSearchHelper(Environment const& env, SymbolicNativeLinearEquationSolver const& rationalSolver, SymbolicNativeLinearEquationSolver const& impreciseSolver, storm::dd::Add const& rationalB, storm::dd::Add const& x, storm::dd::Add const& b) const { - // Storage for the rational sharpened vector. + // Storage for the rational sharpened vector and the power iteration intermediate vector. storm::dd::Add sharpenedX; + storm::dd::Add currentX = x; // The actual rational search. uint64_t overallIterations = 0; @@ -201,7 +202,7 @@ namespace storm { bool relative = env.solver().native().getRelativeTerminationCriterion(); SolverStatus status = SolverStatus::InProgress; while (status == SolverStatus::InProgress && overallIterations < maxIter) { - typename SymbolicNativeLinearEquationSolver::PowerIterationResult result = impreciseSolver.performPowerIteration(x, b, storm::utility::convertNumber(precision), relative, maxIter - overallIterations); + typename SymbolicNativeLinearEquationSolver::PowerIterationResult result = impreciseSolver.performPowerIteration(currentX, b, storm::utility::convertNumber(precision), relative, maxIter - overallIterations); ++powerIterationInvocations; STORM_LOG_TRACE("Completed " << powerIterationInvocations << " power iteration invocations, the last one with precision " << precision << " completed in " << result.iterations << " iterations."); @@ -218,6 +219,7 @@ namespace storm { if (isSolution) { status = SolverStatus::Converged; } else { + currentX = result.values; precision /= storm::utility::convertNumber(10); } } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index a62600562..635d16aed 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -941,7 +941,7 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, Add const& add) { - out << "ADD with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; + out << "ADD [" << add.getInternalAdd().getStringId() << "] with " << add.getNonZeroCount() << " nnz, " << add.getNodeCount() << " nodes, " << add.getLeafCount() << " leaves" << std::endl; std::vector variableNames; for (auto const& variable : add.getContainedMetaVariables()) { variableNames.push_back(variable.getName()); @@ -993,15 +993,19 @@ namespace storm { } template class Add; + template std::ostream& operator<<(std::ostream& out, Add const& add); template class Add; template class Add; + template std::ostream& operator<<(std::ostream& out, Add const& add); template class Add; #ifdef STORM_HAVE_CARL template class Add; + template std::ostream& operator<<(std::ostream& out, Add const& add); template class Add; + template std::ostream& operator<<(std::ostream& out, Add const& add); template class Add; template Add Add::toValueType() const; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 83ace48ae..9645ebdf3 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -420,6 +420,13 @@ namespace storm { DdNode* InternalAdd::getCuddDdNode() const { return this->getCuddAdd().getNode(); } + + template + std::string InternalAdd::getStringId() const { + std::stringstream ss; + ss << this->getCuddDdNode(); + return ss.str(); + } template Odd InternalAdd::createOdd(std::vector const& ddVariableIndices) const { diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 5871e20dc..2262d5da0 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -629,6 +629,11 @@ namespace storm { */ DdNode* getCuddDdNode() const; + /*! + * Retrieves a string representation of an ID for thid ADD. + */ + std::string getStringId() const; + private: /*! * Performs a recursive step to perform the given function between the given DD-based vector and the given diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index b3723a4c4..0173f6aac 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1151,6 +1151,13 @@ namespace storm { return sylvanMtbdd; } + template + std::string InternalAdd::getStringId() const { + std::stringstream ss; + ss << this->getSylvanMtbdd().GetMTBDD(); + return ss.str(); + } + template class InternalAdd; template class InternalAdd; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 79a29f187..dc65e240a 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -620,6 +620,8 @@ namespace storm { */ static ValueType getValue(MTBDD const& node); + std::string getStringId() const; + private: /*! * Recursively builds the ODD from an ADD.