started refactoring of abstraction

Former-commit-id: 72d9fc9fab

src/abstraction/AbstractionDdInformation.cpp

@@ -1,91 +0,0 @@
-#include "src/abstraction/AbstractionDdInformation.h"
-
-#include <sstream>
-
-#include "src/storage/expressions/ExpressionManager.h"
-#include "src/storage/expressions/Expression.h"
-
-#include "src/storage/dd/DdManager.h"
-#include "src/storage/dd/Bdd.h"
-#include "src/storage/dd/Add.h"
-
-#include "src/utility/macros.h"
-
-namespace storm {
-    namespace abstraction {
-        
-        template <storm::dd::DdType DdType, typename ValueType>
-        AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()), bddVariableIndexToPredicateMap() {
-            for (auto const& predicate : initialPredicates) {
-                this->addPredicate(predicate);
-            }
-        }
-        
-        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) {
-                STORM_LOG_ASSERT(!(optionDdVariables[bitIndex].second.isZero() || optionDdVariables[bitIndex].second.isOne()), "Option variable is corrupted.");
-                if ((distributionIndex & 1) != 0) {
-                    result &= optionDdVariables[bitIndex].second;
-                } else {
-                    result &= !optionDdVariables[bitIndex].second;
-                }
-                distributionIndex >>= 1;
-            }
-            STORM_LOG_ASSERT(!result.isZero(), "Update BDD encoding must not be zero.");
-            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->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
-            predicateIdentities.push_back(manager->getEncoding(newMetaVariable.first, 1).iff(manager->getEncoding(newMetaVariable.second, 1)));
-            allPredicateIdentities &= predicateIdentities.back();
-            sourceVariables.insert(newMetaVariable.first);
-            successorVariables.insert(newMetaVariable.second);
-            expressionToBddMap[predicate] = predicateBdds.back().first;
-            bddVariableIndexToPredicateMap[predicateIdentities.back().getIndex()] = predicate;
-        }
-        
-        template <storm::dd::DdType DdType, typename ValueType>
-        storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::getMissingOptionVariableCube(uint_fast64_t begin, uint_fast64_t end) const {
-            storm::dd::Bdd<DdType> result = manager->getBddOne();
-            
-            for (uint_fast64_t index = begin; index < end; ++index) {
-                result &= optionDdVariables[index].second;
-            }
-            
-            STORM_LOG_ASSERT(!result.isZero(), "Update variable cube must not be zero.");
-            
-            return result;
-        }
-        
-        template <storm::dd::DdType DdType, typename ValueType>
-        std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> AbstractionDdInformation<DdType, ValueType>::declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldRelevantPredicates, std::set<uint_fast64_t> const& newRelevantPredicates) {
-            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> result;
-            
-            auto oldIt = oldRelevantPredicates.begin();
-            auto oldIte = oldRelevantPredicates.end();
-            for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) {
-                // If the new variable does not yet exist as a source variable, we create it now.
-                if (oldIt == oldIte || oldIt->second != *newIt) {
-                    result.push_back(std::make_pair(manager.declareFreshBooleanVariable(), *newIt));
-                } else {
-                    ++oldIt;
-                }
-            }
-            
-            return result;
-        }
-        
-        template struct AbstractionDdInformation<storm::dd::DdType::CUDD, double>;
-        template struct AbstractionDdInformation<storm::dd::DdType::Sylvan, double>;
-        
-    }
-}

src/abstraction/AbstractionDdInformation.h

@@ -1,113 +0,0 @@
-#pragma once
-
-#include <memory>
-#include <vector>
-#include <set>
-#include <map>
-#include <unordered_map>
-
-#include "src/storage/dd/DdType.h"
-#include "src/storage/expressions/Variable.h"
-
-namespace storm {
-    namespace dd {
-        template <storm::dd::DdType DdType>
-        class DdManager;
-        
-        template <storm::dd::DdType DdType>
-        class Bdd;
-    }
-    
-    namespace expressions {
-        class Expression;
-    }
-    
-    namespace abstraction {
-        
-        template <storm::dd::DdType DdType, typename ValueType>
-        struct AbstractionDdInformation {
-        public:
-            /*!
-             * Creates a new DdInformation that uses the given manager.
-             *
-             * @param manager The manager to use.
-             * @param initialPredicates The initially considered predicates.
-             */
-            AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates = std::vector<storm::expressions::Expression>());
-            
-            /*!
-             * 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);
-            
-            /*!
-             * Retrieves the cube of option variables in the range [begin, end) the given indices.
-             *
-             * @param begin The first variable of the range to return.
-             * @param end One past the last variable of the range to return.
-             * @return The cube of variables in the given range.
-             */
-            storm::dd::Bdd<DdType> getMissingOptionVariableCube(uint_fast64_t begin, uint_fast64_t end) const;
-            
-            /*!
-             * Examines the old and new relevant predicates and declares decision variables for the missing relevant
-             * predicates.
-             *
-             * @param manager The manager in which to declare the decision variable.
-             * @param oldRelevantPredicates The previously relevant predicates.
-             * @param newRelevantPredicates The new relevant predicates.
-             * @return Pairs of decision variables and their index for the missing predicates.
-             */
-            static std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldRelevantPredicates, std::set<uint_fast64_t> const& newRelevantPredicates);
-            
-            // The manager responsible for the DDs.
-            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 set of all source variables.
-            std::set<storm::expressions::Variable> sourceVariables;
-            
-            // The set of all source variables.
-            std::set<storm::expressions::Variable> successorVariables;
-            
-            // 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;
-            
-            // A BDD that represents the identity of all predicate variables.
-            storm::dd::Bdd<DdType> allPredicateIdentities;
-            
-            // The DD variable encoding the command (i.e., the nondeterministic choices of player 1).
-            storm::expressions::Variable commandDdVariable;
-            
-            // The DD variable encoding the update IDs for all actions.
-            storm::expressions::Variable updateDdVariable;
-            
-            // The DD variables encoding the nondeterministic choices of player 2.
-            std::vector<std::pair<storm::expressions::Variable, storm::dd::Bdd<DdType>>> optionDdVariables;
-            
-            // A mapping from the predicates to the BDDs.
-            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> expressionToBddMap;
-            
-            // A mapping from the indices of the BDD variables to the predicates.
-            std::unordered_map<uint_fast64_t, storm::expressions::Expression> bddVariableIndexToPredicateMap;
-        };
-        
-    }
-}

src/abstraction/AbstractionExpressionInformation.cpp

@@ -1,64 +0,0 @@
-#include "src/abstraction/AbstractionExpressionInformation.h"
-
-#include "src/storage/expressions/ExpressionManager.h"
-#include "src/storage/expressions/Expression.h"
-
-namespace storm {
-    namespace abstraction {
-        
-        AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression> const& predicates, std::set<storm::expressions::Variable> const& variables, std::vector<storm::expressions::Expression> const& rangeExpressions) : manager(manager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) {
-            // Intentionally left empty.
-        }
-        
-        void AbstractionExpressionInformation::addPredicate(storm::expressions::Expression const& predicate) {
-            predicates.push_back(predicate);
-        }
-        
-        void AbstractionExpressionInformation::addPredicates(std::vector<storm::expressions::Expression> const& predicates) {
-            for (auto const& predicate : predicates) {
-                this->addPredicate(predicate);
-            }
-        }
-        
-        storm::expressions::ExpressionManager& AbstractionExpressionInformation::getManager() {
-            return manager;
-        }
-        
-        storm::expressions::ExpressionManager const& AbstractionExpressionInformation::getManager() const {
-            return manager;
-        }
-        
-        std::vector<storm::expressions::Expression>& AbstractionExpressionInformation::getPredicates() {
-            return predicates;
-        }
-        
-        std::vector<storm::expressions::Expression> const& AbstractionExpressionInformation::getPredicates() const {
-            return predicates;
-        }
-        
-        storm::expressions::Expression const& AbstractionExpressionInformation::getPredicateByIndex(uint_fast64_t index) const {
-            return predicates[index];
-        }
-        
-        std::size_t AbstractionExpressionInformation::getNumberOfPredicates() const {
-            return predicates.size();
-        }
-        
-        std::set<storm::expressions::Variable>& AbstractionExpressionInformation::getVariables() {
-            return variables;
-        }
-        
-        std::set<storm::expressions::Variable> const& AbstractionExpressionInformation::getVariables() const {
-            return variables;
-        }
-        
-        std::vector<storm::expressions::Expression>& AbstractionExpressionInformation::getRangeExpressions() {
-            return rangeExpressions;
-        }
-        
-        std::vector<storm::expressions::Expression> const& AbstractionExpressionInformation::getRangeExpressions() const {
-            return rangeExpressions;
-        }
-        
-    }
-}

src/abstraction/AbstractionExpressionInformation.h

