more work on game abstraction of PRISM programs

Former-commit-id: b5bec829e2

src/storage/dd/CuddAdd.h

@@ -2,6 +2,7 @@
 #define STORM_STORAGE_DD_CUDDADD_H_
 
 #include <boost/optional.hpp>
+#include <boost/functional/hash.hpp>
 #include <map>
 
 #include "src/storage/dd/Add.h"
@@ -35,6 +36,8 @@ namespace storm {
             friend class Bdd<DdType::CUDD>;
             friend class Odd<DdType::CUDD>;
             
+            // Declare the hashing struct for DDs as a friend so it can access the internal DD pointer.
+            friend struct std::hash<storm::dd::Add<storm::dd::DdType::CUDD>>;
             /*!
              * Creates an ADD from the given explicit vector.
              *
@@ -825,4 +828,15 @@ namespace storm {
     }
 }
 
+namespace std {
+    template <> struct hash<storm::dd::Add<storm::dd::DdType::CUDD>>
+    {
+        size_t operator()(storm::dd::Add<storm::dd::DdType::CUDD> const& dd) const {
+            std::size_t seed = 0;
+            boost::hash_combine(seed, dd.getCuddAdd().getNode());
+            return seed;
+        }
+    };
+}
+
 #endif /* STORM_STORAGE_DD_CUDDADD_H_ */

src/storage/dd/CuddBdd.h

@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_DD_CUDDBDD_H_
 #define STORM_STORAGE_DD_CUDDBDD_H_
 
+#include <boost/functional/hash.hpp>
+
 #include "src/storage/dd/Bdd.h"
 #include "src/storage/dd/CuddDd.h"
 #include "src/utility/OsDetection.h"
@@ -21,8 +23,6 @@ namespace storm {
         class BitVector;
     }
     
-    
-    
     namespace dd {
         // Forward-declare some classes.
         template<DdType Type> class DdManager;
@@ -51,6 +51,9 @@ namespace storm {
             friend class Add<DdType::CUDD>;
             friend class Odd<DdType::CUDD>;
             
+            // Declare the hashing struct for DDs as a friend so it can access the internal DD pointer.
+            friend struct std::hash<storm::dd::Bdd<storm::dd::DdType::CUDD>>;
+            
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Bdd() = default;
             Bdd(Bdd<DdType::CUDD> const& other) = default;
@@ -357,4 +360,15 @@ namespace storm {
     }
 }
 
+namespace std {
+    template <> struct hash<storm::dd::Bdd<storm::dd::DdType::CUDD>>
+    {
+        size_t operator()(storm::dd::Bdd<storm::dd::DdType::CUDD> const& dd) const {
+            std::size_t seed = 0;
+            boost::hash_combine(seed, dd.getCuddBdd().getNode());
+            return seed;
+        }
+    };
+}
+
 #endif /* STORM_STORAGE_DD_CUDDBDD_H_ */

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -1,5 +1,7 @@
 #include "src/storage/prism/menu_games/AbstractCommand.h"
 
+#include <boost/iterator/transform_iterator.hpp>
+
 #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h"
 #include "src/storage/prism/menu_games/AbstractionDdInformation.h"
 
@@ -13,7 +15,7 @@ namespace storm {
     namespace prism {
         namespace menu_games {
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.ddManager->getAddZero(), 0)) {
+            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() {
 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@@ -37,7 +39,7 @@ namespace storm {
                     auto const& rightHandSidePredicates = variablePartition.getExpressionsUsingVariables(assignment.getExpression().getVariables());
                     result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end());
                     
-                    // Variables that are being assigned are relevant for the target state.
+                    // Variables that are being assigned are relevant for the successor state.
                     storm::expressions::Variable const& assignedVariable = assignment.getVariable();
                     auto const& leftHandSidePredicates = variablePartition.getExpressionsUsingVariable(assignedVariable);
                     result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end());
@@ -102,6 +104,7 @@ namespace storm {
                 std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first);
                 for (auto const& element : newSourceVariables) {
                     smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second]));
+                    decisionVariables.push_back(element.first);
                 }
                 
                 // Insert the new variables into the record of relevant source variables.
@@ -110,34 +113,109 @@ namespace storm {
                 
                 // Do the same for every update.
                 for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
-                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newTargetVariables = declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
-                    for (auto const& element : newSourceVariables) {
+                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
+                    for (auto const& element : newSuccessorVariables) {
                         smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
+                        decisionVariables.push_back(element.first);
                     }
                     
-                    relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newTargetVariables.begin(), newTargetVariables.end());
+                    relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newSuccessorVariables.begin(), newSuccessorVariables.end());
                     std::sort(relevantPredicatesAndVariables.second[index].begin(), relevantPredicatesAndVariables.second[index].end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
                 }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            std::pair<storm::dd::Add<DdType>, uint_fast64_t> AbstractCommand<DdType, ValueType>::computeDd() {
+            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
+                for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
+                    if (model.getBooleanValue(variableIndexPair.first)) {
+                        result &= ddInformation.predicateBdds[variableIndexPair.second].first;
+                    } else {
+                        result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
+                    }
+                }
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
+                
+                for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
+                    storm::dd::Bdd<DdType> updateBdd = ddInformation.manager->getBddOne();
+
+                    for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) {
+                        if (model.getBooleanValue(variableIndexPair.first)) {
+                            updateBdd &= ddInformation.predicateBdds[variableIndexPair.second].second;
+                        } else {
+                            updateBdd &= !ddInformation.predicateBdds[variableIndexPair.second].second;
+                        }
+                        updateBdd &= ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
+                    }
+                    
+                    // Compute the identities that are missing for this update.
+                    auto firstIt = relevantPredicatesAndVariables.first.begin();
+                    auto firstIte = relevantPredicatesAndVariables.first.end();
+                    auto secondIt = relevantPredicatesAndVariables.second[updateIndex].begin();
+                    auto secondIte = relevantPredicatesAndVariables.second[updateIndex].end();
+                    
+                    for (; firstIt != firstIte; ++firstIt) {
+                        if (secondIt == secondIte || firstIt->second != secondIt->second) {
+                            result &= ddInformation.predicateIdentities[firstIt->second];
+                        } else if (secondIt != secondIte) {
+                            ++secondIt;
+                        }
+                    }
+                    
+                    result |= updateBdd;
+                }
+                
+                return result;
+            }
+                        
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> AbstractCommand<DdType, ValueType>::computeDd() {
                 // First, we check whether there is work to be done by recomputing the relevant predicates and checking
                 // whether they changed.
-                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates;
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();
+
+                // If the DD does not need recomputation, we can return the cached result.
                 bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates);
