DD meta variables can now be inserted at particular locations. added some tests for game abstraction

Former-commit-id: 1c870dc0de

src/storage/dd/CuddAdd.cpp

@@ -420,6 +420,10 @@ namespace storm {
             return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
         }
         
+        uint_fast64_t Add<DdType::CUDD>::getLevel() const {
+            return static_cast<uint_fast64_t>(this->getDdManager()->getCuddManager().ReadPerm(this->getIndex()));
+        }
+        
         template<typename ValueType>
         std::vector<ValueType> Add<DdType::CUDD>::toVector() const {
             return this->toVector<ValueType>(Odd<DdType::CUDD>(*this));

src/storage/dd/CuddAdd.h

@@ -520,6 +520,13 @@ namespace storm {
              */
             virtual uint_fast64_t getIndex() const override;
             
+            /*!
+             * Retrieves the level of the topmost variable in the DD.
+             *
+             * @return The level of the topmost variable in DD.
+             */
+            virtual uint_fast64_t getLevel() const override;
+            
             /*!
              * Converts the ADD to a vector.
              *

src/storage/dd/CuddBdd.cpp

@@ -35,7 +35,6 @@ namespace storm {
                     this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
                     break;
             }
-
         }
         
         Add<DdType::CUDD> Bdd<DdType::CUDD>::toAdd() const {
@@ -242,6 +241,10 @@ namespace storm {
             return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
         }
         
+        uint_fast64_t Bdd<DdType::CUDD>::getLevel() const {
+            return static_cast<uint_fast64_t>(this->getDdManager()->getCuddManager().ReadPerm(this->getIndex()));
+        }
+        
         void Bdd<DdType::CUDD>::exportToDot(std::string const& filename) const {
             if (filename.empty()) {
                 std::vector<BDD> cuddBddVector = { this->getCuddBdd() };

src/storage/dd/CuddBdd.h

@@ -262,6 +262,13 @@ namespace storm {
              */
             virtual uint_fast64_t getIndex() const override;
             
+            /*!
+             * Retrieves the level of the topmost variable in the DD.
+             *
+             * @return The level of the topmost variable in DD.
+             */
+            virtual uint_fast64_t getLevel() const override;
+            
             /*!
              * Exports the BDD to the given file in the dot format.
              *

src/storage/dd/CuddDd.h

@@ -68,6 +68,13 @@ namespace storm {
              */
             virtual uint_fast64_t getIndex() const = 0;
             
+            /*!
+             * Retrieves the level of the topmost variable in the DD.
+             *
+             * @return The level of the topmost variable in DD.
+             */
+            virtual uint_fast64_t getLevel() const = 0;
+            
             /*!
              * Retrieves whether the given meta variable is contained in the DD.
              *

src/storage/dd/CuddDdManager.cpp

@@ -114,7 +114,7 @@ namespace storm {
             return result;
         }
 
-        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
+        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
             // Check whether the variable name is legal.
             STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
             
@@ -126,15 +126,33 @@ namespace storm {
             
             std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
             
+            // If a specific position was requested, we compute it now.
+            boost::optional<uint_fast64_t> level;
+            if (position) {
+                storm::dd::DdMetaVariable<DdType::CUDD> beforeVariable = this->getMetaVariable(position.get().second);
+                level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits<uint_fast64_t>::max() : std::numeric_limits<uint_fast64_t>::min();
+                for (auto const& ddVariable : beforeVariable.getDdVariables()) {
+                    level = position.get().first == MetaVariablePosition::Above ? std::min(level.get(), ddVariable.getLevel()) : std::max(level.get(), ddVariable.getLevel());
+                }
+                if (position.get().first == MetaVariablePosition::Below) {
+                    ++level.get();
+                }
+            }
+            
             storm::expressions::Variable unprimed = manager->declareBitVectorVariable(name, numberOfBits);
             storm::expressions::Variable primed = manager->declareBitVectorVariable(name + "'", numberOfBits);
             
             std::vector<Bdd<DdType::CUDD>> variables;
             std::vector<Bdd<DdType::CUDD>> variablesPrime;
             for (std::size_t i = 0; i < numberOfBits; ++i) {
+                if (level) {
+                    variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get() + 2 * i), {unprimed}));
+                    variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get() + 2 * i + 1), {primed}));
+                } else {
                     variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
                     variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
                 }
+            }
             
             // Now group the non-primed and primed variable.
             for (uint_fast64_t i = 0; i < numberOfBits; ++i) {
@@ -147,20 +165,38 @@ namespace storm {
             return std::make_pair(unprimed, primed);
         }
         
-        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name) {
+        std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<DdType::CUDD>::addMetaVariable(std::string const& name, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
             // Check whether the variable name is legal.
             STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
             
             // Check whether a meta variable already exists.
             STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
             
+            // If a specific position was requested, we compute it now.
+            boost::optional<uint_fast64_t> level;
+            if (position) {
+                storm::dd::DdMetaVariable<DdType::CUDD> beforeVariable = this->getMetaVariable(position.get().second);
+                level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits<uint_fast64_t>::max() : std::numeric_limits<uint_fast64_t>::min();
+                for (auto const& ddVariable : beforeVariable.getDdVariables()) {
+                    level = position.get().first == MetaVariablePosition::Above ? std::min(level.get(), ddVariable.getLevel()) : std::max(level.get(), ddVariable.getLevel());
+                }
+                if (position.get().first == MetaVariablePosition::Below) {
+                    ++level.get();
+                }
+            }
+            
             storm::expressions::Variable unprimed = manager->declareBooleanVariable(name);
             storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'");
 
             std::vector<Bdd<DdType::CUDD>> variables;
             std::vector<Bdd<DdType::CUDD>> variablesPrime;
+            if (position) {
+                variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get()), {unprimed}));
+                variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddNewVarAtLevel(level.get() + 1), {primed}));
+            } else {
                 variables.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
                 variablesPrime.emplace_back(Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
+            }
 
             // Now group the non-primed and primed variable.
             this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED);

src/storage/dd/CuddDdManager.h

@@ -3,7 +3,9 @@
 
 #include <unordered_map>
 #include <memory>
+#include <boost/optional.hpp>
 
+#include "src/storage/dd/MetaVariablePosition.h"
 #include "src/storage/dd/DdManager.h"
 #include "src/storage/dd/CuddDdMetaVariable.h"
 #include "src/utility/OsDetection.h"
@@ -110,15 +112,19 @@ namespace storm {
              * @param variableName The name of the new variable.
              * @param low The lowest value of the range of the variable.
              * @param high The highest value of the range of the variable.
+             * @param position A pair indicating the position of the new meta variable. If not given, the meta variable
+             * will be created below all existing ones.
              */
-            std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high);
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, int_fast64_t low, int_fast64_t high, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);
             
             /*!
              * Adds a boolean meta variable.
              *
              * @param variableName The name of the new variable.
+             * @param position A pair indicating the position of the new meta variable. If not given, the meta variable
+             * will be created below all existing ones.
              */
