started on hybrid solution of abstraction

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -32,7 +32,6 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/AbstractionSettings.h"
 
 #include "storm/utility/prism.h"
 #include "storm/utility/macros.h"
@@ -50,7 +49,7 @@ namespace storm {
         using storm::abstraction::QuantitativeGameResultMinMax;
         
         template<storm::dd::DdType Type, typename ModelType>
-        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) {
+        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()) {
             model.requireNoUndefinedConstants();
             if (model.isPrismProgram()) {
                 storm::prism::Program const& originalProgram = model.asPrismProgram();
@@ -424,10 +423,13 @@ namespace storm {
                 // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
                 if (!qualitativeRefinement) {
                     // At this point, we know that we cannot answer the query without further numeric computation.
+                    STORM_LOG_TRACE("Starting numerical solution step.");
 
+                    // Solve abstraction using the selected mode.
+                    if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) {
+                        STORM_LOG_TRACE("Using dd-based solving.");
                         storm::dd::Add<Type, ValueType> initialStatesAdd = initialStates.template toAdd<ValueType>();
                         
-                    STORM_LOG_TRACE("Starting numerical solution step.");
                         auto quantitativeStart = std::chrono::high_resolution_clock::now();
                         
                         QuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
@@ -471,6 +473,22 @@ namespace storm {
                         refiner.refine(game, transitionMatrixBdd, quantitativeResult);
                         auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
                         STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
+                    } else {
+                        STORM_LOG_TRACE("Using hybrid solving.");
+
+                        storm::dd::Odd odd = (maybeMin || maybeMax || targetStates).createOdd();
+                        
+                        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> transitionMatrixLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), odd, odd, true);
+                        auto const& transitionMatrix = transitionMatrixLabeling.first;
+                        auto const& labeling = transitionMatrixLabeling.second;
+                        
+                        std::cout << transitionMatrix << std::endl;
+                        for (auto const& e : labeling) {
+                            std::cout << e << std::endl;
+                        }
+                        
+                        exit(-1);
+                    }
 
                 }
                 auto iterationEnd = std::chrono::high_resolution_clock::now();

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -14,6 +14,8 @@
 
 #include "storm/logic/Bound.h"
 
+#include "storm/settings/modules/AbstractionSettings.h"
+
 #include "storm/utility/ConstantsComparator.h"
 #include "storm/utility/solver.h"
 #include "storm/utility/graph.h"
@@ -95,6 +97,9 @@ namespace storm {
             
             /// A flag indicating whether to reuse the quantitative results.
             bool reuseQuantitativeResults;
+            
+            /// The mode selected for solving the abstraction.
+            storm::settings::modules::AbstractionSettings::SolveMode solveMode;
         };
     }
 }

src/storm/settings/modules/AbstractionSettings.cpp

@@ -22,6 +22,7 @@ namespace storm {
             const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic";
             const std::string AbstractionSettings::reuseResultsOptionName = "reuse";
             const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant";
+            const std::string AbstractionSettings::solveModeOptionName = "solve";
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@@ -43,6 +44,12 @@ namespace storm {
                                              .setDefaultValueString("all").build())
                                 .build());
 
+                std::vector<std::string> solveModes = {"dd", "hybrid"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, solveModeOptionName, true, "Sets how the abstractions are solved.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(solveModes))
+                                             .setDefaultValueString("dd").build())
+                                .build());
+
                 this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("on").build())
@@ -98,6 +105,14 @@ namespace storm {
                 return SplitMode::All;
             }
             
+            AbstractionSettings::SolveMode AbstractionSettings::getSolveMode() const {
+                std::string solveModeAsString = this->getOption(solveModeOptionName).getArgumentByName("mode").getValueAsString();
+                if (solveModeAsString == "dd") {
+                    return SolveMode::Dd;
+                }
+                return SolveMode::Hybrid;
+            }
+            
             bool AbstractionSettings::isAddAllGuardsSet() const {
                 return this->getOption(addAllGuardsOptionName).getArgumentByName("value").getValueAsString() == "on";
             }

src/storm/settings/modules/AbstractionSettings.h

@@ -27,6 +27,10 @@ namespace storm {
                     All, None, Qualitative, Quantitative
                 };
                 
+                enum class SolveMode {
+                    Dd, Hybrid
+                };
+                
                 /*!
                  * Creates a new set of abstraction settings.
                  */
@@ -100,6 +104,11 @@ namespace storm {
                  */
                 bool isRestrictToRelevantStatesSet() const;
                 
+                /*!
+                 * Retrieves the mode with which to solve the games.
+                 */
+                SolveMode getSolveMode() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -112,6 +121,7 @@ namespace storm {
                 const static std::string pivotHeuristicOptionName;
                 const static std::string reuseResultsOptionName;
                 const static std::string restrictToRelevantStatesOptionName;
+                const static std::string solveModeOptionName;
             };
             
         }

