From f5ba5204c91c0ae9fe3efd7c005ac12a90948afb Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Jul 2017 22:28:17 +0200 Subject: [PATCH] adding some debug functionality to DdManager to corner dynamic reordering issue with CUDD --- CMakeLists.txt | 2 ++ resources/3rdparty/include_cudd.cmake | 9 ++++++++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 5 +---- src/storm/settings/modules/CuddSettings.cpp | 13 ++++++++++--- src/storm/settings/modules/CuddSettings.h | 8 ++++++++ .../modules/EigenEquationSolverSettings.cpp | 2 +- .../modules/NativeEquationSolverSettings.cpp | 2 +- src/storm/solver/LinearEquationSolver.h | 6 +++--- .../solver/StandardMinMaxLinearEquationSolver.cpp | 2 +- .../solver/SymbolicNativeLinearEquationSolver.cpp | 2 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 1 - src/storm/storage/dd/DdManager.cpp | 5 +++++ src/storm/storage/dd/DdManager.h | 5 +++++ src/storm/storage/dd/cudd/InternalCuddDdManager.cpp | 13 +++++++++++-- src/storm/storage/dd/cudd/InternalCuddDdManager.h | 5 +++++ .../storage/dd/sylvan/InternalSylvanDdManager.cpp | 4 ++++ .../storage/dd/sylvan/InternalSylvanDdManager.h | 5 +++++ 17 files changed, 71 insertions(+), 18 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d5b905eb1..f8cfcea20 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -49,6 +49,8 @@ export_option(STORM_USE_CLN_EA) option(STORM_USE_CLN_RF "Sets whether CLN instead of GMP numbers should be used for rational functions." ON) export_option(STORM_USE_CLN_RF) option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF) +option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF) +MARK_AS_ADVANCED(STORM_DEBUG_CUDD) set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index e4bcebcb9..3030f44b3 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -16,7 +16,14 @@ endif() set(CUDD_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib) -set(STORM_CUDD_FLAGS "CFLAGS=-O3 -w -DPIC -DHAVE_IEEE_754 -fno-common -ffast-math -fno-finite-math-only") +# create CUDD compilation flags +if (NOT STORM_DEBUG_CUDD) + set(STORM_CUDD_FLAGS "-O3") +else() + message(WARNING "Building CUDD in DEBUG mode.") + set(STORM_CUDD_FLAGS "-O0 -g") +endif() +set(STORM_CUDD_FLAGS "CFLAGS=${STORM_CUDD_FLAGS} -w -DPIC -DHAVE_IEEE_754 -fno-common -ffast-math -fno-finite-math-only") if (NOT STORM_PORTABLE) set(STORM_CUDD_FLAGS "${STORM_CUDD_FLAGS} -march=native") endif() diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index b10934fdb..13dc404ed 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -388,10 +388,8 @@ namespace storm { MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); - // Determine which states have a reward that is infinity or less than infinity. storm::storage::BitVector maybeStates, infinityStates; if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { @@ -497,7 +495,6 @@ namespace storm { } STORM_LOG_ASSERT((!produceScheduler && !scheduler) || (!scheduler->isPartialScheduler() && scheduler->isDeterministicScheduler() && scheduler->isMemorylessScheduler()), "Unexpected format of obtained scheduler."); - return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } @@ -510,7 +507,7 @@ namespace storm { } // Likewise, if all bits are set, we can avoid the computation and set. - if ((~psiStates).empty()) { + if (psiStates.full()) { return std::vector(numberOfStates, storm::utility::one()); } diff --git a/src/storm/settings/modules/CuddSettings.cpp b/src/storm/settings/modules/CuddSettings.cpp index e680276bf..89e299aee 100644 --- a/src/storm/settings/modules/CuddSettings.cpp +++ b/src/storm/settings/modules/CuddSettings.cpp @@ -17,12 +17,15 @@ namespace storm { const std::string CuddSettings::moduleName = "cudd"; const std::string CuddSettings::precisionOptionName = "precision"; const std::string CuddSettings::maximalMemoryOptionName = "maxmem"; - const std::string CuddSettings::reorderOptionName = "reorder"; + const std::string CuddSettings::reorderOptionName = "dynreorder"; + const std::string CuddSettings::reorderTechniqueOptionName = "reordertechnique"; CuddSettings::CuddSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, false, "Sets whether dynamic reordering is allowed.").build()); std::vector reorderingTechniques; reorderingTechniques.push_back("none"); @@ -43,7 +46,7 @@ namespace storm { reorderingTechniques.push_back("annealing"); reorderingTechniques.push_back("genetic"); reorderingTechniques.push_back("exact"); - this->addOption(storm::settings::OptionBuilder(moduleName, reorderOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines.").setDefaultValueString("gsift").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reorderingTechniques)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, reorderTechniqueOptionName, true, "Sets the reordering technique used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used by Cudd's reordering routines.").setDefaultValueString("gsift").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reorderingTechniques)).build()).build()); } double CuddSettings::getConstantPrecision() const { @@ -54,8 +57,12 @@ namespace storm { return this->getOption(maximalMemoryOptionName).getArgumentByName("value").getValueAsUnsignedInteger(); } + bool CuddSettings::isReorderingEnabled() const { + return this->getOption(reorderOptionName).getHasOptionBeenSet(); + } + CuddSettings::ReorderingTechnique CuddSettings::getReorderingTechnique() const { - std::string reorderingTechniqueAsString = this->getOption(reorderOptionName).getArgumentByName("method").getValueAsString(); + std::string reorderingTechniqueAsString = this->getOption(reorderTechniqueOptionName).getArgumentByName("method").getValueAsString(); if (reorderingTechniqueAsString == "none") { return CuddSettings::ReorderingTechnique::None; } else if (reorderingTechniqueAsString == "random") { diff --git a/src/storm/settings/modules/CuddSettings.h b/src/storm/settings/modules/CuddSettings.h index 01a81389c..5c4e22da2 100644 --- a/src/storm/settings/modules/CuddSettings.h +++ b/src/storm/settings/modules/CuddSettings.h @@ -34,6 +34,13 @@ namespace storm { */ uint_fast64_t getMaximalMemory() const; + /*! + * Retrieves whether dynamic reordering is enabled. + * + * @return True iff dynamic reordering is enabled. + */ + bool isReorderingEnabled() const; + /*! * Retrieves the reordering technique that CUDD is supposed to use. * @@ -49,6 +56,7 @@ namespace storm { static const std::string precisionOptionName; static const std::string maximalMemoryOptionName; static const std::string reorderOptionName; + static const std::string reorderTechniqueOptionName; }; } // namespace modules diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp index 937f36026..cc3589937 100644 --- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp +++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp @@ -26,7 +26,7 @@ namespace storm { EigenEquationSolverSettings::EigenEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = {"sparselu", "bicgstab", "dgmres", "gmres"}; - this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the eigen solver.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("sparselu").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the eigen solver.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("gmres").build()).build()); // Register available preconditioners. std::vector preconditioner = {"ilu", "diagonal", "none"}; diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index 7803939bf..26a15ea67 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -25,7 +25,7 @@ namespace storm { NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = { "jacobi", "gaussseidel", "sor" }; - this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("gaussseidel").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h index b94626cd2..170d625f7 100644 --- a/src/storm/solver/LinearEquationSolver.h +++ b/src/storm/solver/LinearEquationSolver.h @@ -85,17 +85,17 @@ namespace storm { virtual void clearCache() const; /*! - * Sets a lower bound for the solution that can potentially used by the solver. + * Sets a lower bound for the solution that can potentially be used by the solver. */ void setLowerBound(ValueType const& value); /*! - * Sets an upper bound for the solution that can potentially used by the solver. + * Sets an upper bound for the solution that can potentially be used by the solver. */ void setUpperBound(ValueType const& value); /*! - * Sets bounds for the solution that can potentially used by the solver. + * Sets bounds for the solution that can potentially be used by the solver. */ void setBounds(ValueType const& lower, ValueType const& upper); diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 627dcd131..1162ee496 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -106,7 +106,7 @@ namespace storm { std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A.getRowGroupCount()); // Get a vector for storing the right-hand side of the inner equation system. - if(!auxiliaryRowGroupVector) { + if (!auxiliaryRowGroupVector) { auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); } std::vector& subB = *auxiliaryRowGroupVector; diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 000e25926..2d0e82a1d 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -69,7 +69,7 @@ namespace storm { storm::dd::Add lu = diagonal.ite(manager.template getAddZero(), this->A); storm::dd::Add diagonalAdd = diagonal.template toAdd(); storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); - + storm::dd::Add scaledLu = lu / diag; storm::dd::Add scaledB = b / diag; diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index d47bff510..88a7ea218 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -453,7 +453,6 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices()); - } } diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index b029da879..a27e86dea 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -464,6 +464,11 @@ namespace storm { return &internalDdManager; } + template + void DdManager::debugCheck() const { + internalDdManager.debugCheck(); + } + template class DdManager; template Add DdManager::getAddZero() const; diff --git a/src/storm/storage/dd/DdManager.h b/src/storm/storage/dd/DdManager.h index fdee32589..2d2405bb6 100644 --- a/src/storm/storage/dd/DdManager.h +++ b/src/storm/storage/dd/DdManager.h @@ -290,6 +290,11 @@ namespace storm { * @return The internal DD manager. */ InternalDdManager const& getInternalDdManager() const; + + /*! + * Performs a debug check if available. + */ + void debugCheck() const; private: /*! diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp index 0585b793e..e7b7961fe 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.cpp @@ -10,10 +10,12 @@ namespace storm { InternalDdManager::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), numberOfDdVariables(0) { this->cuddManager.SetMaxMemory(static_cast(storm::settings::getModule().getMaximalMemory() * 1024ul * 1024ul)); - this->cuddManager.SetEpsilon(storm::settings::getModule().getConstantPrecision()); + + auto const& settings = storm::settings::getModule(); + this->cuddManager.SetEpsilon(settings.getConstantPrecision()); // Now set the selected reordering technique. - storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::getModule().getReorderingTechnique(); + storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = settings.getReorderingTechnique(); switch (reorderingTechniqueAsSetting) { case storm::settings::modules::CuddSettings::ReorderingTechnique::None: this->reorderingTechnique = CUDD_REORDER_NONE; break; case storm::settings::modules::CuddSettings::ReorderingTechnique::Random: this->reorderingTechnique = CUDD_REORDER_RANDOM; break; @@ -34,6 +36,8 @@ namespace storm { case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic: this->reorderingTechnique = CUDD_REORDER_GENETIC; break; case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact: this->reorderingTechnique = CUDD_REORDER_EXACT; break; } + + this->allowDynamicReordering(settings.isReorderingEnabled()); } InternalDdManager::~InternalDdManager() { @@ -111,6 +115,11 @@ namespace storm { this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0); } + void InternalDdManager::debugCheck() const { + this->getCuddManager().CheckKeys(); + this->getCuddManager().DebugCheck(); + } + cudd::Cudd& InternalDdManager::getCuddManager() { return cuddManager; } diff --git a/src/storm/storage/dd/cudd/InternalCuddDdManager.h b/src/storm/storage/dd/cudd/InternalCuddDdManager.h index 08717f345..44efef0c5 100644 --- a/src/storm/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storm/storage/dd/cudd/InternalCuddDdManager.h @@ -119,6 +119,11 @@ namespace storm { */ void triggerReordering(); + /*! + * Performs a debug check if available. + */ + void debugCheck() const; + /*! * Retrieves the number of DD variables managed by this manager. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index 85f1d2fa4..11c7b09d6 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -207,6 +207,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); } + void InternalDdManager::debugCheck() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); + } + uint_fast64_t InternalDdManager::getNumberOfDdVariables() const { return nextFreeVariableIndex; } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h index 71db91b7e..c10915145 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h @@ -120,6 +120,11 @@ namespace storm { */ void triggerReordering(); + /*! + * Performs a debug check if available. + */ + void debugCheck() const; + /*! * Retrieves the number of DD variables managed by this manager. *