-            std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName);
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> addMetaVariable(std::string const& variableName, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none);
             
             /*!
              * Retrieves the names of all meta variables that have been added to the manager.

src/storage/dd/MetaVariablePosition.h

@@ -0,0 +1,15 @@
+#ifndef STORM_STORAGE_DD_METAVARIABLEPOSITION_H_
+#define STORM_STORAGE_DD_METAVARIABLEPOSITION_H_
+
+#include "src/storage/dd/DdType.h"
+
+namespace storm {
+    namespace dd {
+
+        // An enum that expresses the relation of two meta variables relative to each other.
+        enum class MetaVariablePosition { Above, Below };
+        
+    }
+}
+
+#endif /* STORM_STORAGE_DD_METAVARIABLEPOSITION_H_ */

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -71,11 +71,11 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
                 STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
-                std::cout << "recomputing " << command.get() << std::endl;
                 
                 // Create a mapping from source state DDs to their distributions.
                 std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
-                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); return true; } );
+                uint_fast64_t modelCounter = 0;
+                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); ++modelCounter; return true; } );
                 
                 // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
                 // need to encode the nondeterminism.
@@ -88,17 +88,27 @@ namespace storm {
                 
                 // Finally, build overall result.
                 storm::dd::Bdd<DdType> resultBdd = ddInformation.manager->getBddZero();
+                uint_fast64_t sourceStateIndex = 0;
                 for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
-                    uint_fast64_t distributionIndex = 0;
+                    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();
+                    uint_fast64_t distributionIndex = 0;
                     for (auto const& distribution : sourceDistributionsPair.second) {
                         allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex);
+                        ++distributionIndex;
+                        STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty.");
                     }
                     resultBdd |= sourceDistributionsPair.first && allDistributions;
+                    ++sourceStateIndex;
+                    STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty.");
                 }
                 
-                resultBdd &= computeMissingSourceStateIdentities();
+                STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
+                resultBdd &= computeMissingIdentities();
+                STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
                 resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex());
+                STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
                 
                 // Cache the result.
                 cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded);
@@ -172,10 +182,6 @@ namespace storm {
                 // Insert the new variables into the record of relevant source variables.
                 relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end());
                 std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