+                if (!recomputeDd) {
+                    // FIXME: multiply identity of new predicates
+                    return cachedDd;
+                }
                 
-                if (recomputeDd) {
-                    relevantPredicates = std::move(newRelevantPredicates);
+                // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver.
+                addMissingPredicates(newRelevantPredicates);
 
+                // Create a mapping from source state DDs to their distributions.
+                std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
+                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); return true; } );
                 
+                // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
+                // need to encode the nondeterminism.
+                uint_fast64_t maximalNumberOfChoices = 0;
+                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast<uint_fast64_t>(sourceDistributionsPair.second.size()));
+                }
                 
-                    storm::dd::Add<DdType> result;
+                uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices)));
                 
-                    return result;
-                } else {
-                    return cachedDd;
+                // Finally, build overall result.
+                storm::dd::Bdd<DdType> resultBdd = ddInformation.manager->getBddZero();
+                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    uint_fast64_t distributionIndex = 0;
+                    storm::dd::Bdd<DdType> allDistributions = ddInformation.manager->getBddZero();
+                    for (auto const& distribution : sourceDistributionsPair.second) {
+                        allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex);
+                    }
+                    resultBdd |= sourceDistributionsPair.first && allDistributions;
                 }
+                
+                // Cache the result before returning it.
+                cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded);
+                return cachedDd;
             }
             
             template class AbstractCommand<storm::dd::DdType::CUDD, double>;

src/storage/prism/menu_games/AbstractCommand.h

@@ -2,7 +2,9 @@
 #define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_
 
 #include <memory>
+#include <vector>
 #include <set>
+#include <map>
 
 #include "src/storage/prism/menu_games/VariablePartition.h"
 
