adding some debug functionality to DdManager to corner dynamic reordering issue with CUDD

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).")

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()

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -388,10 +388,8 @@ namespace storm {
             MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
                 
                 std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
-
                 std::vector<uint_fast64_t> 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<ValueType>().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<ValueType>(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<ValueType>(numberOfStates, storm::utility::one<ValueType>());
                 }
                 

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<std::string> 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") {

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

src/storm/settings/modules/EigenEquationSolverSettings.cpp

@@ -26,7 +26,7 @@ namespace storm {
             
             EigenEquationSolverSettings::EigenEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> 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<std::string> preconditioner = {"ilu", "diagonal", "none"};

src/storm/settings/modules/NativeEquationSolverSettings.cpp

@@ -25,7 +25,7 @@ namespace storm {
             
             NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> 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());
                 

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);
 

src/storm/solver/StandardMinMaxLinearEquationSolver.cpp

@@ -106,7 +106,7 @@ namespace storm {
             std::vector<storm::storage::sparse::state_type> scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector<storm::storage::sparse::state_type>(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<std::vector<ValueType>>(this->A.getRowGroupCount());
             }
             std::vector<ValueType>& subB = *auxiliaryRowGroupVector;

src/storm/solver/SymbolicNativeLinearEquationSolver.cpp

@@ -69,7 +69,7 @@ namespace storm {
             storm::dd::Add<DdType, ValueType> lu = diagonal.ite(manager.template getAddZero<ValueType>(), this->A);
             storm::dd::Add<DdType, ValueType> diagonalAdd = diagonal.template toAdd<ValueType>();
             storm::dd::Add<DdType, ValueType> diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables);
-            
+
             storm::dd::Add<DdType, ValueType> scaledLu = lu / diag;
             storm::dd::Add<DdType, ValueType> scaledB = b / diag;
             

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());
-                
             }
         }
 

src/storm/storage/dd/DdManager.cpp

@@ -464,6 +464,11 @@ namespace storm {
             return &internalDdManager;
         }
         
+        template<DdType LibraryType>
+        void DdManager<LibraryType>::debugCheck() const {
+            internalDdManager.debugCheck();
+        }
+        
         template class DdManager<DdType::CUDD>;
         
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getAddZero() const;

src/storm/storage/dd/DdManager.h

@@ -290,6 +290,11 @@ namespace storm {
              * @return The internal DD manager.
              */
             InternalDdManager<LibraryType> const& getInternalDdManager() const;
+            
+            /*!
+             * Performs a debug check if available.
+             */
+            void debugCheck() const;
 
         private:
             /*!

src/storm/storage/dd/cudd/InternalCuddDdManager.cpp

@@ -10,10 +10,12 @@ namespace storm {
         
         InternalDdManager<DdType::CUDD>::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), numberOfDdVariables(0) {
             this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::getModule<storm::settings::modules::CuddSettings>().getMaximalMemory() * 1024ul * 1024ul));
-            this->cuddManager.SetEpsilon(storm::settings::getModule<storm::settings::modules::CuddSettings>().getConstantPrecision());
+            
+            auto const& settings = storm::settings::getModule<storm::settings::modules::CuddSettings>();
+            this->cuddManager.SetEpsilon(settings.getConstantPrecision());
             
             // Now set the selected reordering technique.
-            storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = storm::settings::getModule<storm::settings::modules::CuddSettings>().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<DdType::CUDD>::~InternalDdManager() {
@@ -111,6 +115,11 @@ namespace storm {
             this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0);
         }
         
+        void InternalDdManager<DdType::CUDD>::debugCheck() const {
+            this->getCuddManager().CheckKeys();
+            this->getCuddManager().DebugCheck();
+        }
+        
         cudd::Cudd& InternalDdManager<DdType::CUDD>::getCuddManager() {
             return cuddManager;
         }

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.
              *

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<DdType::Sylvan>::debugCheck() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+        
         uint_fast64_t InternalDdManager<DdType::Sylvan>::getNumberOfDdVariables() const {
             return nextFreeVariableIndex;
         }

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.
              *