-                std::cout << "sorted!" << std::endl;
-                for (auto const& el : relevantPredicatesAndVariables.first) {
-                    std::cout << el.first.getName() << " // " << el.second << std::endl;
-                }
                 
                 // Do the same for every update.
                 for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
@@ -195,13 +201,14 @@ namespace storm {
                 STORM_LOG_TRACE("Building source state BDD.");
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
-                    std::cout << "size: " << ddInformation.predicateBdds.size() << " and index " << variableIndexPair.second << std::endl;
                     if (model.getBooleanValue(variableIndexPair.first)) {
                         result &= ddInformation.predicateBdds[variableIndexPair.second].first;
                     } else {
                         result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
                     }
                 }
+                
+                STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty.");
                 return result;
             }
             
@@ -223,6 +230,24 @@ namespace storm {
                         updateBdd &= ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
                     }
                     
+                    result |= updateBdd;
+                }
+                
+                STORM_LOG_ASSERT(!result.isZero(), "Distribution must not be empty.");
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingIdentities() const {
+                storm::dd::Bdd<DdType> identities = computeMissingGlobalIdentities();
+                identities &= computeMissingUpdateIdentities();
+                return identities;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingUpdateIdentities() const {
+                storm::dd::Bdd<DdType> result = ddInformation.manager->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();
                     auto firstIte = relevantPredicatesAndVariables.first.end();
@@ -231,33 +256,29 @@ 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();
                     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) {
-                            updateBdd &= ddInformation.predicateIdentities[firstIt->second];
+                            updateIdentity &= ddInformation.predicateIdentities[firstIt->second];
                         } else if (secondIt != secondIte) {
                             ++secondIt;
                         }
                     }
                     
-                    result |= updateBdd;
+                    result |= updateIdentity && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex);
                 }
-                
                 return result;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingSourceStateIdentities() const {
+            storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingGlobalIdentities() const {
                 auto relevantIt = relevantPredicatesAndVariables.first.begin();
                 auto relevantIte = relevantPredicatesAndVariables.first.end();
-                std::cout << "the size is " << relevantPredicatesAndVariables.first.size() << std::endl;
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) {
                     if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
-                        std::cout << (relevantIt == relevantIte) << std::endl;
-                        std::cout << relevantIt->second << " vs " << predicateIndex << std::endl;
-                        std::cout << "multiplying identity " << predicateIndex << std::endl;
                         result &= ddInformation.predicateIdentities[predicateIndex];
                     } else {
                         ++relevantIt;

src/storage/prism/menu_games/AbstractCommand.h

@@ -130,12 +130,27 @@ namespace storm {
                 void recomputeCachedBdd();
 
                 /*!
-                 * Computes the missing source state identities.
+                 * Computes the missing state identities.
                  *
-                 * @return A BDD that represents the source state identities for predicates that are irrelevant for the
+                 * @return A BDD that represents the all missing state identities.
-                 * source states.
                  */
-                storm::dd::Bdd<DdType> computeMissingSourceStateIdentities() const;
+                storm::dd::Bdd<DdType> computeMissingIdentities() const;
+                
+                /*!
+                 * Computes the missing state identities for the updates.
+                 *
+                 * @return A BDD that represents the state identities for predicates that are irrelevant for the
+                 * successor states.
+                 */
+                storm::dd::Bdd<DdType> computeMissingUpdateIdentities() const;
+                
+                /*!
+                 * Computes the globally missing state identities.
+                 *
+                 * @return A BDD that represents the global state identities for predicates that are irrelevant for the
+                 * source and successor states.
+                 */
+                storm::dd::Bdd<DdType> computeMissingGlobalIdentities() const;
                 
                 // An SMT responsible for this abstract command.
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -34,11 +34,6 @@ namespace storm {
                     totalNumberOfCommands += module.getNumberOfCommands();
                 }
                 
-                // Create DD variables for all predicates.
-                for (auto const& predicate : expressionInformation.predicates) {
-                    ddInformation.addPredicate(predicate);
-                }
-                
                 // Create DD variable for the command encoding.
                 ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
                 
@@ -51,7 +46,12 @@ namespace storm {
                 // 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->getRange(newOptionVar)));
+                    ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getIdentity(newOptionVar).toBdd()));
+                }
+                
+                // Create DD variables for all predicates.
+                for (auto const& predicate : expressionInformation.predicates) {
+                    ddInformation.addPredicate(predicate);
                 }
                 
                 // For each module of the concrete program, we create an abstract counterpart.
@@ -68,8 +68,6 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
-                std::cout << "refining!" << std::endl;
-
                 // Add the predicates to the global list of predicates.
                 uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
                 expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end());