@@ -40,27 +42,27 @@ namespace storm {
                 /*!
                  * Computes the abstraction of the command wrt. to the current set of predicates.
                  *
-                 * @return The abstraction of the command in the form of an ADD together with the number of DD variables
+                 * @return The abstraction of the command in the form of a BDD together with the number of DD variables
                  * used to encode the choices of player 2.
                  */
-                std::pair<storm::dd::Add<DdType>, uint_fast64_t> computeDd();
+                std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> computeDd();
                 
             private:
                 /*!
-                 * Determines the relevant predicates for source as well as target states wrt. to the given assignments
+                 * Determines the relevant predicates for source as well as successor states wrt. to the given assignments
                  * (that, for example, form an update).
                  *
                  * @param assignments The assignments that are to be considered.
                  * @return A pair whose first component represents the relevant source predicates and whose second
-                 * component represents the relevant target state predicates.
+                 * component represents the relevant successor state predicates.
                  */
                 std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const;
                 
                 /*!
-                 * Determines the relevant predicates for source as well as target states.
+                 * Determines the relevant predicates for source as well as successor states.
                  *
                  * @return A pair whose first component represents the relevant source predicates and whose second
-                 * component represents the relevant target state predicates.
+                 * component represents the relevant successor state predicates.
                  */
                 std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> computeRelevantPredicates() const;
 
@@ -87,6 +89,22 @@ namespace storm {
                  */
                 void addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates);
                 
+                /*!
+                 * Translates the given model to a source state DD.
+                 *
+                 * @param model The model to translate.
+                 * @return The source state encoded as a DD.
+                 */
+                storm::dd::Bdd<DdType> getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const;
+
+                /*!
+                 * Translates the given model to a distribution over successor states.
+                 *
+                 * @param model The model to translate.
+                 * @return The source state encoded as a DD.
+                 */
+                storm::dd::Bdd<DdType> getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const;
+                
                 // An SMT responsible for this abstract command.
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
@@ -102,12 +120,15 @@ namespace storm {
                 // The partition of variables and expressions.
                 VariablePartition variablePartition;
                 
-                // The currently relevant source/target predicates and the corresponding variables.
+                // The currently relevant source/successor predicates and the corresponding variables.
                 std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>> relevantPredicatesAndVariables;
                 
                 // The most recent result of a call to computeDd. If nothing has changed regarding the relevant
                 // predicates, this result may be reused.
-                std::pair<storm::dd::Add<DdType>, uint_fast64_t> cachedDd;
+                std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> cachedDd;
+                
+                // All relevant decision variables over which to perform AllSat.
+                std::vector<storm::expressions::Variable> decisionVariables;
             };
         }
     }

src/storage/prism/menu_games/AbstractModule.cpp

