From da02237769ab1c041c5b86d57491db42679adc87 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 10 Oct 2017 18:21:24 +0200 Subject: [PATCH] work towards symbolic rational search --- resources/3rdparty/CMakeLists.txt | 3 + .../3rdparty/sylvan/src/storm_wrapper.cpp | 9 + resources/3rdparty/sylvan/src/storm_wrapper.h | 3 +- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 29 +++ .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 7 + .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 2 + .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 6 + .../IterativeMinMaxLinearEquationSolver.cpp | 54 ++--- .../IterativeMinMaxLinearEquationSolver.h | 16 +- .../solver/NativeLinearEquationSolver.cpp | 20 +- src/storm/solver/NativeLinearEquationSolver.h | 9 +- src/storm/solver/SolverStatus.cpp | 23 ++- src/storm/solver/SolverStatus.h | 24 +-- ...ymbolicEliminationLinearEquationSolver.cpp | 2 + .../solver/SymbolicLinearEquationSolver.cpp | 5 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 186 +++++++++++++++--- .../SymbolicMinMaxLinearEquationSolver.h | 44 ++++- .../SymbolicNativeLinearEquationSolver.cpp | 2 + src/storm/storage/dd/Add.cpp | 34 ++-- src/storm/storage/dd/Add.h | 4 +- src/storm/storage/dd/Bdd.cpp | 7 +- src/storm/storage/dd/DdManager.cpp | 12 ++ src/storm/storage/dd/cudd/CuddAddIterator.cpp | 8 +- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 53 ++++- src/storm/storage/dd/cudd/InternalCuddAdd.h | 10 + src/storm/storage/dd/cudd/InternalCuddBdd.cpp | 4 + .../storage/dd/cudd/InternalCuddDdManager.cpp | 12 +- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 7 +- .../storage/dd/sylvan/InternalSylvanAdd.h | 2 +- src/test/storm/storage/SylvanDdTest.cpp | 17 ++ 30 files changed, 492 insertions(+), 122 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 34e38bbf7..9ffababeb 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -436,6 +436,9 @@ ExternalProject_Add( LOG_BUILD ON DEPENDS ${sylvan_dep} BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} + + // FIXME: remove + BUILD_ALWAYS 1 ) ExternalProject_Get_Property(sylvan source_dir) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index 74d191b95..287b56f3e 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -149,6 +149,15 @@ double storm_rational_number_get_value_double(storm_rational_number_ptr a) { return storm::utility::convertNumber(srn_a); } +storm_rational_number_ptr storm_rational_number_from_double(double value) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber* number = new storm::RationalNumber(storm::utility::convertNumber(value)); + return number; +} + storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.h b/resources/3rdparty/sylvan/src/storm_wrapper.h index d5ee75259..b2bff2860 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_wrapper.h @@ -29,7 +29,8 @@ extern "C" { int storm_rational_number_is_zero(storm_rational_number_ptr a); uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed); double storm_rational_number_get_value_double(storm_rational_number_ptr a); - + storm_rational_number_ptr storm_rational_number_from_double(double value); + // Binary operations. storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b); storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 67919ed5f..ab14e67a3 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -621,6 +621,35 @@ TASK_IMPL_2(MTBDD, mtbdd_sharpen, MTBDD, dd, size_t, p) return mtbdd_uapply(dd, TASK(mtbdd_op_sharpen), p); } +TASK_IMPL_2(MTBDD, mtbdd_op_to_rational_number, MTBDD, a, size_t, p) +{ + /* We only expect double or rational number terminals, or false */ + if (a == mtbdd_false) return mtbdd_false; + if (a == mtbdd_true) return mtbdd_true; + + // a != constant + mtbddnode_t na = MTBDD_GETNODE(a); + + if (mtbddnode_isleaf(na)) { + if (mtbddnode_gettype(na) == 1) { + MTBDD result = mtbdd_storm_rational_number(storm_rational_number_from_double(mtbdd_getdouble(a))); + return result; + } else { + printf("ERROR: Unsupported value type in conversion to rational number.\n"); + assert(0); + } + } + + return mtbdd_invalid; + (void)p; // unused variable +} + +TASK_IMPL_2(MTBDD, mtbdd_to_rational_number, MTBDD, dd, size_t, p) +{ + return mtbdd_uapply(dd, TASK(mtbdd_to_rational_number), 0); +} + + TASK_IMPL_3(BDD, mtbdd_min_abstract_representative, MTBDD, a, BDD, v, BDDVAR, prev_level) { /* Maybe perform garbage collection */ sylvan_gc_test(); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 5fcd69383..449a98c3e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -133,6 +133,13 @@ MTBDD mtbdd_ithvar(uint32_t var); TASK_DECL_2(MTBDD, mtbdd_op_sharpen, MTBDD, size_t) TASK_DECL_2(MTBDD, mtbdd_sharpen, MTBDD, size_t) #define mtbdd_sharpen(dd, p) CALL(mtbdd_sharpen, dd, p) + +/** + * Monad that converts the double MTBDD to an MTBDD over rational numbers. + */ +TASK_DECL_2(MTBDD, mtbdd_op_to_rational_number, MTBDD, size_t) +TASK_DECL_2(MTBDD, mtbdd_to_rational_number, MTBDD, size_t) +#define mtbdd_to_rational_number(dd) CALL(mtbdd_to_rational_number, dd, 0) /** * Unary operation Complement. diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index cab9be01b..71b6f2106 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -32,6 +32,8 @@ bool EqualNormRel(const Mtbdd& other, double epsilon) const; Mtbdd SharpenKwekMehlhorn(size_t precision) const; +Mtbdd ToRationalNumber() const; + // Functions that operate on Mtbdds over rational numbers. static Mtbdd stormRationalNumberTerminal(storm::RationalNumber const& value); diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index dcddb3b6f..974e60a18 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -203,6 +203,12 @@ Mtbdd::SharpenKwekMehlhorn(size_t precision) const { return mtbdd_sharpen(mtbdd, precision); } +Mtbdd +Mtbdd::ToRationalNumber() const { + LACE_ME; + return mtbdd_to_rational_number(mtbdd); +} + // Functions for Mtbdds over rational numbers. Mtbdd Mtbdd::stormRationalNumberTerminal(storm::RationalNumber const& value) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index faa04d400..34d0462ab 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -172,7 +172,7 @@ namespace storm { } solver->setCachingEnabled(true); - Status status = Status::InProgress; + SolverStatus status = SolverStatus::InProgress; uint64_t iterations = 0; this->startMeasureProgress(); do { @@ -209,7 +209,7 @@ namespace storm { // If the scheduler did not improve, we are done. if (!schedulerImproved) { - status = Status::Converged; + status = SolverStatus::Converged; } else { // Update the scheduler and the solver. submatrix = this->A->selectRowsFromRowGroups(scheduler, true); @@ -224,7 +224,7 @@ namespace storm { // Potentially show progress. this->showProgressIterative(iterations); - } while (status == Status::InProgress); + } while (status == SolverStatus::InProgress); reportStatus(status, iterations); @@ -237,7 +237,7 @@ namespace storm { clearCache(); } - return status == Status::Converged || status == Status::TerminatedEarly; + return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly; } template @@ -336,8 +336,8 @@ namespace storm { std::vector* originalX = currentX; - Status status = Status::InProgress; - while (status == Status::InProgress) { + SolverStatus status = SolverStatus::InProgress; + while (status == SolverStatus::InProgress) { // Compute x' = min/max(A*x + b). if (useGaussSeidelMultiplication) { // Copy over the current vector so we can modify it in-place. @@ -349,7 +349,7 @@ namespace storm { // Determine whether the method converged. if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative)) { - status = Status::Converged; + status = SolverStatus::Converged; } // Update environment variables. @@ -437,7 +437,7 @@ namespace storm { clearCache(); } - return result.status == Status::Converged || result.status == Status::TerminatedEarly; + return result.status == SolverStatus::Converged || result.status == SolverStatus::TerminatedEarly; } template @@ -500,7 +500,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations. uint64_t iterations = 0; - Status status = Status::InProgress; + SolverStatus status = SolverStatus::InProgress; bool doConvergenceCheck = true; bool useDiffs = this->hasRelevantValues(); std::vector oldValues; @@ -514,7 +514,7 @@ namespace storm { precision *= storm::utility::convertNumber(2.0); } this->startMeasureProgress(); - while (status == Status::InProgress && iterations < this->getSettings().getMaximalNumberOfIterations()) { + while (status == SolverStatus::InProgress && iterations < this->getSettings().getMaximalNumberOfIterations()) { // Remember in which directions we took steps in this iteration. bool lowerStep = false; bool upperStep = false; @@ -597,9 +597,9 @@ namespace storm { if (doConvergenceCheck) { // Determine whether the method converged. if (this->hasRelevantValues()) { - status = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status; + status = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? SolverStatus::Converged : status; } else { - status = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status; + status = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? SolverStatus::Converged : status; } } @@ -640,7 +640,7 @@ namespace storm { clearCache(); } - return status == Status::Converged; + return status == SolverStatus::Converged; } template @@ -868,12 +868,12 @@ namespace storm { std::vector* currentX = &x; std::vector* newX = &tmpX; - Status status = Status::InProgress; + SolverStatus status = SolverStatus::InProgress; uint64_t overallIterations = 0; uint64_t valueIterationInvocations = 0; ValueType precision = this->getSettings().getPrecision(); impreciseSolver.startMeasureProgress(); - while (status == Status::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) { + while (status == SolverStatus::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) { // Perform value iteration with the current precision. typename IterativeMinMaxLinearEquationSolver::ValueIterationResult result = impreciseSolver.performValueIteration(dir, currentX, newX, b, storm::utility::convertNumber(precision), this->getSettings().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations); @@ -897,7 +897,7 @@ namespace storm { // After sharpen, if a solution was found, it is contained in the free rational. if (foundSolution) { - status = Status::Converged; + status = SolverStatus::Converged; TemporaryHelper::swapSolutions(rationalX, temporaryRational, x, currentX, newX); } else { @@ -906,13 +906,13 @@ namespace storm { } } - if (status == Status::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) { - status = Status::MaximalIterationsExceeded; + if (status == SolverStatus::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) { + status = SolverStatus::MaximalIterationsExceeded; } reportStatus(status, overallIterations); - return status == Status::Converged || status == Status::TerminatedEarly; + return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly; } template @@ -1028,23 +1028,23 @@ namespace storm { } template - typename IterativeMinMaxLinearEquationSolver::Status IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const { - if (status != Status::Converged) { + SolverStatus IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(SolverStatus status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const { + if (status != SolverStatus::Converged) { if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x, guarantee)) { - status = Status::TerminatedEarly; + status = SolverStatus::TerminatedEarly; } else if (iterations >= this->getSettings().getMaximalNumberOfIterations()) { - status = Status::MaximalIterationsExceeded; + status = SolverStatus::MaximalIterationsExceeded; } } return status; } template - void IterativeMinMaxLinearEquationSolver::reportStatus(Status status, uint64_t iterations) { + void IterativeMinMaxLinearEquationSolver::reportStatus(SolverStatus status, uint64_t iterations) { switch (status) { - case Status::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break; - case Status::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break; - case Status::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break; + case SolverStatus::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break; + case SolverStatus::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break; + case SolverStatus::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly."); } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index e3c9c8d0f..f4aa7e7a3 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -7,6 +7,8 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" +#include "storm/solver/SolverStatus.h" + namespace storm { namespace solver { @@ -84,18 +86,14 @@ namespace storm { static bool isSolution(storm::OptimizationDirection dir, storm::storage::SparseMatrix const& matrix, std::vector const& values, std::vector const& b); void computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice = nullptr) const; - - enum class Status { - Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress - }; - + struct ValueIterationResult { - ValueIterationResult(uint64_t iterations, Status status) : iterations(iterations), status(status) { + ValueIterationResult(uint64_t iterations, SolverStatus status) : iterations(iterations), status(status) { // Intentionally left empty. } uint64_t iterations; - Status status; + SolverStatus status; }; template @@ -110,8 +108,8 @@ namespace storm { mutable std::unique_ptr> auxiliaryRowGroupVector2; // A.rowGroupCount() entries mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries - Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const; - static void reportStatus(Status status, uint64_t iterations); + SolverStatus updateStatusIfNotConverged(SolverStatus status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const; + static void reportStatus(SolverStatus status, uint64_t iterations); /// The settings of this solver. IterativeMinMaxLinearEquationSolverSettings settings; diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 131ea8c0f..bd41cf80e 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -428,7 +428,7 @@ namespace storm { std::swap(currentX, newX); } - return PowerIterationResult(iterations - currentIterations, converged ? Status::Converged : (terminate ? Status::TerminatedEarly : Status::MaximalIterationsExceeded)); + return PowerIterationResult(iterations - currentIterations, converged ? SolverStatus::Converged : (terminate ? SolverStatus::TerminatedEarly : SolverStatus::MaximalIterationsExceeded)); } template @@ -457,9 +457,9 @@ namespace storm { clearCache(); } - this->logIterations(result.status == Status::Converged, result.status == Status::TerminatedEarly, result.iterations); + this->logIterations(result.status == SolverStatus::Converged, result.status == SolverStatus::TerminatedEarly, result.iterations); - return result.status == Status::Converged || result.status == Status::TerminatedEarly; + return result.status == SolverStatus::Converged || result.status == SolverStatus::TerminatedEarly; } template @@ -688,12 +688,12 @@ namespace storm { std::vector* currentX = &x; std::vector* newX = &tmpX; - Status status = Status::InProgress; + SolverStatus status = SolverStatus::InProgress; uint64_t overallIterations = 0; uint64_t valueIterationInvocations = 0; ValueType precision = this->getSettings().getPrecision(); impreciseSolver.startMeasureProgress(); - while (status == Status::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) { + while (status == SolverStatus::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) { // Perform value iteration with the current precision. typename NativeLinearEquationSolver::PowerIterationResult result = impreciseSolver.performPowerIteration(currentX, newX, b, storm::utility::convertNumber(precision), this->getSettings().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations); @@ -717,7 +717,7 @@ namespace storm { // After sharpen, if a solution was found, it is contained in the free rational. if (foundSolution) { - status = Status::Converged; + status = SolverStatus::Converged; TemporaryHelper::swapSolutions(rationalX, temporaryRational, x, currentX, newX); } else { @@ -726,13 +726,13 @@ namespace storm { } } - if (status == Status::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) { - status = Status::MaximalIterationsExceeded; + if (status == SolverStatus::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) { + status = SolverStatus::MaximalIterationsExceeded; } - this->logIterations(status == Status::Converged, status == Status::TerminatedEarly, overallIterations); + this->logIterations(status == SolverStatus::Converged, status == SolverStatus::TerminatedEarly, overallIterations); - return status == Status::Converged || status == Status::TerminatedEarly; + return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly; } template diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index 5617244c8..add1b6eff 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -6,6 +6,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/NativeMultiplier.h" +#include "storm/solver/SolverStatus.h" #include "storm/utility/NumberTraits.h" @@ -78,17 +79,13 @@ namespace storm { virtual bool internalSolveEquations(std::vector& x, std::vector const& b) const override; private: - enum class Status { - Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress - }; - struct PowerIterationResult { - PowerIterationResult(uint64_t iterations, Status status) : iterations(iterations), status(status) { + PowerIterationResult(uint64_t iterations, SolverStatus status) : iterations(iterations), status(status) { // Intentionally left empty. } uint64_t iterations; - Status status; + SolverStatus status; }; template diff --git a/src/storm/solver/SolverStatus.cpp b/src/storm/solver/SolverStatus.cpp index 49c2e0f52..116a39fc9 100644 --- a/src/storm/solver/SolverStatus.cpp +++ b/src/storm/solver/SolverStatus.cpp @@ -1,8 +1,17 @@ -// -// SolverStatus.cpp -// storm -// -// Created by Christian Dehnert on 10.10.17. -// +#include "storm/solver/SolverStatus.h" -#include "SolverStatus.hpp" +namespace storm { + namespace solver { + + std::ostream& operator<<(std::ostream& out, SolverStatus const& status) { + switch (status) { + case SolverStatus::Converged: out << "converged"; break; + case SolverStatus::TerminatedEarly: out << "terminated"; break; + case SolverStatus::MaximalIterationsExceeded: out << "maximal iterations exceeded"; break; + case SolverStatus::InProgress: out << "in progress"; break; + } + return out; + } + + } +} diff --git a/src/storm/solver/SolverStatus.h b/src/storm/solver/SolverStatus.h index cd346dd53..624890f3a 100644 --- a/src/storm/solver/SolverStatus.h +++ b/src/storm/solver/SolverStatus.h @@ -1,13 +1,15 @@ -// -// SolverStatus.hpp -// storm -// -// Created by Christian Dehnert on 10.10.17. -// +#pragma once -#ifndef SolverStatus_hpp -#define SolverStatus_hpp +#include -#include - -#endif /* SolverStatus_hpp */ +namespace storm { + namespace solver { + + enum class SolverStatus { + Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress + }; + + std::ostream& operator<<(std::ostream& out, SolverStatus const& status); + + } +} diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index 44689d990..1cdc67743 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -124,11 +124,13 @@ namespace storm { } template class SymbolicEliminationLinearEquationSolver; + template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolverFactory; + template class SymbolicEliminationLinearEquationSolverFactory; template class SymbolicEliminationLinearEquationSolverFactory; template class SymbolicEliminationLinearEquationSolverFactory; template class SymbolicEliminationLinearEquationSolverFactory; diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 066b7b19b..41620bbf8 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -116,17 +116,20 @@ namespace storm { } template class SymbolicLinearEquationSolver; + template class SymbolicLinearEquationSolver; + template class SymbolicLinearEquationSolver; - template class SymbolicLinearEquationSolver; template class SymbolicLinearEquationSolver; template class SymbolicLinearEquationSolverFactory; + template class SymbolicLinearEquationSolverFactory; template class SymbolicLinearEquationSolverFactory; template class SymbolicLinearEquationSolverFactory; template class SymbolicLinearEquationSolverFactory; template class GeneralSymbolicLinearEquationSolverFactory; + template class GeneralSymbolicLinearEquationSolverFactory; template class GeneralSymbolicLinearEquationSolverFactory; template class GeneralSymbolicLinearEquationSolverFactory; template class GeneralSymbolicLinearEquationSolverFactory; diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 03f603337..44ba169c6 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -1,7 +1,5 @@ #include "storm/solver/SymbolicMinMaxLinearEquationSolver.h" - - #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" @@ -32,6 +30,7 @@ namespace storm { switch (method) { case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break; case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break; + case MinMaxMethod::RationalSearch: this->solutionMethod = SolutionMethod::RationalSearch; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } @@ -97,25 +96,25 @@ namespace storm { case SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration: return solveEquationsPolicyIteration(dir, x, b); break; + case SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch: + return solveEquationsRationalSearch(dir, x, b); + break; } } template - storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { - // Set up the environment. - storm::dd::Add xCopy = x; - uint_fast64_t iterations = 0; - bool converged = false; - - // If we were given an initial scheduler, we take its solution as the starting point. - if (this->hasInitialScheduler()) { - xCopy = solveEquationsWithScheduler(this->getInitialScheduler(), xCopy, b); - } + typename SymbolicMinMaxLinearEquationSolver::ValueIterationResult SymbolicMinMaxLinearEquationSolver::performValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b, ValueType const& precision, bool relativeTerminationCriterion) const { + + // Set up local variables. + storm::dd::Add localX = x; + uint64_t iterations = 0; - while (!converged && iterations < this->settings.getMaximalNumberOfIterations()) { + // Value iteration loop. + SolverStatus status = SolverStatus::InProgress; + while (status == SolverStatus::Converged && iterations < this->settings.getMaximalNumberOfIterations()) { // Compute tmp = A * x + b - storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); - storm::dd::Add tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); + storm::dd::Add localXAsColumn = localX.swapVariables(this->rowColumnMetaVariablePairs); + storm::dd::Add tmp = this->A.multiplyMatrix(localXAsColumn, this->columnMetaVariables); tmp += b; if (dir == storm::solver::OptimizationDirection::Minimize) { @@ -126,20 +125,163 @@ namespace storm { } // Now check if the process already converged within our precision. - converged = xCopy.equalModuloPrecision(tmp, this->settings.getPrecision(), this->settings.getRelativeTerminationCriterion()); + if (localX.equalModuloPrecision(tmp, precision, relativeTerminationCriterion)) { + status = SolverStatus::Converged; + } + + // Set up next iteration. + localX = tmp; + ++iterations; + } + + if (status != SolverStatus::Converged) { + status = SolverStatus::MaximalIterationsExceeded; + } + + return SymbolicMinMaxLinearEquationSolver::ValueIterationResult(status, iterations, localX); + } + + template + bool SymbolicMinMaxLinearEquationSolver::isSolution(OptimizationDirection dir, storm::dd::Add const& x, storm::dd::Add const& b) const { + storm::dd::Add xAsColumn = x.swapVariables(this->rowColumnMetaVariablePairs); + storm::dd::Add tmp = this->A.multiplyMatrix(xAsColumn, this->columnMetaVariables); + tmp += b; + + if (dir == storm::solver::OptimizationDirection::Minimize) { + tmp += illegalMaskAdd; + tmp = tmp.minAbstract(this->choiceVariables); + } else { + tmp = tmp.maxAbstract(this->choiceVariables); + } + + return x == tmp; + } + + template + template + storm::dd::Add SymbolicMinMaxLinearEquationSolver::sharpen(OptimizationDirection dir, uint64_t precision, SymbolicMinMaxLinearEquationSolver const& rationalSolver, storm::dd::Add const& x, storm::dd::Add const& rationalB, bool& isSolution) { + + storm::dd::Add sharpenedX; + + for (uint64_t p = 1; p < precision; ++p) { + storm::dd::Add sharpenedX = x.sharpenKwekMehlhorn(precision); + isSolution = rationalSolver.isSolution(dir, sharpenedX, rationalB); + + if (isSolution) { + break; + } + } + + return sharpenedX; + } + + template + template + storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(OptimizationDirection dir, SymbolicMinMaxLinearEquationSolver const& rationalSolver, SymbolicMinMaxLinearEquationSolver const& impreciseSolver, storm::dd::Add const& rationalX, storm::dd::Add const& rationalB, storm::dd::Add const& x, storm::dd::Add const& b) const { + + // Storage for the rational sharpened vector. + storm::dd::Add sharpenedX; + + // The actual rational search. + uint64_t overallIterations = 0; + uint64_t valueIterationInvocations = 0; + ValueType precision = this->getSettings().getPrecision(); + SolverStatus status = SolverStatus::InProgress; + while (status == SolverStatus::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) { + typename SymbolicMinMaxLinearEquationSolver::ValueIterationResult viResult = impreciseSolver.performValueIteration(dir, x, b, storm::utility::convertNumber(precision), this->getSettings().getRelativeTerminationCriterion()); - xCopy = tmp; + ++valueIterationInvocations; + STORM_LOG_TRACE("Completed " << valueIterationInvocations << " value iteration invocations, the last one with precision " << precision << " completed in " << viResult.iterations << " iterations."); + + // Count the iterations. + overallIterations += viResult.iterations; - ++iterations; + // Compute maximal precision until which to sharpen. + uint64_t p = storm::utility::convertNumber(storm::utility::ceil(storm::utility::log10(storm::utility::one() / precision))); + + bool isSolution = false; + storm::dd::Add sharpenedX = sharpen(dir, p, rationalSolver, viResult.values, rationalB, isSolution); + + if (isSolution) { + status = SolverStatus::Converged; + } else { + precision = precision / 100; + } } - if (converged) { - STORM_LOG_INFO("Iterative solver (value iteration) converged in " << iterations << " iterations."); + if (status == SolverStatus::InProgress) { + status = SolverStatus::MaximalIterationsExceeded; + } + + if (status == SolverStatus::Converged) { + STORM_LOG_INFO("Iterative solver (rational search) converged in " << overallIterations << " iterations."); } else { - STORM_LOG_WARN("Iterative solver (value iteration) did not converge in " << iterations << " iterations."); + STORM_LOG_WARN("Iterative solver (rational search) did not converge in " << overallIterations << " iterations."); } - return xCopy; + return sharpenedX; + } + + template + template + typename std::enable_if::value && storm::NumberTraits::IsExact, storm::dd::Add>::type SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { + + storm::dd::Add rationalX = x.template toValueType(); + storm::dd::Add rationalB = b.template toValueType(); + SymbolicMinMaxLinearEquationSolver rationalSolver; + + storm::dd::Add rationalResult = solveEquationsRationalSearchHelper(dir, *this, *this, rationalX, rationalB, x, b); + return rationalResult.template toValueType(); + } + + template + template + typename std::enable_if::value && !storm::NumberTraits::IsExact, storm::dd::Add>::type SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { + + storm::dd::Add rationalX = x.template toValueType(); + storm::dd::Add rationalB = b.template toValueType(); + SymbolicMinMaxLinearEquationSolver rationalSolver; + + storm::dd::Add rationalResult = solveEquationsRationalSearchHelper(dir, rationalSolver, *this, rationalX, rationalB, x, b); + return rationalResult.template toValueType(); + } + + template + template + typename std::enable_if::value, storm::dd::Add>::type SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { + + storm::dd::Add impreciseX = x.template toValueType(); + storm::dd::Add impreciseB = b.template toValueType(); + SymbolicMinMaxLinearEquationSolver impreciseSolver; + + storm::dd::Add rationalResult = solveEquationsRationalSearchHelper(dir, *this, impreciseSolver, x, b, impreciseX, impreciseB); + return rationalResult.template toValueType(); + } + + template + storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsRationalSearch(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { + return solveEquationsRationalSearchHelper(dir, x, b); + } + + template + storm::dd::Add SymbolicMinMaxLinearEquationSolver::solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const { + // Set up the environment. + storm::dd::Add localX = x; + + // If we were given an initial scheduler, we take its solution as the starting point. + if (this->hasInitialScheduler()) { + localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b); + } + + ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion()); + + if (viResult.status == SolverStatus::Converged) { + STORM_LOG_INFO("Iterative solver (value iteration) converged in " << viResult.iterations << " iterations."); + } else { + STORM_LOG_WARN("Iterative solver (value iteration) did not converge in " << viResult.iterations << " iterations."); + } + + return viResult.values; } template diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index b99e72cd7..684c0f67d 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -7,11 +7,12 @@ #include #include "storm/solver/OptimizationDirection.h" - #include "storm/solver/SymbolicLinearEquationSolver.h" - #include "storm/solver/EquationSystemType.h" #include "storm/solver/MinMaxLinearEquationSolverRequirements.h" +#include "storm/solver/SolverStatus.h" + +#include "storm/utility/NumberTraits.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/dd/DdType.h" @@ -32,7 +33,7 @@ namespace storm { SymbolicMinMaxLinearEquationSolverSettings(); enum class SolutionMethod { - ValueIteration, PolicyIteration + ValueIteration, PolicyIteration, RationalSearch }; void setSolutionMethod(SolutionMethod const& solutionMethod); @@ -137,14 +138,47 @@ namespace storm { * Retrieves whether the solver is aware that the requirements were checked. */ bool isRequirementsCheckedSet() const; - + + /*! + * Determines whether the given vector x satisfies x = Ax + b. + */ + bool isSolution(OptimizationDirection dir, storm::dd::Add const& x, storm::dd::Add const& b) const; + private: storm::dd::Add solveEquationsWithScheduler(storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b) const; storm::dd::Add solveEquationsWithScheduler(SymbolicLinearEquationSolver& solver, storm::dd::Bdd const& scheduler, storm::dd::Add const& x, storm::dd::Add const& b, storm::dd::Add const& diagonal) const; storm::dd::Add solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; storm::dd::Add solveEquationsPolicyIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; - + storm::dd::Add solveEquationsRationalSearch(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; + + template + static storm::dd::Add sharpen(OptimizationDirection dir, uint64_t precision, SymbolicMinMaxLinearEquationSolver const& rationalSolver, storm::dd::Add const& x, storm::dd::Add const& rationalB, bool& isSolution); + + template + storm::dd::Add solveEquationsRationalSearchHelper(OptimizationDirection dir, SymbolicMinMaxLinearEquationSolver const& rationalSolver, SymbolicMinMaxLinearEquationSolver const& impreciseSolver, storm::dd::Add const& rationalX, storm::dd::Add const& rationalB, storm::dd::Add const& x, storm::dd::Add const& b) const; + template + typename std::enable_if::value && storm::NumberTraits::IsExact, storm::dd::Add>::type solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; + template + typename std::enable_if::value && !storm::NumberTraits::IsExact, storm::dd::Add>::type solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; + template + typename std::enable_if::value, storm::dd::Add>::type solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b) const; + + template + friend class SymbolicMinMaxLinearEquationSolver; + + struct ValueIterationResult { + ValueIterationResult(SolverStatus status, uint64_t iterations, storm::dd::Add const& values) : status(status), iterations(iterations), values(values) { + // Intentionally left empty. + } + + SolverStatus status; + uint64_t iterations; + storm::dd::Add values; + }; + + ValueIterationResult performValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add const& x, storm::dd::Add const& b, ValueType const& precision, bool relativeTerminationCriterion) const; + protected: // The matrix defining the coefficients of the linear equation system. storm::dd::Add A; diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 9132ac710..89f75bd41 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -129,10 +129,12 @@ namespace storm { template class SymbolicNativeLinearEquationSolverSettings; template class SymbolicNativeLinearEquationSolver; + template class SymbolicNativeLinearEquationSolver; template class SymbolicNativeLinearEquationSolver; template class SymbolicNativeLinearEquationSolver; template class SymbolicNativeLinearEquationSolverFactory; + template class SymbolicNativeLinearEquationSolverFactory; template class SymbolicNativeLinearEquationSolverFactory; template class SymbolicNativeLinearEquationSolverFactory; } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 92a0f78ab..ed8e2a966 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -976,30 +976,36 @@ namespace storm { template template - Add Add::toValueType() const { - if (std::is_same::value) { - return *this; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); - } - -#ifdef STORM_HAVE_CARL - template<> - template<> - Add Add::toValueType() const { - return Add(this->getDdManager(), internalAdd.toValueType(), this->getContainedMetaVariables()); + typename std::enable_if::value, Add>::type Add::toValueType() const { + return *this; } -#endif + + template + template + typename std::enable_if::value, Add>::type Add::toValueType() const { + return Add(this->getDdManager(), internalAdd.template toValueType(), this->getContainedMetaVariables()); + } template class Add; template class Add; template class Add; template class Add; - + #ifdef STORM_HAVE_CARL + template class Add; + template class Add; template class Add; + + template Add Add::toValueType() const; + template Add Add::toValueType() const; + template Add Add::toValueType() const; + + template Add Add::toValueType() const; + template Add Add::toValueType() const; + template Add Add::toValueType() const; + template Add Add::toValueType() const; #endif } } diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 1094bf0a1..8f3100b18 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -266,7 +266,9 @@ namespace storm { * @return The resulting function represented as an ADD. */ template - Add toValueType() const; + typename std::enable_if::value, Add>::type toValueType() const; + template + typename std::enable_if::value, Add>::type toValueType() const; /*! * Sum-abstracts from the given meta variables. diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 3303cc983..66c6d69a7 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -424,13 +424,16 @@ namespace storm { template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; - + template Add Bdd::toAdd() const; + template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; - +#ifdef STORM_HAVE_CARL + template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; +#endif template class Bdd; diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index be3809135..b711f5f92 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -481,14 +481,26 @@ namespace storm { template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; +#ifdef STORM_HAVE_CARL + template Add DdManager::getAddZero() const; +#endif + template Add DdManager::getAddOne() const; template Add DdManager::getAddOne() const; +#ifdef STORM_HAVE_CARL + template Add DdManager::getAddOne() const; +#endif + template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; template Add DdManager::getConstant(double const& value) const; template Add DdManager::getConstant(uint_fast64_t const& value) const; + +#ifdef STORM_HAVE_CARL + template Add DdManager::getConstant(storm::RationalNumber const& value) const; +#endif template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; diff --git a/src/storm/storage/dd/cudd/CuddAddIterator.cpp b/src/storm/storage/dd/cudd/CuddAddIterator.cpp index aad40db84..19e148390 100644 --- a/src/storm/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storm/storage/dd/cudd/CuddAddIterator.cpp @@ -4,6 +4,8 @@ #include "storm/utility/macros.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/constants.h" + #include namespace storm { @@ -14,7 +16,7 @@ namespace storm { } template - AddIterator::AddIterator(DdManager const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), generator(generator), cube(cube), valueAsDouble(static_cast(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager.getExpressionManager().getSharedPointer()) { + AddIterator::AddIterator(DdManager const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), generator(generator), cube(cube), valueAsDouble(storm::utility::convertNumber(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager.getExpressionManager().getSharedPointer()) { // If the given generator is not yet at its end, we need to create the current valuation from the cube from // scratch. if (!this->isAtEnd) { @@ -186,5 +188,9 @@ namespace storm { template class AddIterator; template class AddIterator; + +#ifdef STORM_HAVE_CARL + template class AddIterator; +#endif } } diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index f129177cb..325f0ad9a 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -143,6 +143,18 @@ namespace storm { return InternalAdd(ddManager, this->getCuddAdd().Maximum(other.getCuddAdd())); } + template + template + typename std::enable_if::value, InternalAdd>::type InternalAdd::toValueType() const { + return *this; + } + + template + template + typename std::enable_if::value, InternalAdd>::type InternalAdd::toValueType() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); + } + template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->getCuddAdd().ExistAbstract(cube.toAdd().getCuddAdd())); @@ -176,6 +188,11 @@ namespace storm { return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision); } } + + template<> + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, storm::RationalNumber const& precision, bool relative) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); + } template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { @@ -229,22 +246,42 @@ namespace storm { InternalBdd InternalAdd::greater(ValueType const& value) const { return InternalBdd(ddManager, this->getCuddAdd().BddStrictThreshold(value)); } - + + template<> + InternalBdd InternalAdd::greater(storm::RationalNumber const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); + } + template InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { return InternalBdd(ddManager, this->getCuddAdd().BddThreshold(value)); } + + template<> + InternalBdd InternalAdd::greaterOrEqual(storm::RationalNumber const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); + } template InternalBdd InternalAdd::less(ValueType const& value) const { return InternalBdd(ddManager, ~this->getCuddAdd().BddThreshold(value)); } + template<> + InternalBdd InternalAdd::less(storm::RationalNumber const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); + } + template InternalBdd InternalAdd::lessOrEqual(ValueType const& value) const { return InternalBdd(ddManager, ~this->getCuddAdd().BddStrictThreshold(value)); } + template<> + InternalBdd InternalAdd::lessOrEqual(storm::RationalNumber const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); + } + template InternalBdd InternalAdd::notZero() const { return InternalBdd(ddManager, this->getCuddAdd().BddPattern()); @@ -655,7 +692,21 @@ namespace storm { } } + template<> + DdNode* InternalAdd::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported"); + } + template class InternalAdd; + template InternalAdd InternalAdd::toValueType() const; template class InternalAdd; + template InternalAdd InternalAdd::toValueType() const; + +#ifdef STORM_HAVE_CARL + template class InternalAdd; + template InternalAdd InternalAdd::toValueType() const; + template InternalAdd InternalAdd::toValueType() const; + template InternalAdd InternalAdd::toValueType() const; +#endif } } diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 49adeea69..64e1176e7 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -262,6 +262,16 @@ namespace storm { */ InternalAdd maximum(InternalAdd const& other) const; + /*! + * Replaces the leaves in this MTBDD with the converted values in the target value type. + * + * @return The resulting function represented as an ADD. + */ + template + typename std::enable_if::value, InternalAdd>::type toValueType() const; + template + typename std::enable_if::value, InternalAdd>::type toValueType() const; + /*! * Sum-abstracts from the given cube. * diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index 87051bfc6..5fc12e567 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -528,6 +528,9 @@ namespace storm { template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalBdd::toAdd() const; +#endif template void InternalBdd::filterExplicitVectorRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); template void InternalBdd::filterExplicitVectorRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector& result, uint_fast64_t& currentIndex, std::vector const& values); @@ -537,5 +540,6 @@ namespace storm { template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; + template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; } } diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp index 7dd5b75f6..0bfc8c1ad 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp @@ -102,6 +102,11 @@ namespace storm { return InternalAdd(this, cuddManager.constant(value)); } + template<> + InternalAdd InternalDdManager::getConstant(storm::RationalNumber const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported."); + } + std::vector> InternalDdManager::createDdVariables(uint64_t numberOfLayers, boost::optional const& position) { std::vector> result; @@ -166,11 +171,14 @@ namespace storm { template InternalAdd InternalDdManager::getAddOne() const; template InternalAdd InternalDdManager::getAddOne() const; - + template InternalAdd InternalDdManager::getAddOne() const; + template InternalAdd InternalDdManager::getAddZero() const; template InternalAdd InternalDdManager::getAddZero() const; - + template InternalAdd InternalDdManager::getAddZero() const; + template InternalAdd InternalDdManager::getConstant(double const& value) const; template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; + template InternalAdd InternalDdManager::getConstant(storm::RationalNumber const& value) const; } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index d3f0f3b85..3eca707ca 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -457,7 +457,12 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.ToDoubleRN()); } - + template<> + template<> + InternalAdd InternalAdd::toValueType() const { + return InternalAdd(ddManager, this->sylvanMtbdd.ToRationalNumber()); + } + #ifdef STORM_HAVE_CARL template<> template<> diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 99f7609ef..139d39ee4 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -256,7 +256,7 @@ namespace storm { InternalAdd maximum(InternalAdd const& other) const; /*! - * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else. + * Replaces the leaves in this MTBDD with the converted values in the target value type. * * @return The resulting function represented as an ADD. */ diff --git a/src/test/storm/storage/SylvanDdTest.cpp b/src/test/storm/storage/SylvanDdTest.cpp index ca294b273..1a34cdf71 100644 --- a/src/test/storm/storage/SylvanDdTest.cpp +++ b/src/test/storm/storage/SylvanDdTest.cpp @@ -855,6 +855,23 @@ TEST(SylvanDd, AddSharpenTest) { ASSERT_EQ(storm::utility::convertNumber(std::string("19/10")), sharpened.getValue(metaVariableToValueMap)); } +TEST(SylvanDd, AddToRationalTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add dd = manager->template getAddOne(); + ASSERT_NO_THROW(dd.setValue(x.first, 4, 0.4)); + ASSERT_EQ(2ul, dd.getLeafCount()); + + storm::dd::Add rationalDd = dd.template toValueType(); + + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(x.first, 4); + + ASSERT_EQ(storm::utility::convertNumber(std::string("4/10")), rationalDd.getValue(metaVariableToValueMap)); +} + + TEST(SylvanDd, BddOddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair a = manager->addMetaVariable("a");