@@ -1,126 +0,0 @@
-#pragma once
-
-#include <vector>
-#include <set>
-
-namespace storm {
-    namespace expressions {
-        class ExpressionManager;
-        class Expression;
-        class Variable;
-    }
-    
-    namespace abstraction {
-        
-        struct AbstractionExpressionInformation {
-        public:
-            /*!
-             * Creates an expression information object with the given expression manager.
-             *
-             * @param manager The expression manager to use.
-             * @param predicates The initial set of predicates.
-             * @param variables The variables.
-             * @param rangeExpressions A set of expressions that enforce the variable bounds.
-             */
-            AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression> const& predicates = std::vector<storm::expressions::Expression>(), std::set<storm::expressions::Variable> const& variables = std::set<storm::expressions::Variable>(), std::vector<storm::expressions::Expression> const& rangeExpressions = std::vector<storm::expressions::Expression>());
-            
-            /*!
-             * Adds the given predicate.
-             *
-             * @param predicate The predicate to add.
-             */
-            void addPredicate(storm::expressions::Expression const& predicate);
-            
-            /*!
-             * Adds the given predicates.
-             *
-             * @param predicates The predicates to add.
-             */
-            void addPredicates(std::vector<storm::expressions::Expression> const& predicates);
-            
-            /*!
-             * Retrieves the expression manager.
-             *
-             * @return The manager.
-             */
-            storm::expressions::ExpressionManager& getManager();
-            
-            /*!
-             * Retrieves the expression manager.
-             *
-             * @return The manager.
-             */
-            storm::expressions::ExpressionManager const& getManager() const;
-            
-            /*!
-             * Retrieves all currently known predicates.
-             *
-             * @return The list of known predicates.
-             */
-            std::vector<storm::expressions::Expression>& getPredicates();
-            
-            /*!
-             * Retrieves all currently known predicates.
-             *
-             * @return The list of known predicates.
-             */
-            std::vector<storm::expressions::Expression> const& getPredicates() const;
-            
-            /*!
-             * Retrieves the predicate with the given index.
-             *
-             * @param index The index of the predicate.
-             */
-            storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const;
-            
-            /*!
-             * Retrieves the number of predicates.
-             *
-             * @return The number of predicates.
-             */
-            std::size_t getNumberOfPredicates() const;
-            
-            /*!
-             * Retrieves all currently known variables.
-             *
-             * @return The set of known variables.
-             */
-            std::set<storm::expressions::Variable>& getVariables();
-            
-            /*!
-             * Retrieves all currently known variables.
-             *
-             * @return The set of known variables.
-             */
-            std::set<storm::expressions::Variable> const& getVariables() const;
-            
-            /*!
-             * Retrieves a list of expressions that ensure the ranges of the variables.
-             *
-             * @return The range expressions.
-             */
-            std::vector<storm::expressions::Expression>& getRangeExpressions();
-            
-            /*!
-             * Retrieves a list of expressions that ensure the ranges of the variables.
-             *
-             * @return The range expressions.
-             */
-            std::vector<storm::expressions::Expression> const& getRangeExpressions() const;
-            
-        private:
-            // The manager responsible for the expressions of the program and the SMT solvers.
-            storm::expressions::ExpressionManager& manager;
-            
-            // The current set of predicates used in the abstraction.
-            std::vector<storm::expressions::Expression> predicates;
-            
-            // The set of all variables.
-            std::set<storm::expressions::Variable> variables;
-            
-            // The expression characterizing the legal ranges of all variables.
-            std::vector<storm::expressions::Expression> rangeExpressions;
-        };
-        
-    }
-}

src/abstraction/AbstractionInformation.cpp

@@ -1,77 +1,303 @@
 #include "src/abstraction/AbstractionInformation.h"
 