@@ -22,16 +22,16 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Add<DdType> AbstractModule<DdType, ValueType>::computeDd() {
+            storm::dd::Bdd<DdType> AbstractModule<DdType, ValueType>::computeDd() {
                 // First, we retrieve the abstractions of all commands.
-                std::vector<std::pair<storm::dd::Add<DdType>, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts;
-                for (auto const& command : commands) {
+                std::vector<std::pair<storm::dd::Bdd<DdType>, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts;
+                for (auto& command : commands) {
                     commandDdsAndUsedOptionVariableCounts.push_back(command.computeDd());
                 }
                 
                 // Then, we build the module ADD by adding the single command DDs. We need to make sure that all command
                 // DDs use the same amount DD variable encoding the choices of player 2.
-                storm::dd::Add<DdType> result = ddInformation.ddManager->getAddZero();
+                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
                 
                 // TODO
                 

src/storage/prism/menu_games/AbstractModule.h

@@ -36,9 +36,9 @@ namespace storm {
                 /*!
                  * Computes the abstraction of the module wrt. to the current set of predicates.
                  *
-                 * @return The abstraction of the module in the form of an ADD.
+                 * @return The abstraction of the module in the form of a BDD.
                  */
-                storm::dd::Add<DdType> computeDd();
+                storm::dd::Bdd<DdType> computeDd();
                 
             private:
                 // A factory that can be used to create new SMT solvers.

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -1,7 +1,5 @@
 #include "src/storage/prism/menu_games/AbstractProgram.h"
 
-#include <sstream>
-
 #include "src/storage/prism/Program.h"
 
 #include "src/storage/dd/CuddDdManager.h"
@@ -38,23 +36,22 @@ namespace storm {
                 
                 // Create DD variables for all predicates.
                 for (auto const& predicate : expressionInformation.predicates) {
-                    std::stringstream stream;
-                    stream << predicate;
-                    ddInformation.predicateDdVariables.push_back(ddInformation.ddManager->addMetaVariable(stream.str()));
+                    ddInformation.addPredicate(predicate);
                 }
                 
                 // Create DD variable for the command encoding.
-                ddInformation.commandDdVariable = ddInformation.ddManager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
+                ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
                 
                 // Create DD variable for update encoding.
-                ddInformation.updateDdVariable = ddInformation.ddManager->addMetaVariable("update", 0, maximalUpdateCount - 1).first;
+                ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1).first;
                 
                 // Create DD variables encoding the nondeterministic choices of player 2.
                 // NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices.
                 // If for some reason this should not be enough, we could grow this vector dynamically, but odds are
                 // that it's impossible to treat such models in any event.
                 for (uint_fast64_t index = 0; index < 100; ++index) {
-                    ddInformation.optionDdVariables.push_back(ddInformation.ddManager->addMetaVariable("opt" + std::to_string(index)).first);
+                    storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first;
+                    ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getRange(newOptionVar)));
                 }
                 
                 // For each module of the concrete program, we create an abstract counterpart.
@@ -66,7 +63,8 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Add<DdType> AbstractProgram<DdType, ValueType>::computeDd() {
                 // As long as there is only one module, we build its game representation and return it.
-                return modules.front().computeDd();
+                // FIXME: multiply with probabilities for updates.
+                return modules.front().computeDd().toAdd();
             }
             
             // Explicitly instantiate the class.

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -1,17 +1,47 @@
 #include "src/storage/prism/menu_games/AbstractionDdInformation.h"
 
-#include "src/storage/dd/DdManager.h"
+#include <sstream>
+
+#include "src/storage/expressions/Expression.h"
+
+#include "src/storage/dd/CuddDdManager.h"
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddAdd.h"
 
 namespace storm {
     namespace prism {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager) : ddManager(manager) {
+            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager) : manager(manager) {
                 // Intentionally left empty.
             }
             
-            template class AbstractionDdInformation<storm::dd::DdType::CUDD, double>;
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const {
+                storm::dd::Bdd<DdType> result = manager->getBddOne();
+                for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) {
+                    if ((distributionIndex & 1) != 0) {
+                        result &= optionDdVariables[bitIndex].second;
+                    } else {
+                        result &= !optionDdVariables[bitIndex].second;
+                    }
+                    distributionIndex >>= 1;
+                }
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractionDdInformation<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) {
+                std::stringstream stream;
+                stream << predicate;
+                std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = manager->addMetaVariable(stream.str());
+                predicateDdVariables.push_back(newMetaVariable);
+                predicateBdds.emplace_back(manager->getRange(newMetaVariable.first), manager->getRange(newMetaVariable.second));
+                predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd());
+            }
+         
+            template struct AbstractionDdInformation<storm::dd::DdType::CUDD, double>;
             
         }
     }

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -11,6 +11,13 @@ namespace storm {
     namespace dd {
         template <storm::dd::DdType DdType>
         class DdManager;
+
+        template <storm::dd::DdType DdType>
+        class Bdd;
+    }
+    
+    namespace expressions {
+        class Expression;
     }
 
     namespace prism {
@@ -26,12 +33,35 @@ namespace storm {
                  */
                 AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager);
                 
+                /*!
+                 * Encodes the given distribution index by using the given number of variables from the optionDdVariables
+                 * vector.
+                 *
+                 * @param numberOfVariables The number of variables to use.
+                 * @param distributionIndex The distribution index to encode.
+                 * @return The encoded distribution index.
+                 */
+                storm::dd::Bdd<DdType> encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const;
+                
+                /*!
+                 * Adds the given predicate and creates all associated ressources.
+                 *
+                 * @param predicate The predicate to add.
+                 */
+                void addPredicate(storm::expressions::Expression const& predicate);
+                
                 // The manager responsible for the DDs.
-                std::shared_ptr<storm::dd::DdManager<DdType>> ddManager;
+                std::shared_ptr<storm::dd::DdManager<DdType>> manager;
                 
                 // The DD variables corresponding to the predicates.
                 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;
 
+                // The BDDs corresponding to the predicates.
+                std::vector<std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>>> predicateBdds;
+                
+                // The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value).
+                std::vector<storm::dd::Bdd<DdType>> predicateIdentities;
+                
                 // The DD variable encoding the command (i.e., the nondeterministic choices of player 1).
                 storm::expressions::Variable commandDdVariable;
                 
@@ -39,7 +69,7 @@ namespace storm {
                 storm::expressions::Variable updateDdVariable;
                 
                 // The DD variables encoding the nondeterministic choices of player 2.
-                std::vector<storm::expressions::Variable> optionDdVariables;
+                std::vector<std::pair<storm::expressions::Variable, storm::dd::Bdd<DdType>>> optionDdVariables;
             };
             
         }