@@ -85,17 +83,13 @@ namespace storm {
                     newPredicateIndices.push_back(index);
                 }
                 
-                std::cout << "refining modules" << std::endl;
                 // Refine all abstract modules.
                 for (auto& module : modules) {
                     module.refine(newPredicateIndices);
                 }
                 
-                std::cout << "refining initial" << std::endl;
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(newPredicateIndices);
-                
-                std::cout << "done " << std::endl;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -108,8 +102,6 @@ namespace storm {
                     return lastAbstractAdd;
                 }
                 
-                std::cout << "abstr DD new " << std::endl;
-                
                 // Otherwise, we remember that the abstract BDD changed and perform a reachability analysis.
                 lastAbstractBdd = gameBdd.first;
 
@@ -119,14 +111,10 @@ namespace storm {
                     variablesToAbstract.insert(ddInformation.optionDdVariables[index].first);
                 }
                 
-                std::cout << "reachability... " << std::endl;
-                
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
 
-                std::cout << "done " << std::endl;
-                
                 // Find the deadlock states in the model.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
                 deadlockStates = reachableStates && !deadlockStates;

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -9,6 +9,8 @@
 #include "src/storage/dd/CuddBdd.h"
 #include "src/storage/dd/CuddAdd.h"
 
+#include "src/utility/macros.h"
+
 namespace storm {
     namespace prism {
         namespace menu_games {
@@ -22,6 +24,7 @@ namespace storm {
             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 {
@@ -29,6 +32,7 @@ namespace storm {
                     }
                     distributionIndex >>= 1;
                 }
+                STORM_LOG_ASSERT(!result.isZero(), "Update BDD encoding must not be zero.");
                 return result;
             }
             
@@ -36,7 +40,15 @@ namespace storm {
             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());
+                std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable;
+                
+                // Create the new predicate variable below all other predicate variables.
+                if (predicateDdVariables.empty()) {
+                    newMetaVariable = manager->addMetaVariable(stream.str());
+                } else {
+                    newMetaVariable = manager->addMetaVariable(stream.str(), std::make_pair(storm::dd::MetaVariablePosition::Below, predicateDdVariables.back().second));
+                }
+                
                 predicateDdVariables.push_back(newMetaVariable);
                 predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
                 predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd());
@@ -46,13 +58,15 @@ namespace storm {
             }
          
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> AbstractionDdInformation<DdType, ValueType>::getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const {
+            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 = lastUsed + 1; index <= lastToBe; ++index) {
+                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;
             }
             
@@ -66,6 +80,8 @@ namespace storm {
                     // 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;
                     }
                 }
                 

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -52,13 +52,13 @@ namespace storm {
                 void addPredicate(storm::expressions::Expression const& predicate);
                 
                 /*!
-                 * Retrieves the cube of option variables in the range (lastUsed, lastToBe] the given indices.
+                 * Retrieves the cube of option variables in the range [begin, end) the given indices.
                  *
-                 * @param lastUsed The last variable before the range to return.
+                 * @param begin The first variable of the range to return.
-                 * @param lastToBe The last 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 lastUsed, uint_fast64_t lastToBe) const;
+                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

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -15,7 +15,7 @@
 
 #include "src/utility/solver.h"
 
-TEST(PrismMenuGame, CommandAbstractionTest) {
+TEST(PrismMenuGame, DieProgramAbstractionTest) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
 
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -25,13 +25,156 @@ TEST(PrismMenuGame, CommandAbstractionTest) {
     
     storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
-    storm::dd::Add<storm::dd::DdType::CUDD> abstraction = abstractProgram.getAbstractAdd();
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
-    abstraction.exportToDot("abstr1.dot");
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
     
-    abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)});
+    EXPECT_EQ(19, abstraction.getNodeCount());
-    abstraction = abstractProgram.getAbstractAdd();
+}
-    abstraction.exportToDot("abstr2.dot");
+TEST(PrismMenuGame, DieProgramAbstractionAndRefinementTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)}));
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(26, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, CrowdsProgramAbstractionTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    program = program.substituteConstants();
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(46, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, CrowdsProgramAbstractionAndRefinementTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    program = program.substituteConstants();
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(46, abstraction.getNodeCount());
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(75, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, TwoDiceProgramAbstractionTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(38, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, TwoDiceProgramAbstractionAndRefinementTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(38, abstraction.getNodeCount());
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+
+    EXPECT_EQ(107, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, WlanProgramAbstractionTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(219, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, WlanProgramAbstractionAndRefinementTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(219, abstraction.getNodeCount());
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
     
+    EXPECT_EQ(292, abstraction.getNodeCount());
 }
 
 #endif