+#include "src/storage/dd/DdManager.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidOperationException.h"
+
 namespace storm {
     namespace abstraction {
 
-        template<storm::dd::DdType DdType, typename ValueType>
-        AbstractionInformation<DdType, ValueType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager) : expressionManager(expressionManager) {
+        template<storm::dd::DdType DdType>
+        AbstractionInformation<DdType>::AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager) : expressionManager(expressionManager), ddManager(ddManager) {
             // Intentionally left empty.
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        void AbstractionInformation<DdType, ValueType>::addVariable(storm::expressions::Variable const& variable) {
+        template<storm::dd::DdType DdType>
+        void AbstractionInformation<DdType>::addExpressionVariable(storm::expressions::Variable const& variable) {
             variables.insert(variable);
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        void AbstractionInformation<DdType, ValueType>::addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) {
-            addVariable(variable);
+        template<storm::dd::DdType DdType>
+        void AbstractionInformation<DdType>::addExpressionVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint) {
+            addExpressionVariable(variable);
             addConstraint(constraint);
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        void AbstractionInformation<DdType, ValueType>::addConstraint(storm::expressions::Expression const& constraint) {
+        template<storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getExpressionVariables() const {
+            return variables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        void AbstractionInformation<DdType>::addConstraint(storm::expressions::Expression const& constraint) {
             constraints.push_back(constraint);
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        void AbstractionInformation<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) {
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::addPredicate(storm::expressions::Expression const& predicate) {
+            std::size_t predicateIndex = predicates.size();
+            predicateToIndexMap[predicate] = predicateIndex;
+            
+            // Add the new predicate to the list of known predicates.
             predicates.push_back(predicate);
+            
+            // Add DD variables for the new predicate.
+            std::stringstream stream;
+            stream << predicate;
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = ddManager->addMetaVariable(stream.str());
+            
+            predicateDdVariables.push_back(newMetaVariable);
+            predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1));
+            predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1)));
+            allPredicateIdentities &= predicateIdentities.back();
+            sourceVariables.insert(newMetaVariable.first);
+            successorVariables.insert(newMetaVariable.second);
+            ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex;
+            return predicateIndex;
         }
 
-        template<storm::dd::DdType DdType, typename ValueType>
-        void AbstractionInformation<DdType, ValueType>::addPredicates(std::vector<storm::expressions::Expression> const& predicates) {
+        template<storm::dd::DdType DdType>
+        std::vector<uint_fast64_t> AbstractionInformation<DdType>::addPredicates(std::vector<storm::expressions::Expression> const& predicates) {
+            std::vector<uint_fast64_t> predicateIndices;
             for (auto const& predicate : predicates) {
-                this->addPredicate(predicate);
+                predicateIndices.push_back(this->addPredicate(predicate));
+            }
+            return predicateIndices;
         }
+        
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType>::getConstraints() const {
+            return constraints;
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        storm::expressions::ExpressionManager& AbstractionInformation<DdType, ValueType>::getExpressionManager() {
-            return expressionManager;
+        template<storm::dd::DdType DdType>
+        storm::expressions::ExpressionManager& AbstractionInformation<DdType>::getExpressionManager() {
+            return expressionManager.get();
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        storm::expressions::ExpressionManager const& AbstractionInformation<DdType, ValueType>::getExpressionManager() const {
-            return expressionManager;
+        template<storm::dd::DdType DdType>
+        storm::expressions::ExpressionManager const& AbstractionInformation<DdType>::getExpressionManager() const {
+            return expressionManager.get();
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType, ValueType>::getPredicates() const {
+        template<storm::dd::DdType DdType>
+        storm::dd::DdManager<DdType>& AbstractionInformation<DdType>::getDdManager() {
+            return *ddManager;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::DdManager<DdType> const& AbstractionInformation<DdType>::getDdManager() const {
+            return *ddManager;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::shared_ptr<storm::dd::DdManager<DdType>> AbstractionInformation<DdType>::getDdManagerAsSharedPointer() {
+            return ddManager;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::shared_ptr<storm::dd::DdManager<DdType> const> AbstractionInformation<DdType>::getDdManagerAsSharedPointer() const {
+            return ddManager;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType>::getPredicates() const {
             return predicates;
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        storm::expressions::Expression const& AbstractionInformation<DdType, ValueType>::getPredicateByIndex(uint_fast64_t index) const {
+        template<storm::dd::DdType DdType>
+        storm::expressions::Expression const& AbstractionInformation<DdType>::getPredicateByIndex(uint_fast64_t index) const {
             return predicates[index];
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        std::size_t AbstractionInformation<DdType, ValueType>::getNumberOfPredicates() const {
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getPredicateSourceVariable(storm::expressions::Expression const& predicate) const {
+            auto indexIt = predicateToIndexMap.find(predicate);
+            STORM_LOG_THROW(indexIt != predicateToIndexMap.end(), storm::exceptions::InvalidOperationException, "Cannot retrieve BDD for unknown predicate.");
+            return predicateBdds[indexIt->second].first;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::size_t AbstractionInformation<DdType>::getNumberOfPredicates() const {
             return predicates.size();
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType, ValueType>::getVariables() const {
+        template<storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getVariables() const {
             return variables;
         }
         
-        template<storm::dd::DdType DdType, typename ValueType>
-        std::vector<storm::expressions::Expression> const& AbstractionInformation<DdType, ValueType>::getConstraints() const {
-            return constraints;
+        template<storm::dd::DdType DdType>
+        void AbstractionInformation<DdType>::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount) {
+            STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && probabilisticBranchingVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created.");
+            
+            for (uint64_t index = 0; index < player1VariableCount; ++index) {
+                storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1" + std::to_string(index)).first;
+                player1Variables.push_back(newVariable);
+                player1VariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
+            }
+            STORM_LOG_DEBUG("Created " << player1VariableCount << " player 1 variables.");
+
+            for (uint64_t index = 0; index < player2VariableCount; ++index) {
+                storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2" + std::to_string(index)).first;
+                player2Variables.push_back(newVariable);
+                player2VariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
+            }
+            STORM_LOG_DEBUG("Created " << player2VariableCount << " player 2 variables.");
+
+            for (uint64_t index = 0; index < probabilisticBranchingVariableCount; ++index) {
+                storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb" + std::to_string(index)).first;
+                probabilisticBranchingVariables.push_back(newVariable);
+                probabilisticBranchingVariableBdds.push_back(ddManager->getEncoding(newVariable, 1));
+            }
+            STORM_LOG_DEBUG("Created " << probabilisticBranchingVariableCount << " probabilistic branching variables.");
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
+            return encodeChoice(index, numberOfVariables, player1VariableBdds);
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
+            return encodeChoice(index, numberOfVariables, player2VariableBdds);
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
+            return encodeChoice(index, numberOfVariables, probabilisticBranchingVariableBdds);
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const {
+            storm::dd::Bdd<DdType> result = ddManager->getBddOne();
+            for (uint_fast64_t index = offset; index < numberOfVariables - offset; ++index) {
+                result &= player2VariableBdds[index];
+            }
+            STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero.");
+            return result;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getPlayer1Variables() const {
+            return player1Variables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getPlayer2Variables() const {
+            return player2Variables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getProbabilisticBranchingVariables() const {
+            return probabilisticBranchingVariables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getSourceVariables() const {
+            return sourceVariables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getSuccessorVariables() const {
+            return successorVariables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllPredicateIdentities() const {
+            return allPredicateIdentities;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::size_t AbstractionInformation<DdType>::getPlayer1VariableCount() const {
+            return player1Variables.size();
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::size_t AbstractionInformation<DdType>::getPlayer2VariableCount() const {
+            return player2Variables.size();
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::size_t AbstractionInformation<DdType>::getProbabilisticBranchingVariableCount() const {
+            return probabilisticBranchingVariables.size();
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> AbstractionInformation<DdType>::getPredicateToBddMap() const {
+            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> result;
+            
+            for (uint_fast64_t index = 0; index < predicates.size(); ++index) {
+                result[predicates[index]] = predicateBdds[index].first;
+            }
+            
+            return result;
+        }
+        
+        template<storm::dd::DdType DdType>
+        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& AbstractionInformation<DdType>::getSourceSuccessorVariablePairs() const {
+            return predicateDdVariables;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::encodePredicateAsSource(uint_fast64_t predicateIndex) const {
+            return predicateBdds[predicateIndex].first;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::encodePredicateAsSuccessor(uint_fast64_t predicateIndex) const {
+            return predicateBdds[predicateIndex].second;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getPredicateIdentity(uint_fast64_t predicateIndex) const {
+            return predicateIdentities[predicateIndex];
+        }
+
+        template<storm::dd::DdType DdType>
+        storm::expressions::Expression const& AbstractionInformation<DdType>::getPredicateForDdVariableIndex(uint_fast64_t ddVariableIndex) const {
+            auto indexIt = ddVariableIndexToPredicateIndexMap.find(ddVariableIndex);
+            STORM_LOG_THROW(indexIt != ddVariableIndexToPredicateIndexMap.end(), storm::exceptions::InvalidOperationException, "Unknown DD variable index.");
+            return predicates[indexIt->second];
+        }
+        
+        template <storm::dd::DdType DdType>
+        std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> AbstractionInformation<DdType>::declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldPredicates, std::set<uint_fast64_t> const& newPredicates) const {
+            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> result;
+            
+            auto oldIt = oldPredicates.begin();
+            auto oldIte = oldPredicates.end();
+            auto newIt = newPredicates.begin();
+            auto newIte = newPredicates.end();
+            
+            for (; newIt != newIte; ++newIt) {
+                if (oldIt == oldIte || oldIt->second != *newIt) {
+                    result.push_back(std::make_pair(expressionManager.get().declareFreshBooleanVariable(), *newIt));
+                } else {
+                    ++oldIt;
+                }
+            }
+            
+            return result;
+        }
+        
+        template<storm::dd::DdType DdType>
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const {
+            storm::dd::Bdd<DdType> result = ddManager->getBddOne();
+            for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) {
+                if ((index & 1) != 0) {
+                    result &= variables[bitIndex];
+                } else {
+                    result &= !variables[bitIndex];
+                }
+                index >>= 1;
+            }
+            STORM_LOG_ASSERT(!result.isZero(), "BDD encoding must not be zero.");
+            return result;
         }
         
-        template class AbstractionInformation<storm::dd::DdType::CUDD, double>;
-        template class AbstractionInformation<storm::dd::DdType::Sylvan, double>;
+        template class AbstractionInformation<storm::dd::DdType::CUDD>;
+        template class AbstractionInformation<storm::dd::DdType::Sylvan>;
     }
 }

src/abstraction/AbstractionInformation.h

@@ -5,6 +5,8 @@
 
 #include "src/storage/dd/DdType.h"
 
+#include "src/storage/dd/Bdd.h"
+
 namespace storm {
     namespace expressions {
         class ExpressionManager;
@@ -12,9 +14,14 @@ namespace storm {
         class Variable;
     }
     
+    namespace dd {
+        template <storm::dd::DdType DdType>
+        class DdManager;
+    }
+    
     namespace abstraction {
         
-        template<storm::dd::DdType DdType, typename ValueType>
+        template<storm::dd::DdType DdType>
         class AbstractionInformation {
         public:
             /*!
@@ -22,14 +29,21 @@ namespace storm {
              *
              * @param expressionManager The manager responsible for all variables and expressions during the abstraction process.
              */
-            AbstractionInformation(storm::expressions::ExpressionManager& expressionManager);
+            AbstractionInformation(storm::expressions::ExpressionManager& expressionManager, std::shared_ptr<storm::dd::DdManager<DdType>> ddManager = std::make_shared<storm::dd::DdManager<DdType>>());
 
             /*!
              * Adds the given variable.
              *
              * @param variable The variable to add.
              */
-            void addVariable(storm::expressions::Variable const& variable);
+            void addExpressionVariable(storm::expressions::Variable const& variable);
+
+            /*!
+             * Retrieves all known variables that may be used in predicates.
+             *
+             * @return All known variables.
+             */
+            std::set<storm::expressions::Variable> getExpressionVariables() const;
             
             /*!
              * Adds the given variable whose range is restricted.
@@ -37,7 +51,7 @@ namespace storm {
              * @param variable The variable to add.
              * @param constraint An expression characterizing the legal values of the variable.
              */
-            void addVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint);
+            void addExpressionVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint);
 
             /*!
              * Adds an expression that constrains the legal variable values.
@@ -46,19 +60,28 @@ namespace storm {
              */
             void addConstraint(storm::expressions::Expression const& constraint);
             
+            /*!
+             * Retrieves a list of expressions that constrain the valid variable values.
+             *
+             * @return The constraint expressions.
+             */
+            std::vector<storm::expressions::Expression> const& getConstraints() const;
+            
             /*!
              * Adds the given predicate.
              *
              * @param predicate The predicate to add.
+             * @return The index of the newly added predicate in the global list of predicates.
              */
-            void addPredicate(storm::expressions::Expression const& predicate);
+            uint_fast64_t addPredicate(storm::expressions::Expression const& predicate);
             
             /*!
              * Adds the given predicates.
              *
              * @param predicates The predicates to add.
+             * @return A list of indices corresponding to the new predicates.
              */
-            void addPredicates(std::vector<storm::expressions::Expression> const& predicates);
+            std::vector<uint_fast64_t> addPredicates(std::vector<storm::expressions::Expression> const& predicates);
             
             /*!
              * Retrieves the expression manager.
@@ -74,6 +97,34 @@ namespace storm {
              */
             storm::expressions::ExpressionManager const& getExpressionManager() const;
             
+            /*!
+             * Retrieves the DD manager.
+             *
+             * @return The manager.
+             */
+            storm::dd::DdManager<DdType>& getDdManager();
+            
+            /*!
+             * Retrieves the DD manager.
+             *
+             * @return The manager.
+             */
+            storm::dd::DdManager<DdType> const& getDdManager() const;
+            
+            /*!
+             * Retrieves the shared pointer to the DD manager.
+             *
+             * @return The shared pointer to the DD manager.
+             */
+            std::shared_ptr<storm::dd::DdManager<DdType>> getDdManagerAsSharedPointer();
+
+            /*!
+             * Retrieves the shared pointer to the DD manager.
+             *
+             * @return The shared pointer to the DD manager.
+             */
+            std::shared_ptr<storm::dd::DdManager<DdType> const> getDdManagerAsSharedPointer() const;
+            
             /*!
              * Retrieves all currently known predicates.
              *
@@ -88,6 +139,14 @@ namespace storm {
              */
             storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const;
             
+            /*!
+             * Retrieves the source variable associated with the given predicate. Note that the given predicate must be
+             * known to this abstraction information.
+             *
+             * @param predicate The predicate for which to retrieve the source variable.
+             */
+            storm::dd::Bdd<DdType> getPredicateSourceVariable(storm::expressions::Expression const& predicate) const;
+            
             /*!
              * Retrieves the number of predicates.
              *
@@ -103,17 +162,187 @@ namespace storm {
             std::set<storm::expressions::Variable> const& getVariables() const;
             
             /*!
-             * Retrieves a list of expressions that constrain the valid variable values.
+             * Creates the given number of variables used to encode the choices of player 1/2 and probabilistic branching.
              *
-             * @return The constraint expressions.
+             * @param player1VariableCount The number of variables to use for encoding player 1 choices.
+             * @param player2VariableCount The number of variables to use for encoding player 2 choices.
+             * @param probabilisticBranchingVariableCount The number of variables to use for encoding probabilistic branching.
              */
-            std::vector<storm::expressions::Expression> const& getConstraints() const;
+            void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount);
+            
+            /*!
+             * Encodes the given index using the indicated player 1 variables.
+             *
+             * @param index The index to encode.
+             * @param numberOfVariables The number of variables to use for encoding the index.
+             * @return The index encoded as a BDD.
+             */
+            storm::dd::Bdd<DdType> encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const;
+            
+            /*!
+             * Encodes the given index using the indicated player 2 variables.
+             *
+             * @param index The index to encode.
+             * @param numberOfVariables The number of variables to use for encoding the index.
+             * @return The index encoded as a BDD.
+             */
+            storm::dd::Bdd<DdType> encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const;
+
+            /*!
+             * Encodes the given index using the indicated probabilistic branching variables.
+             *
+             * @param index The index to encode.
+             * @param numberOfVariables The number of variables to use for encoding the index.
+             * @return The index encoded as a BDD.
+             */
+            storm::dd::Bdd<DdType> encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const;
+            
+            /*!
+             * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables).
+             *
+             * @param numberOfVariables The number of variables to use in total. The number of variables in the returned
+             * cube is the number of variables minus the offset.
+             * @param offset The first variable of the range to return.
+             * @return The cube of variables starting from the offset until the given number of variables is reached.
+             */
+            storm::dd::Bdd<DdType> getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const;
+            
+            /*!
+             * Retrieves the meta variables associated with the player 1 choices.
+             *
+             * @return The meta variables associated with the player 1 choices.
+             */
+            std::vector<storm::expressions::Variable> const& getPlayer1Variables() const;
+            
+            /*!
+             * Retrieves the number of player 1 variables.
+             *
+             * @return The number of player 1 variables.
+             */
+            std::size_t getPlayer1VariableCount() const;
+
+            /*!
+             * Retrieves the meta variables associated with the player 2 choices.
+             *
+             * @return The meta variables associated with the player 2 choices.
+             */
+            std::vector<storm::expressions::Variable> const& getPlayer2Variables() const;
+
+            /*!
+             * Retrieves the number of player 2 variables.
+             *
+             * @return The number of player 2 variables.
+             */
+            std::size_t getPlayer2VariableCount() const;
+
+            /*!
+             * Retrieves the meta variables associated with the probabilistic branching.
+             *
+             * @return The meta variables associated with the probabilistic branching.
+             */
+            std::vector<storm::expressions::Variable> const& getProbabilisticBranchingVariables() const;
+
+            /*!
+             * Retrieves the number of probabilistic branching variables.
+             *
+             * @return The number of probabilistic branching variables.
+             */
+            std::size_t getProbabilisticBranchingVariableCount() const;
+            
+            /*!
+             * Retrieves the set of source meta variables.
+             *
+             * @return All source meta variables.
+             */
+            std::set<storm::expressions::Variable> const& getSourceVariables() const;
+
+            /*!
+             * Retrieves the set of successor meta variables.
+             *
+             * @return All successor meta variables.
+             */
+            std::set<storm::expressions::Variable> const& getSuccessorVariables() const;
+
+            /*!
+             * Retrieves a BDD representing the identities of all predicates.
+             *
+             * @return All predicate identities.
+             */
+            storm::dd::Bdd<DdType> const& getAllPredicateIdentities() const;
+            
+            /*!
+             * Retrieves a mapping of the known predicates to the BDDs that represent the corresponding states.
+             *
+             * @return A mapping from predicates to their representing BDDs.
+             */
+            std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> getPredicateToBddMap() const;
+            
+            /*!
+             * Retrieves the meta variables pairs for all predicates.
+             *
+             * @return The meta variable pairs for all predicates.
+             */
+            std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getSourceSuccessorVariablePairs() const;
+            
+            /*!
+             * Retrieves the BDD for the predicate with the given index over the source variables.
+             *
+             * @param predicateIndex The index of the predicate.
+             * @return The encoding the predicate over the source variables.
+             */
+            storm::dd::Bdd<DdType> const& encodePredicateAsSource(uint_fast64_t predicateIndex) const;
+
+            /*!
+             * Retrieves the BDD for the predicate with the given index over the successor variables.
+             *
+             * @param predicateIndex The index of the predicate.
+             * @return The encoding the predicate over the successor variables.
+             */
+            storm::dd::Bdd<DdType> const& encodePredicateAsSuccessor(uint_fast64_t predicateIndex) const;
+
+            /*!
+             * Retrieves a BDD representing the identity for the predicate with the given index.
+             *
+             * @param predicateIndex The index of the predicate.
+             * @return The identity for the predicate.
+             */
+            storm::dd::Bdd<DdType> const& getPredicateIdentity(uint_fast64_t predicateIndex) const;
+            
+            /*!
+             * Retrieves the predicate associated with the given DD variable index.
+             *
+             * @param ddVariableIndex The DD variable index for which to retrieve the predicate.
+             * @return The predicate associated with the given DD variable index.
+             */
+            storm::expressions::Expression const& getPredicateForDdVariableIndex(uint_fast64_t ddVariableIndex) const;
+            
+            /*!
+             * Declares new variables for the missing predicates.
+             *
+             * @param oldPredicates The old predicates.
+             * @param newPredicates The new predicates.
+             * @return A list of the missing variables together with the predicate index they represent.
+             */
+            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldPredicates, std::set<uint_fast64_t> const& newPredicates) const;
             
         private:
+            /*!
+             * Encodes the given index with the given number of variables from the given variables.
+             *
+             * @param index The index to encode.
+             * @param numberOfVariables The total number of variables to use.
+             * @param variables The BDDs of the variables to use to encode the index.
+             */
+            storm::dd::Bdd<DdType> encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const;
+                        
             // The expression related data.
             
             /// The manager responsible for the expressions of the program and the SMT solvers.
-            storm::expressions::ExpressionManager& expressionManager;
+            std::reference_wrapper<storm::expressions::ExpressionManager> expressionManager;
+            
+            /// A mapping from predicates to their indices in the predicate list.
+            // FIXME: Does this properly store the expressions? What about equality checking?
+            std::unordered_map<storm::expressions::Expression, uint64_t> predicateToIndexMap;
             
             /// The current set of predicates used in the abstraction.
             std::vector<storm::expressions::Expression> predicates;
@@ -123,6 +352,50 @@ namespace storm {
             
             /// The expressions characterizing legal variable values.
             std::vector<storm::expressions::Expression> constraints;
+            
+            // The DD-related data.
+            
+            /// The manager responsible for the DDs.
+            std::shared_ptr<storm::dd::DdManager<DdType>> ddManager;
+            
+            /// The DD variables corresponding to the predicates.
+            std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;
+            
+            /// The set of all source variables.
+            std::set<storm::expressions::Variable> sourceVariables;
+            
+            /// The set of all source variables.
+            std::set<storm::expressions::Variable> successorVariables;
+            
+            /// 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;
+            
+            /// A BDD that represents the identity of all predicate variables.
+            storm::dd::Bdd<DdType> allPredicateIdentities;
+            
+            /// A mapping from DD variable indices to the predicate index they represent.
+            std::unordered_map<uint_fast64_t, uint_fast64_t> ddVariableIndexToPredicateIndexMap;
+            
+            /// Variables that encode the choices of player 1.
+            std::vector<storm::expressions::Variable> player1Variables;
+            
+            /// The BDDs associated with the meta variables of player 1.
+            std::vector<storm::dd::Bdd<DdType>> player1VariableBdds;
+
+            /// Variables that encode the choices of player 2.
+            std::vector<storm::expressions::Variable> player2Variables;
+            
+            /// The BDDs associated with the meta variables of player 2.
+            std::vector<storm::dd::Bdd<DdType>> player2VariableBdds;
+            
+            /// Variables that can be used to encode the probabilistic branching.
+            std::vector<storm::expressions::Variable> probabilisticBranchingVariables;
+            
+            /// The BDDs associated with the meta variables encoding the probabilistic branching.
+            std::vector<storm::dd::Bdd<DdType>> probabilisticBranchingVariableBdds;
         };
         
     }

src/abstraction/MenuGame.cpp

@@ -24,8 +24,8 @@ namespace storm {
                                             std::set<storm::expressions::Variable> const& player1Variables,
                                             std::set<storm::expressions::Variable> const& player2Variables,
                                             std::set<storm::expressions::Variable> const& allNondeterminismVariables,
-                                            storm::expressions::Variable const& updateVariable,
-                                            std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
+                                            std::set<storm::expressions::Variable> const& probabilisticBranchingVariables,
+                                            std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
             // Intentionally left empty.
         }
         

src/abstraction/MenuGame.h

@@ -37,7 +37,7 @@ namespace storm {
                  * @param player1Variables The meta variables used to encode the nondeterministic choices of player 1.
                  * @param player2Variables The meta variables used to encode the nondeterministic choices of player 2.
                  * @param allNondeterminismVariables The meta variables used to encode the nondeterminism in the model.
-                 * @param updateVariable The variable used to encode the different updates of the probabilistic program.
+                 * @param probabilisticBranchingVariables The variables used to encode probabilistic branching.
                  * @param expressionToBddMap A mapping from expressions (used) in the abstraction to the BDDs encoding
                  * them.
                  */
@@ -53,7 +53,7 @@ namespace storm {
                          std::set<storm::expressions::Variable> const& player1Variables,
                          std::set<storm::expressions::Variable> const& player2Variables,
                          std::set<storm::expressions::Variable> const& allNondeterminismVariables,
-                         storm::expressions::Variable const& updateVariable,
+                         std::set<storm::expressions::Variable> const& probabilisticBranchingVariables,
                          std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap);
                 
                 virtual storm::dd::Bdd<Type> getStates(std::string const& label) const override;
@@ -87,8 +87,8 @@ namespace storm {
                 virtual bool hasLabel(std::string const& label) const override;
                 
             private:
-                // The meta variable used to encode the updates.
-                storm::expressions::Variable updateVariable;
+                // The meta variables used to probabilistic branching.
+                std::set<storm::expressions::Variable> probabilisticBranchingVariables;
                 
                 // A mapping from expressions that were used in the abstraction process to the the BDDs representing them.
                 std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> expressionToBddMap;

src/abstraction/StateSetAbstractor.cpp

@@ -1,7 +1,6 @@
 #include "src/abstraction/StateSetAbstractor.h"
 
-#include "src/abstraction/AbstractionExpressionInformation.h"
-#include "src/abstraction/AbstractionDdInformation.h"
+#include "src/abstraction/AbstractionInformation.h"
 
 #include "src/storage/dd/DdManager.h"
 
@@ -12,11 +11,16 @@ namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType DdType, typename ValueType>
-        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation& globalExpressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(globalExpressionInformation.getManager())), globalExpressionInformation(globalExpressionInformation), ddInformation(ddInformation), localExpressionInformation(globalExpressionInformation.getVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) {
+        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation) : smtSolver(nullptr), abstractionInformation(abstractionInformation), localExpressionInformation(), relevantPredicatesAndVariables(), concretePredicateVariables(), decisionVariables(), needsRecomputation(false), cachedBdd(), constraint() {
+            // Intentionally left empty.
+        }
+        
+        template <storm::dd::DdType DdType, typename ValueType>
+        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation.getExpressionVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) {
             
-            // Assert all range expressions to enforce legal variable values.
-            for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) {
-                smtSolver->add(rangeExpression);
+            // Assert all constraints to enforce legal variable values.
+            for (auto const& constraint : abstractionInformation.getConstraints()) {
+                smtSolver->add(constraint);
             }
             
             // Assert all state predicates.
@@ -30,8 +34,8 @@ namespace storm {
             }
             
             // Refine the command based on all initial predicates.
-            std::vector<uint_fast64_t> allPredicateIndices(globalExpressionInformation.getPredicates().size());
-            for (auto index = 0; index < globalExpressionInformation.getPredicates().size(); ++index) {
+            std::vector<uint_fast64_t> allPredicateIndices(abstractionInformation.getNumberOfPredicates());
+            for (auto index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
                 allPredicateIndices[index] = index;
             }
             this->refine(allPredicateIndices);
@@ -39,10 +43,10 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         void StateSetAbstractor<DdType, ValueType>::addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices) {
-            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables, newRelevantPredicateIndices);
+            std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables, newRelevantPredicateIndices);
             
             for (auto const& element : newPredicateVariables) {
-                smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicates()[element.second]));
+                smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
                 decisionVariables.push_back(element.first);
             }
             
@@ -54,7 +58,7 @@ namespace storm {
         void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) {
             // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
             for (auto const& predicateIndex : newPredicates) {
-                localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex);
+                localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
             }
             needsRecomputation = true;
         }
@@ -71,12 +75,12 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
             STORM_LOG_TRACE("Building source state BDD.");
-            storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
+            storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
             for (auto const& variableIndexPair : relevantPredicatesAndVariables) {
                 if (model.getBooleanValue(variableIndexPair.first)) {
-                    result &= ddInformation.predicateBdds[variableIndexPair.second].first;
+                    result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                 } else {
-                    result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
+                    result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                 }
             }
             return result;
@@ -108,7 +112,7 @@ namespace storm {
             
             STORM_LOG_TRACE("Recomputing BDD for state set abstraction.");
             
-            storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
+            storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
             uint_fast64_t modelCounter = 0;
             smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } );
             
@@ -134,7 +138,7 @@ namespace storm {
             smtSolver->push();
             
             // Create the constraint.
-            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<uint_fast64_t, storm::expressions::Variable>> result = constraint.toExpression(globalExpressionInformation.getManager());
+            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<uint_fast64_t, storm::expressions::Variable>> result = constraint.toExpression(this->getAbstractionInformation().getExpressionManager());
             
             // Then add the constraint.
             for (auto const& expression : result.first) {
@@ -143,9 +147,7 @@ namespace storm {
             
             // Finally associate the level variables with the predicates.
             for (auto const& indexVariablePair : result.second) {
-                auto predicateIt = ddInformation.bddVariableIndexToPredicateMap.find(indexVariablePair.first);
-                STORM_LOG_ASSERT(predicateIt != ddInformation.bddVariableIndexToPredicateMap.end(), "Missing predicate for DD variable.");
-                smtSolver->add(storm::expressions::iff(indexVariablePair.second, predicateIt->second));
+                smtSolver->add(storm::expressions::iff(indexVariablePair.second, this->getAbstractionInformation().getPredicateForDdVariableIndex(indexVariablePair.first)));
             }
         }
         
@@ -157,6 +159,16 @@ namespace storm {
             return cachedBdd;
         }
         
+        template <storm::dd::DdType DdType, typename ValueType>
+        AbstractionInformation<DdType>& StateSetAbstractor<DdType, ValueType>::getAbstractionInformation() {
+            return abstractionInformation.get();
+        }
+        
+        template <storm::dd::DdType DdType, typename ValueType>
+        AbstractionInformation<DdType> const& StateSetAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+            return abstractionInformation.get();
+        }
+        
         template class StateSetAbstractor<storm::dd::DdType::CUDD, double>;
         template class StateSetAbstractor<storm::dd::DdType::Sylvan, double>;
     }

src/abstraction/StateSetAbstractor.h

@@ -28,16 +28,13 @@ namespace storm {
     }
     
     namespace abstraction {
-        template <storm::dd::DdType DdType, typename ValueType>
-        class AbstractionDdInformation;
-        
-        class AbstractionExpressionInformation;
+        template <storm::dd::DdType DdType>
+        class AbstractionInformation;
         
         template <storm::dd::DdType DdType, typename ValueType>
         class StateSetAbstractor {
         public:
-            // Provide a no-op default constructor.
-            StateSetAbstractor() = default;
+            StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation);
             
             StateSetAbstractor(StateSetAbstractor const& other) = default;
             StateSetAbstractor& operator=(StateSetAbstractor const& other) = default;
@@ -50,13 +47,12 @@ namespace storm {
             /*!
              * Creates a state set abstractor.
              *
-             * @param expressionInformation The expression-related information including the manager and the predicates.
-             * @param ddInformation The DD-related information including the manager.
+             * @param abstractionInformation An object storing information about the abstraction such as predicates and BDDs.
              * @param statePredicates A set of predicates that have to hold in the concrete states this abstractor is
              * supposed to abstract.
              * @param smtSolverFactory A factory that can create new SMT solvers.
              */
-            StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+            StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
             
             /*!
              * Refines the abstractor by making the given predicates new abstract predicates.
@@ -110,14 +106,25 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const;
             
+            /*!
+             * Retrieves the abstraction information.
+             *
+             * @return The abstraction information.
+             */
+            AbstractionInformation<DdType>& getAbstractionInformation();
+
+            /*!
+             * Retrieves the abstraction information.
+             *
+             * @return The abstraction information.
+             */
+            AbstractionInformation<DdType> const& getAbstractionInformation() const;
+            
             // The SMT solver used for abstracting the set of states.
             std::unique_ptr<storm::solver::SmtSolver> smtSolver;
             
-            // The global expression-related information.
-            AbstractionExpressionInformation& globalExpressionInformation;
-            
-            // The DD-related information.
-            AbstractionDdInformation<DdType, ValueType> const& ddInformation;
+            // The abstraction-related information.
+            std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
             
             // The local expression-related information.
             LocalExpressionInformation localExpressionInformation;

src/abstraction/prism/AbstractCommand.cpp

@@ -2,8 +2,7 @@
 
 #include <boost/iterator/transform_iterator.hpp>
 
-#include "src/abstraction/AbstractionExpressionInformation.h"
-#include "src/abstraction/AbstractionDdInformation.h"
+#include "src/abstraction/AbstractionInformation.h"
 
 #include "src/storage/dd/DdManager.h"
 #include "src/storage/dd/Add.h"
@@ -11,8 +10,6 @@
 #include "src/storage/prism/Command.h"
 #include "src/storage/prism/Update.h"
 
-#include "src/storage/expressions/ExpressionEvaluator.h"
-
 #include "src/utility/solver.h"
 #include "src/utility/macros.h"
 
@@ -20,22 +17,22 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& globalExpressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(globalExpressionInformation.getManager())), globalExpressionInformation(globalExpressionInformation), ddInformation(ddInformation), command(command), localExpressionInformation(globalExpressionInformation.getVariables()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() {
+            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(abstractionInformation.getDdManager().getBddZero(), 0)), decisionVariables() {
 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
                 
-                // Assert all range expressions to enforce legal variable values.
-                for (auto const& rangeExpression : globalExpressionInformation.getRangeExpressions()) {
-                    smtSolver->add(rangeExpression);
+                // Assert all constraints to enforce legal variable values.
+                for (auto const& constraint : abstractionInformation.getConstraints()) {
+                    smtSolver->add(constraint);
                 }
                 
                 // Assert the guard of the command.
                 smtSolver->add(command.getGuardExpression());
 
                 // Refine the command based on all initial predicates.
-                std::vector<uint_fast64_t> allPredicateIndices(globalExpressionInformation.getNumberOfPredicates());
-                for (auto index = 0; index < globalExpressionInformation.getNumberOfPredicates(); ++index) {
+                std::vector<uint_fast64_t> allPredicateIndices(abstractionInformation.getNumberOfPredicates());
+                for (auto index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
                     allPredicateIndices[index] = index;
                 }
                 this->refine(allPredicateIndices);
@@ -45,7 +42,7 @@ namespace storm {
             void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
                 // Add all predicates to the variable partition.
                 for (auto predicateIndex : predicates) {
-                    localExpressionInformation.addExpression(globalExpressionInformation.getPredicateByIndex(predicateIndex), predicateIndex);
+                    localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
                 }
                 
                 STORM_LOG_TRACE("Current variable partition is: " << localExpressionInformation);
@@ -89,15 +86,15 @@ namespace storm {
                 uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices)));
                 
                 // Finally, build overall result.
-                storm::dd::Bdd<DdType> resultBdd = ddInformation.manager->getBddZero();
+                storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();
                 uint_fast64_t sourceStateIndex = 0;
                 for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
                     STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
                     STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty.");
-                    storm::dd::Bdd<DdType> allDistributions = ddInformation.manager->getBddZero();
+                    storm::dd::Bdd<DdType> allDistributions = this->getAbstractionInformation().getDdManager().getBddZero();
                     uint_fast64_t distributionIndex = 0;
                     for (auto const& distribution : sourceDistributionsPair.second) {
-                        allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex);
+                        allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded);
                         ++distributionIndex;
                         STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty.");
                     }
@@ -107,7 +104,7 @@ namespace storm {
                 }
                 
                 resultBdd &= computeMissingIdentities();
-                resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex());
+                resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount());
                 STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
                 
                 // Cache the result.
@@ -175,9 +172,9 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractCommand<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
                 // Determine and add new relevant source predicates.
-                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables.first, newRelevantPredicates.first);
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first);
                 for (auto const& element : newSourceVariables) {
-                    smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicateByIndex(element.second)));
+                    smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
                     decisionVariables.push_back(element.first);
                 }
                 
@@ -187,9 +184,9 @@ 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>> newSuccessorVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(globalExpressionInformation.getManager(), relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
+                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
                     for (auto const& element : newSuccessorVariables) {
-                        smtSolver->add(storm::expressions::iff(element.first, globalExpressionInformation.getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
+                        smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
                         decisionVariables.push_back(element.first);
                     }
                     
@@ -201,12 +198,12 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
                 STORM_LOG_TRACE("Building source state BDD.");
-                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
                     if (model.getBooleanValue(variableIndexPair.first)) {
-                        result &= ddInformation.predicateBdds[variableIndexPair.second].first;
+                        result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                     } else {
-                        result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
+                        result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                     }
                 }
                 
@@ -217,19 +214,19 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
                 STORM_LOG_TRACE("Building distribution BDD.");
-                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
                 
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
-                    storm::dd::Bdd<DdType> updateBdd = ddInformation.manager->getBddOne();
+                    storm::dd::Bdd<DdType> updateBdd = this->getAbstractionInformation().getDdManager().getBddOne();
 
                     // Translate block variables for this update into a successor block.
                     for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) {
                         if (model.getBooleanValue(variableIndexPair.first)) {
-                            updateBdd &= ddInformation.predicateBdds[variableIndexPair.second].second;
+                            updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
                         } else {
-                            updateBdd &= !ddInformation.predicateBdds[variableIndexPair.second].second;
+                            updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
                         }
-                        updateBdd &= ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
+                        updateBdd &= this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount());
                     }
                     
                     result |= updateBdd;
@@ -248,7 +245,7 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingUpdateIdentities() const {
-                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
                     // Compute the identities that are missing for this update.
                     auto firstIt = relevantPredicatesAndVariables.first.begin();
@@ -258,17 +255,17 @@ namespace storm {
                     
                     // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
                     // relevant successor predicates for any update.
-                    storm::dd::Bdd<DdType> updateIdentity = ddInformation.manager->getBddOne();
+                    storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
                     for (; firstIt != firstIte; ++firstIt) {
                         // If the predicates do not match, there is a predicate missing, so we need to add its identity.
                         if (secondIt == secondIte || firstIt->second != secondIt->second) {
-                            updateIdentity &= ddInformation.predicateIdentities[firstIt->second];
+                            updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(firstIt->second);
                         } else if (secondIt != secondIte) {
                             ++secondIt;
                         }
                     }
                     
-                    result |= updateIdentity && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
+                    result |= updateIdentity && this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount());
                 }
                 return result;
             }
@@ -278,10 +275,10 @@ namespace storm {
                 auto relevantIt = relevantPredicatesAndVariables.first.begin();
                 auto relevantIte = relevantPredicatesAndVariables.first.end();
                 
-                storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
-                for (uint_fast64_t predicateIndex = 0; predicateIndex < globalExpressionInformation.getNumberOfPredicates(); ++predicateIndex) {
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
+                for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                     if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
-                        result &= ddInformation.predicateIdentities[predicateIndex];
+                        result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                     } else {
                         ++relevantIt;
                     }
@@ -296,15 +293,24 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Add<DdType, ValueType> AbstractCommand<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
-                storm::expressions::ExpressionEvaluator<ValueType> evaluator(globalExpressionInformation.getManager());
-                storm::dd::Add<DdType, ValueType> result = ddInformation.manager->template getAddZero<ValueType>();
+                storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
-                    result += ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex).template toAdd<ValueType>() * ddInformation.manager->getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
+                    result += this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
                 }
-                result *= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()).template toAdd<ValueType>();
+                result *= this->getAbstractionInformation().encodePlayer2Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer2VariableCount()).template toAdd<ValueType>();
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType> const& AbstractCommand<DdType, ValueType>::getAbstractionInformation() const {
+                return abstractionInformation.get();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType>& AbstractCommand<DdType, ValueType>::getAbstractionInformation() {
+                return abstractionInformation.get();
+            }
+            
             template class AbstractCommand<storm::dd::DdType::CUDD, double>;
             template class AbstractCommand<storm::dd::DdType::Sylvan, double>;
         }

src/abstraction/prism/AbstractCommand.h

@@ -7,6 +7,8 @@
 
 #include "src/abstraction/LocalExpressionInformation.h"
 
+#include "src/storage/expressions/ExpressionEvaluator.h"
+
 #include "src/storage/dd/DdType.h"
 #include "src/storage/expressions/Expression.h"
 
@@ -34,10 +36,8 @@ namespace storm {
     }
     
     namespace abstraction {
-        template <storm::dd::DdType DdType, typename ValueType>
-        struct AbstractionDdInformation;
-        
-        struct AbstractionExpressionInformation;
+        template <storm::dd::DdType DdType>
+        class AbstractionInformation;
         
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
@@ -47,11 +47,10 @@ namespace storm {
                  * Constructs an abstract command from the given command and the initial predicates.
                  *
                  * @param command The concrete command for which to build the abstraction.
-                 * @param expressionInformation The expression-related information including the manager and the predicates.
-                 * @param ddInformation The DD-related information including the manager.
+                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  */
-                AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 /*!
                  * Refines the abstract command with the given predicates.
@@ -145,6 +144,20 @@ namespace storm {
                  */
                 storm::dd::Bdd<DdType> computeMissingUpdateIdentities() const;
                 
+                /*!
+                 * Retrieves the abstraction information object.
+                 *
+                 * @return The abstraction information object.
+                 */
+                AbstractionInformation<DdType> const& getAbstractionInformation() const;
+
+                /*!
+                 * Retrieves the abstraction information object.
+                 *
+                 * @return The abstraction information object.
+                 */
+                AbstractionInformation<DdType>& getAbstractionInformation();
+                
                 /*!
                  * Computes the globally missing state identities.
                  *
@@ -156,11 +169,8 @@ namespace storm {
                 // An SMT responsible for this abstract command.
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
-                // The global expression-related information.
-                AbstractionExpressionInformation& globalExpressionInformation;
-                
-                // The DD-related information.
-                AbstractionDdInformation<DdType, ValueType> const& ddInformation;
+                // The abstraction-related information.
+                std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
                 
                 // The concrete command this abstract command refers to.
                 std::reference_wrapper<storm::prism::Command const> command;
@@ -168,6 +178,9 @@ namespace storm {
                 // The local expression-related information.
                 LocalExpressionInformation localExpressionInformation;
                 
+                // The evaluator used to translate the probability expressions.
+                storm::expressions::ExpressionEvaluator<ValueType> evaluator;
+                
                 // 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;
                 

src/abstraction/prism/AbstractModule.cpp

@@ -1,7 +1,6 @@
 #include "src/abstraction/prism/AbstractModule.h"
 
-#include "src/abstraction/AbstractionExpressionInformation.h"
-#include "src/abstraction/AbstractionDdInformation.h"
+#include "src/abstraction/AbstractionInformation.h"
 
 #include "src/storage/dd/DdManager.h"
 #include "src/storage/dd/Add.h"
@@ -13,11 +12,11 @@ namespace storm {
         namespace prism {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) {
+            AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
                 
                 // For each concrete command, we create an abstract counterpart.
                 for (auto const& command : module.getCommands()) {
-                    commands.emplace_back(command, expressionInformation, ddInformation, smtSolverFactory);
+                    commands.emplace_back(command, abstractionInformation, smtSolverFactory);
                 }
             }
             
@@ -40,16 +39,16 @@ namespace storm {
                 
                 // Then, we build the module BDD 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::Bdd<DdType> result = ddInformation.manager->getBddZero();
+                storm::dd::Bdd<DdType> result = abstractionInformation.getDdManager().getBddZero();
                 for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) {
-                    result |= commandDd.first && ddInformation.getMissingOptionVariableCube(commandDd.second, maximalNumberOfUsedOptionVariables);
+                    result |= commandDd.first && abstractionInformation.getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.second);
                 }
                 return std::make_pair(result, maximalNumberOfUsedOptionVariables);
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Add<DdType, ValueType> AbstractModule<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
-                storm::dd::Add<DdType, ValueType> result = ddInformation.manager->template getAddZero<ValueType>();
+                storm::dd::Add<DdType, ValueType> result = abstractionInformation.getDdManager().template getAddZero<ValueType>();
                 for (auto const& command : commands) {
                     result += command.getCommandUpdateProbabilitiesAdd();
                 }

src/abstraction/prism/AbstractModule.h

@@ -15,10 +15,8 @@ namespace storm {
     }
     
     namespace abstraction {
-        template <storm::dd::DdType DdType, typename ValueType>
-        struct AbstractionDdInformation;
-        
-        struct AbstractionExpressionInformation;
+        template <storm::dd::DdType DdType>
+        class AbstractionInformation;
         
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
@@ -28,11 +26,10 @@ namespace storm {
                  * Constructs an abstract module from the given module and the initial predicates.
                  *
                  * @param module The concrete module for which to build the abstraction.
-                 * @param expressionInformation The expression-related information including the manager and the predicates.
-                 * @param ddInformation The DD-related information including the manager.
+                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  */
-                AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                AbstractModule(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 /*!
                  * Refines the abstract module with the given predicates.
@@ -60,7 +57,7 @@ namespace storm {
                 storm::utility::solver::SmtSolverFactory const& smtSolverFactory;
                 
                 // The DD-related information.
-                AbstractionDdInformation<DdType, ValueType> const& ddInformation;
+                AbstractionInformation<DdType> const& abstractionInformation;
                 
                 // The abstract commands of the abstract module.
                 std::vector<AbstractCommand<DdType, ValueType>> commands;

src/abstraction/prism/AbstractProgram.cpp

@@ -17,12 +17,24 @@ namespace storm {
         namespace prism {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) {
+            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program,
+                                                                std::vector<storm::expressions::Expression> const& initialPredicates,
+                                                                std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory,
+                                                                bool addAllGuards)
+            : program(program), smtSolverFactory(std::move(smtSolverFactory)), modules(), abstractionInformation(expressionManager), initialStateAbstractor(), addedAllGuards(addAllGuards), bottomStateAbstractor(), currentGame(nullptr) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
                 STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules.");
                 
+                // Add all variables and range expressions to the information object.
+                for (auto const& variable : this->program.get().getAllExpressionVariables()) {
+                    abstractionInformation.addExpressionVariable(variable);
+                }
+                for (auto const& range : this->program.get().getAllRangeExpressions()) {
+                    abstractionInformation.addConstraint(range);
+                }
+                
                 uint_fast64_t totalNumberOfCommands = 0;
                 uint_fast64_t maximalUpdateCount = 0;
                 std::vector<storm::expressions::Expression> allGuards;
@@ -30,7 +42,6 @@ namespace storm {
                     // If we were requested to add all guards to the set of predicates, we do so now.
                     for (auto const& command : module.getCommands()) {
                         if (addAllGuards) {
-                            expressionInformation.getPredicates().push_back(command.getGuardExpression());
                             allGuards.push_back(command.getGuardExpression());
                         }
                         maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
@@ -39,39 +50,33 @@ namespace storm {
                     totalNumberOfCommands += module.getNumberOfCommands();
                 }
                 
-                // Create DD variable for the command encoding.
-                ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
-                
-                // Create DD variable for update encoding.
-                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) {
-                    storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first;
-                    ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getEncoding(newOptionVar, 1)));
-                }
+                // NOTE: currently we assume that 100 player 2variables 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.
+                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
                 
                 // Now that we have created all other DD variables, we create the DD variables for the predicates.
                 if (addAllGuards) {
                     for (auto const& guard : allGuards) {
-                        ddInformation.addPredicate(guard);
+                        abstractionInformation.addPredicate(guard);
                     }
                 }
                 for (auto const& predicate : initialPredicates) {
-                    ddInformation.addPredicate(predicate);
+                    abstractionInformation.addPredicate(predicate);
                 }
                 
                 // For each module of the concrete program, we create an abstract counterpart.
                 for (auto const& module : program.getModules()) {
-                    modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory);
+                    modules.emplace_back(module, abstractionInformation, *this->smtSolverFactory);
                 }
                 
                 // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
                 commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
                 
+                // Create the state set abstractors.
+                initialStateAbstractor = storm::abstraction::StateSetAbstractor<DdType, ValueType>(abstractionInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory);
+                bottomStateAbstractor = storm::abstraction::StateSetAbstractor<DdType, ValueType>(abstractionInformation, program.getAllGuards(true), *this->smtSolverFactory);
+                
                 // Finally, we build the game the first time.
                 currentGame = buildGame();
             }
@@ -81,19 +86,11 @@ namespace storm {
                 STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates.");
                 
                 // Add the predicates to the global list of predicates.
-                uint_fast64_t firstNewPredicateIndex = expressionInformation.getPredicates().size();
-                expressionInformation.addPredicates(predicates);
-                
-                // Create DD variables and some auxiliary data structures for the new predicates.
+                std::vector<uint_fast64_t> newPredicateIndices;
                 for (auto const& predicate : predicates) {
                     STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool.");
-                    ddInformation.addPredicate(predicate);
-                }
-
-                // Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors.
-                std::vector<uint_fast64_t> newPredicateIndices;
-                for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.getPredicates().size(); ++index) {
-                    newPredicateIndices.push_back(index);
+                    uint_fast64_t newPredicateIndex = abstractionInformation.addPredicate(predicate);
+                    newPredicateIndices.push_back(newPredicateIndex);
                 }
                 
                 // Refine all abstract modules.
@@ -107,7 +104,7 @@ namespace storm {
                 // Refine bottom state abstractor.
                 bottomStateAbstractor.refine(newPredicateIndices);
                 
-                // Finally, we rebuild the game..
+                // Finally, we rebuild the game.
                 currentGame = buildGame();
             }
             
@@ -120,14 +117,7 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
-                uint_fast64_t index = 0;
-                for (auto const& knownPredicate : expressionInformation.getPredicates()) {
-                    if (knownPredicate.areSame(predicate)) {
-                        return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first;
-                    }
-                    ++index;
-                }
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given predicate is illegal, since it was neither used as an initial predicate nor used to refine the abstraction.");
+                return abstractionInformation.getPredicateSourceVariable(predicate);
             }
                         
             template <storm::dd::DdType DdType, typename ValueType>
@@ -136,10 +126,9 @@ namespace storm {
                 std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> gameBdd = modules.front().getAbstractBdd();
 
                 // Construct a set of all unnecessary variables, so we can abstract from it.
-                std::set<storm::expressions::Variable> variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable};
-                for (uint_fast64_t index = 0; index < gameBdd.second; ++index) {
-                    variablesToAbstract.insert(ddInformation.optionDdVariables[index].first);
-                }
+                std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
+                variablesToAbstract.insert(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().end());
+                variablesToAbstract.insert(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().begin() + gameBdd.second);
 
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract);
@@ -149,34 +138,31 @@ namespace storm {
                 // Determine the bottom states.
                 storm::dd::Bdd<DdType> bottomStates;
                 if (addedAllGuards) {
-                    bottomStates = ddInformation.manager->getBddZero();
+                    bottomStates = abstractionInformation.getDdManager().getBddZero();
                 } else {
                     bottomStateAbstractor.constrain(reachableStates);
                     bottomStates = bottomStateAbstractor.getAbstractStates();
                 }
                 
                 // Find the deadlock states in the model.
-                storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
+                storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());
                 deadlockStates = reachableStates && !deadlockStates;
                 
                 // If there are deadlock states, we fix them now.
-                storm::dd::Add<DdType, ValueType> deadlockTransitions = ddInformation.manager->template getAddZero<ValueType>();
+                storm::dd::Add<DdType, ValueType> deadlockTransitions = abstractionInformation.getDdManager().template getAddZero<ValueType>();
                 if (!deadlockStates.isZero()) {
-                    deadlockTransitions = (deadlockStates && ddInformation.allPredicateIdentities && ddInformation.manager->getEncoding(ddInformation.commandDdVariable, 0)  && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, 0) && ddInformation.getMissingOptionVariableCube(0, gameBdd.second)).template toAdd<ValueType>();
+                    deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeProbabilisticChoice(0, abstractionInformation.getProbabilisticBranchingVariableCount())).template toAdd<ValueType>();
                 }
                 
                 // Construct the transition matrix by cutting away the transitions of unreachable states.
                 storm::dd::Add<DdType> transitionMatrix = (gameBdd.first && reachableStates).template toAdd<ValueType>() * commandUpdateProbabilitiesAdd + deadlockTransitions;
             
-                std::set<storm::expressions::Variable> usedPlayer2Variables;
-                for (uint_fast64_t index = 0; index < gameBdd.second; ++index) {
-                    usedPlayer2Variables.insert(usedPlayer2Variables.end(), ddInformation.optionDdVariables[index].first);
-                }
+                std::set<storm::expressions::Variable> usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + gameBdd.second);
                 
                 std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
-                allNondeterminismVariables.insert(ddInformation.commandDdVariable);
+                allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
                 
-                return std::unique_ptr<MenuGame<DdType, ValueType>>(new MenuGame<DdType, ValueType>(ddInformation.manager, reachableStates, initialStates, ddInformation.manager->getBddZero(), transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap));
+                return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set<storm::expressions::Variable>(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().end()), abstractionInformation.getPredicateToBddMap());
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -187,8 +173,8 @@ namespace storm {
                 uint_fast64_t reachabilityIteration = 0;
                 while (!frontier.isZero()) {
                     ++reachabilityIteration;
-                    frontier = frontier.andExists(transitionRelation, ddInformation.sourceVariables);
-                    frontier = frontier.swapVariables(ddInformation.predicateDdVariables);
+                    frontier = frontier.andExists(transitionRelation, abstractionInformation.getSourceVariables());
+                    frontier = frontier.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs());
                     frontier &= !reachableStates;
                     reachableStates |= frontier;
                     STORM_LOG_TRACE("Iteration " << reachabilityIteration << " of reachability analysis.");

src/abstraction/prism/AbstractProgram.h

@@ -2,8 +2,7 @@
 
 #include "src/storage/dd/DdType.h"
 
-#include "src/abstraction/AbstractionDdInformation.h"
-#include "src/abstraction/AbstractionExpressionInformation.h"
+#include "src/abstraction/AbstractionInformation.h"
 #include "src/abstraction/StateSetAbstractor.h"
 #include "src/abstraction/MenuGame.h"
 #include "src/abstraction/prism/AbstractModule.h"
@@ -87,20 +86,17 @@ namespace storm {
                  */
                 std::unique_ptr<MenuGame<DdType, ValueType>> buildGame();
                 
+                // The concrete program this abstract program refers to.
+                std::reference_wrapper<storm::prism::Program const> program;
+
                 // A factory that can be used to create new SMT solvers.
                 std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
                 
-                // A struct containing all DD-related information like variables and managers.
-                AbstractionDdInformation<DdType, ValueType> ddInformation;
-                
-                // A struct containing all expression-related information like variables, managers and the predicates.
-                AbstractionExpressionInformation expressionInformation;
-                
                 // The abstract modules of the abstract program.
                 std::vector<AbstractModule<DdType, ValueType>> modules;
                 
-                // The concrete program this abstract program refers to.
-                std::reference_wrapper<storm::prism::Program const> program;
+                // An object containing all information about the abstraction like predicates and the corresponding DDs.
+                AbstractionInformation<DdType> abstractionInformation;
 
                 // A state-set abstractor used to determine the initial states of the abstraction.
                 StateSetAbstractor<DdType, ValueType> initialStateAbstractor;

src/storage/expressions/Expression.h

@@ -368,17 +368,22 @@ namespace storm {
 namespace std {
 	template <>
 	struct less<storm::expressions::Expression> {
-		bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const {
+		bool operator()(storm::expressions::Expression const& lhs, storm::expressions::Expression const& rhs) const {
 			return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer();
 		}
 	};
-}
 
-namespace std {
     template <>
     struct hash<storm::expressions::Expression> {
-        size_t operator()(const storm::expressions::Expression& expr) const {
-            return reinterpret_cast<size_t>(expr.getBaseExpressionPointer().get());
+        size_t operator()(storm::expressions::Expression const& e) const {
+            return reinterpret_cast<size_t>(e.getBaseExpressionPointer().get());
+        }
+    };
+
+    template <>
+    struct equal_to<storm::expressions::Expression> {
+        bool operator()(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2) const {
+            return e1.areSame(e2);
         }
     };
 }

src/storage/expressions/ExprtkExpressionEvaluator.cpp

@@ -7,18 +7,18 @@
 namespace storm {
     namespace expressions {
         template<typename RationalType>
-        ExprtkExpressionEvaluatorBase<RationalType>::ExprtkExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorBase<RationalType>(manager), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
+        ExprtkExpressionEvaluatorBase<RationalType>::ExprtkExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorBase<RationalType>(manager), parser(std::make_unique<exprtk::parser<ValueType>>()), symbolTable(std::make_unique<exprtk::symbol_table<ValueType>>()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
 
             for (auto const& variableTypePair : manager) {
                 if (variableTypePair.second.isBooleanType()) {
-                    symbolTable.add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]);
                 } else if (variableTypePair.second.isIntegerType()) {
-                    symbolTable.add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]);
                 } else if (variableTypePair.second.isRationalType()) {
-                    symbolTable.add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]);
+                    symbolTable->add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]);
                 }
             }
-            symbolTable.add_constants();
+            symbolTable->add_constants();
         }
         
         template<typename RationalType>
@@ -47,8 +47,8 @@ namespace storm {
         typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const {
             std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType());
             CompiledExpressionType& compiledExpression = result.first->second;
-            compiledExpression.register_symbol_table(symbolTable);
-            bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
+            compiledExpression.register_symbol_table(*symbolTable);
+            bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
             STORM_LOG_ASSERT(parsingOk, "Expression was not properly parsed by ExprTk: " << expression);
             return compiledExpression;
         }

src/storage/expressions/ExprtkExpressionEvaluator.h

@@ -37,10 +37,10 @@ namespace storm {
             CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const;
             
             // The parser used.
-            mutable exprtk::parser<ValueType> parser;
+            mutable std::unique_ptr<exprtk::parser<ValueType>> parser;
             
             // The symbol table used.
-            mutable exprtk::symbol_table<ValueType> symbolTable;
+            mutable std::unique_ptr<exprtk::symbol_table<ValueType>> symbolTable;
             
             // The actual data that is fed into the expression.
             std::vector<ValueType> booleanValues;