src/storm/storage/dd/Add.cpp

@@ -703,11 +703,11 @@ namespace storm {
             }
             
             // Create the canonical row group sizes and build the matrix.
-            return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd);
+            return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd).first;
         }
 
         template<DdType LibraryType, typename ValueType>
-        storm::storage::SparseMatrix<ValueType> Add<LibraryType, ValueType>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const {
+        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> Add<LibraryType, ValueType>::toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const {
             std::vector<uint_fast64_t> ddRowVariableIndices;
             std::vector<uint_fast64_t> ddColumnVariableIndices;
             std::vector<uint_fast64_t> ddGroupVariableIndices;
@@ -760,12 +760,24 @@ namespace storm {
                 groups.push_back(Add<LibraryType, ValueType>(this->getDdManager(), internalAdd, rowAndColumnMetaVariables));
             }
             
+            // Create the group labelings if requested.
+            std::vector<uint64_t> groupLabels;
+            if (buildLabeling) {
+                groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices);
+                STORM_LOG_ASSERT(groupLabels.size() == groups.size(), "Mismatching label sizes.");
+            }
+            
             // Create the actual storage for the non-zero entries.
             std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>> columnsAndValues(this->getNonZeroCount());
             
             // Now compute the indices at which the individual rows start.
             std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
             
+            std::vector<uint64_t> labeling;
+            if (buildLabeling) {
+                labeling.resize(rowGroupIndices.back());
+            }
+            
             std::vector<InternalAdd<LibraryType, uint_fast64_t>> statesWithGroupEnabled(groups.size());
             InternalAdd<LibraryType, uint_fast64_t> stateToRowGroupCount = this->getDdManager().template getAddZero<uint_fast64_t>();
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
@@ -779,6 +791,11 @@ namespace storm {
                 
                 statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd<uint_fast64_t>();
                 statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
+                
+                if (buildLabeling) {
+                    uint64_t currentLabel = groupLabels[i];
+                    statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, labeling, [currentLabel] (uint_fast64_t a, uint_fast64_t l) { return currentLabel; });
+                }
             }
             
             // Since we modified the rowGroupIndices, we need to restore the correct values.
@@ -812,7 +829,7 @@ namespace storm {
             }
             rowIndications[0] = 0;
             
-            return storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
+            return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), labeling);
         }
         
         template<DdType LibraryType, typename ValueType>

src/storm/storage/dd/Add.h

