more work on introducing relation products

Former-commit-id: 6b78fa09d2

src/builder/DdPrismModelBuilder.cpp

@@ -1174,7 +1174,7 @@ namespace storm {
             do {
                 STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis.");
                 changed = false;
-                storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables);
+                storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
                 storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates);
                                 
                 // Check whether new states were indeed discovered.

src/storage/dd/Bdd.cpp

@@ -143,10 +143,10 @@ namespace storm {
         }
         
         template<DdType LibraryType>
-        Bdd<LibraryType> Bdd<LibraryType>::relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables) const {
+        Bdd<LibraryType> Bdd<LibraryType>::relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
             std::set<storm::expressions::Variable> tmpMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, relation);
             std::set<storm::expressions::Variable> newMetaVariables;
-            std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+            std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
             
             std::vector<InternalBdd<LibraryType>> rowVariables;
             for (auto const& metaVariable : rowMetaVariables) {
@@ -159,6 +159,23 @@ namespace storm {
             return Bdd<LibraryType>(this->getDdManager(), internalBdd.relationalProduct(relation, rowVariables), newMetaVariables);
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> Bdd<LibraryType>::inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
+            std::set<storm::expressions::Variable> tmpMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, relation);
+            std::set<storm::expressions::Variable> newMetaVariables;
+            std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+            
+            std::vector<InternalBdd<LibraryType>> columnVariables;
+            for (auto const& metaVariable : columnMetaVariables) {
+                DdMetaVariable<LibraryType> const& variable = this->getDdManager()->getMetaVariable(metaVariable);
+                for (auto const& ddVariable : variable.getDdVariables()) {
+                    columnVariables.push_back(ddVariable);
+                }
+            }
+            
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, columnVariables), newMetaVariables);
+        }
+        
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
             std::set<storm::expressions::Variable> newContainedMetaVariables;

src/storage/dd/Bdd.h

@@ -187,13 +187,26 @@ namespace storm {
             Bdd<LibraryType> restrict(Bdd<LibraryType> const& constraint) const;
             
             /*!
-             * Computes the relational product of the current BDD and the given BDD representing a relation.
+             * Computes the relational product of the current BDD and the given BDD representing a relation. Note that
+             * this operation assumes that the row and column variables are interleaved.
              *
              * @param relation The relation to use.
              * @param rowMetaVariables The row meta variables used in the relation.
-             * @return The ralational product.
+             * @param columnMetaVariables The row meta variables used in the relation.
+             * @return The relational product.
              */
-            Bdd<LibraryType> relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables) const;
+            Bdd<LibraryType> relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const;
+            
+            /*!
+             * Computes the inverse relational product of the current BDD and the given BDD representing a relation.
+             * Note that this operation assumes that the row and column variables are interleaved.
+             *
+             * @param relation The relation to use.
+             * @param rowMetaVariables The row meta variables used in the relation.
+             * @param columnMetaVariables The row meta variables used in the relation.
+             * @return The inverse relational product.
+             */
+            Bdd<LibraryType> inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const;
             
             /*!
              * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have

src/storage/dd/cudd/InternalCuddBdd.cpp

@@ -37,7 +37,7 @@ namespace storm {
             
             InternalBdd<DdType::CUDD> result = this->andExists(relation, cube);
             
-            // Create the corresponding "from" vector for the variable swap.
+            // Create the corresponding column variable vector for the variable swap.
             std::vector<InternalBdd<DdType::CUDD>> columnVariables;
             for (auto const& variable : rowVariables) {
                 columnVariables.push_back(InternalBdd<DdType::CUDD>(ddManager, ddManager->getCuddManager().bddVar(variable.getIndex() + 1)));
@@ -47,6 +47,24 @@ namespace storm {
             return result;
         }
         
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::inverseRelationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const {
+            InternalBdd<DdType::CUDD> cube = ddManager->getBddOne();
+            for (auto const& variable : columnVariables) {
+                cube &= variable;
+            }
+            
+            InternalBdd<DdType::CUDD> result = this->andExists(relation, cube);
+            
+            // Create the corresponding column variable vector for the variable swap.
+            std::vector<InternalBdd<DdType::CUDD>> rowVariables;
+            for (auto const& variable : rowVariables) {
+                rowVariables.push_back(InternalBdd<DdType::CUDD>(ddManager, ddManager->getCuddManager().bddVar(variable.getIndex() - 1)));
+            }
+            result = result.swapVariables(rowVariables, columnVariables);
+            
+            return result;
+        }
+        
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::ite(InternalBdd<DdType::CUDD> const& thenDd, InternalBdd<DdType::CUDD> const& elseDd) const {
             return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
         }

src/storage/dd/cudd/InternalCuddBdd.h

@@ -84,7 +84,16 @@ namespace storm {
              * @return The ralational product.
              */
             InternalBdd<DdType::CUDD> relationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables) const;
-            
+
+            /*!
+             * Computes the inverse relational product of the current BDD and the given BDD representing a relation.
+             *
+             * @param relation The relation to use.
+             * @param columnVariables The row variables of the relation represented as individual BDDs.
+             * @return The ralational product.
+             */
+            InternalBdd<DdType::CUDD> inverseRelationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;
+
             /*!
              * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
              * function value to the function values specified by the first DD and all others to the function values

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -1,5 +1,6 @@
 #include "src/storage/dd/sylvan/InternalSylvanBdd.h"
 
+#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
 #include "src/storage/dd/sylvan/InternalSylvanAdd.h"
 #include "src/storage/dd/sylvan/SylvanAddIterator.h"
 
@@ -8,7 +9,6 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
 
-
 #include <iostream>
 
 namespace storm {
@@ -31,6 +31,15 @@ namespace storm {
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables) const {
+            InternalBdd<DdType::Sylvan> cube = ddManager->getBddOne();
+            for (auto const& variable : rowVariables) {
+                cube &= variable;
+            }
+            
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, cube.sylvanBdd));
+        }
+
+        InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
         }
         

src/storage/dd/sylvan/InternalSylvanBdd.h

@@ -74,6 +74,15 @@ namespace storm {
              */
             InternalBdd<DdType::Sylvan> relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables) const;
             
+            /*!
+             * Computes the inverse relational product of the current BDD and the given BDD representing a relation.
+             *
+             * @param relation The relation to use.
+             * @param columnVariables The row variables of the relation represented as individual BDDs.
+             * @return The ralational product.
+             */
+            InternalBdd<DdType::Sylvan> inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
+            
             /*!
              * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
              * function value to the function values specified by the first DD and all others to the function values

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -8,7 +8,10 @@
 namespace storm {
     namespace dd {
         uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0;
-        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
+        
+        // We let the variables start at an odd offset, since some functions provided by sylvan assume that the source/row
+        // variables are at odd levels.
+        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 1;
         
         InternalDdManager<DdType::Sylvan>::InternalDdManager() {
             if (numberOfInstances == 0) {