@@ -640,6 +640,23 @@ namespace storm {
              */
             storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
             
+            /*!
+             * Converts the ADD to a row-grouped (sparse) matrix. The given offset-labeled DDs are used to determine the
+             * correct row and column, respectively, for each entry. If requested, it builds a labeling of the rows
+             * that is derived from the group variable encodings. Note: this function assumes that the meta variables
+             * used to distinguish different row groups are at the very top of the ADD.
+             *
+             * @param rowMetaVariables The meta variables that encode the rows of the matrix.
+             * @param columnMetaVariables The meta variables that encode the columns of the matrix.
+             * @param groupMetaVariables The meta variables that are used to distinguish different row groups.
+             * @param rowOdd The ODD used for determining the correct row.
+             * @param columnOdd The ODD used for determining the correct column.
+             * @param buildLabeling If false, no labeling vector is built.
+             * @return The matrix that is represented by this ADD and a vector corresponding to row labeling
+             * (if requested).
+             */
+            std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const;
+            
             /*!
              * Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector.
              * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each
@@ -721,22 +738,6 @@ namespace storm {
              */
             operator InternalAdd<LibraryType, ValueType>() const;
             
-            /*!
-             * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also
-             * translated to an explicit row-grouped vector with the same row-grouping. The given offset-labeled DDs
-             * are used to determine the correct row and column, respectively, for each entry. Note: this function
-             * assumes that the meta variables used to distinguish different row groups are at the very top of the ADD.
-             *
-             * @param rowMetaVariables The meta variables that encode the rows of the matrix.
-             * @param columnMetaVariables The meta variables that encode the columns of the matrix.
-             * @param groupMetaVariables The meta variables that are used to distinguish different row groups.
-             * @param rowOdd The ODD used for determining the correct row.
-             * @param columnOdd The ODD used for determining the correct column.
-             * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector
-             * (if it was given).
-             */
-            storm::storage::SparseMatrix<ValueType> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const;
-            
             /*!
              * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped
              * explicit vector. The given offset-labeled DDs are used to determine the correct row and column,

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

@@ -524,6 +524,31 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        std::vector<uint64_t> InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
+            std::vector<uint64_t> result;
+            decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), 0);
+            return result;
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
+            // For the empty DD, we do not need to create a group.
+            if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
+                return;
+            }
+            
+            if (currentLevel == maxLevel) {
+                labels.push_back(label);
+            } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
+                decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
+                decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1);
+            } else {
+                decodeGroupLabelsRec(Cudd_E(dd), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
+                decodeGroupLabelsRec(Cudd_T(dd), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1 );
+            }
+        }
+        
         template<typename ValueType>
         std::vector<InternalAdd<DdType::CUDD, ValueType>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
             std::vector<InternalAdd<DdType::CUDD, ValueType>> result;

src/storm/storage/dd/cudd/InternalCuddAdd.h

@@ -570,6 +570,15 @@ namespace storm {
              */
             std::vector<InternalAdd<DdType::CUDD, ValueType>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
             
+            /*!
+             * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices).
+             * The labeling is then made by interpreting the group encodings as binary encodings.
+             *
+             * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups.
+             * @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables).
+             */
+            std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
+            
             /*!
              * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of
              * the given group variables (given via indices).
@@ -661,6 +670,19 @@ namespace storm {
              */
             void splitIntoGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const;
             
+            /*!
+             * Splits the given matrix DD into the labelings of the gropus using the given group variables.
+             *
+             * @param dd The DD to split.
+             * @param labels A vector that is to be filled with the labels of the individual groups.
+             * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
+             * @param currentLevel The currently considered level in the DD.
+             * @param maxLevel The number of levels that need to be considered.
+             * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split.
+             * @param label The currently followed label.
+             */
+            void decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const;
+            
             /*!
              * Splits the given DDs into the groups using the given group variables.
              *

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -921,6 +921,36 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        std::vector<uint64_t> InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
+            std::vector<uint64_t> result;
+            decodeGroupLabelsRec(mtbdd_regular(this->getSylvanMtbdd().GetMTBDD()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), 0);
+            return result;
+        }
+        
+        template<typename ValueType>
+        void InternalAdd<DdType::Sylvan, ValueType>::decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const {
+            // For the empty DD, we do not need to create a group.
+            if (mtbdd_isleaf(dd) && mtbdd_iszero(dd)) {
+                return;
+            }
+
+            if (currentLevel == maxLevel) {
+                labels.push_back(label);
+            } else if (mtbdd_isleaf(dd) || ddGroupVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
+                decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
+                decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1);
+            } else {
+                // Otherwise, we compute the ODDs for both the then- and else successors.
+                MTBDD thenDdNode = mtbdd_gethigh(dd);
+                MTBDD elseDdNode = mtbdd_getlow(dd);
+
+                decodeGroupLabelsRec(mtbdd_regular(elseDdNode), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, label << 1);
+                decodeGroupLabelsRec(mtbdd_regular(thenDdNode), labels, ddGroupVariableIndices, currentLevel + 1, maxLevel, (label << 1) | 1 );
+                
+            }
+        }
+        
         template<typename ValueType>
         std::vector<InternalAdd<DdType::Sylvan, ValueType>> InternalAdd<DdType::Sylvan, ValueType>::splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
             std::vector<InternalAdd<DdType::Sylvan, ValueType>> result;

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -561,6 +561,15 @@ namespace storm {
              */
             std::vector<InternalAdd<DdType::Sylvan, ValueType>> splitIntoGroups(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
             
+            /*!
+             * Splits the ADD into several ADDs that differ in the encoding of the given group variables (given via indices).
+             * The labeling is then made by interpreting the group encodings as binary encodings.
+             *
+             * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups.
+             * @return A vector of ADDs that are the separate groups (wrt. to the encoding of the given variables).
+             */
+            std::vector<uint64_t> decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices) const;
+            
             /*!
              * Simultaneously splits the ADD and the given vector ADD into several ADDs that differ in the encoding of
              * the given group variables (given via indices).
@@ -651,6 +660,19 @@ namespace storm {
              */
             void composeWithExplicitVectorRec(MTBDD dd, bool negated, std::vector<uint_fast64_t> const* offsets, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, ValueType const&)> const& function) const;
             
+            /*!
+             * Splits the given matrix DD into the labelings of the gropus using the given group variables.
+             *
+             * @param dd The DD to split.
+             * @param labels A vector that is to be filled with the labels of the individual groups.
+             * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered.
+             * @param currentLevel The currently considered level in the DD.
+             * @param maxLevel The number of levels that need to be considered.
+             * @param remainingMetaVariables The meta variables that remain in the DDs after the groups have been split.
+             * @param label The currently followed label.
+             */
+            void decodeGroupLabelsRec(MTBDD dd, std::vector<uint64_t>& labels, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint64_t label) const;
+            
             /*!
              * Splits the given matrix DD into the groups using the given group variables.
              *