more work on proper bottom state computation

Former-commit-id: 38718e1c5c

src/abstraction/AbstractionInformation.cpp

@@ -155,24 +155,24 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType>
-        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const {
-            return encodeChoice(index, 0, numberOfVariables, player1VariableBdds);
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const {
+            return encodeChoice(index, 0, end, 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, 0, numberOfVariables, player2VariableBdds);
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const {
+            return encodeChoice(index, 0, end, player2VariableBdds);
         }
         
         template<storm::dd::DdType DdType>
-        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const {
-            return encodeChoice(index, offset, numberOfVariables, auxVariableBdds);
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const {
+            return encodeChoice(index, start, end, auxVariableBdds);
         }
         
         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> AbstractionInformation<DdType>::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const {
             storm::dd::Bdd<DdType> result = ddManager->getBddOne();
-            for (uint_fast64_t index = offset; index < numberOfVariables; ++index) {
+            for (uint_fast64_t index = start; index < end; ++index) {
                 result &= player2VariableBdds[index];
             }
             STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero.");
@@ -205,8 +205,8 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType>
-        std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const {
-            return std::set<storm::expressions::Variable>(auxVariables.begin() + offset, auxVariables.begin() + offset + count);
+        std::set<storm::expressions::Variable> AbstractionInformation<DdType>::getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const {
+            return std::set<storm::expressions::Variable>(auxVariables.begin() + start, auxVariables.begin() + end);
         }
         
         template<storm::dd::DdType DdType>
@@ -298,10 +298,9 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType>
-        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const {
+        storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector<storm::dd::Bdd<DdType>> const& variables) const {
             storm::dd::Bdd<DdType> result = ddManager->getBddOne();
-            numberOfVariables += offset;
-            for (uint_fast64_t bitIndex = numberOfVariables; bitIndex > offset; --bitIndex) {
+            for (uint_fast64_t bitIndex = end; bitIndex > start; --bitIndex) {
                 if ((index & 1) != 0) {
                     result &= variables[bitIndex - 1];
                 } else {

src/abstraction/AbstractionInformation.h

@@ -174,29 +174,29 @@ namespace storm {
              * 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.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
              * @return The index encoded as a BDD.
              */
-            storm::dd::Bdd<DdType> encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const;
+            storm::dd::Bdd<DdType> encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) 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.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
              * @return The index encoded as a BDD.
              */
-            storm::dd::Bdd<DdType> encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const;
+            storm::dd::Bdd<DdType> encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const;
 
             /*!
              * Encodes the given index using the indicated probabilistic branching variables.
              *
              * @param index The index to encode.
-             * @param offset The offset within the auxiliary variables at which to start encoding.
-             * @param numberOfVariables The number of variables to use for encoding the index.
+             * @param start The index of the first variable of the range that is used to encode the index.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
              * @return The index encoded as a BDD.
              */
-            storm::dd::Bdd<DdType> encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const;
+            storm::dd::Bdd<DdType> encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const;
             
             /*!
              * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables).
@@ -262,11 +262,11 @@ namespace storm {
             /*!
              * Retrieves the requested set of auxiliary variables.
              *
-             * @param offset The offset at which to start gatherin the auxiliary variables.
-             * @param count The number of auxiliary variables to include.
+             * @param start The index of the first auxiliary variable to include.
+             * @param end The index of the auxiliary variable past the end of the range to include.
              * @return The set of auxiliary variables.
              */
-            std::set<storm::expressions::Variable> getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const;
+            std::set<storm::expressions::Variable> getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const;
 
             /*!
              * Retrieves the number of auxiliary variables.
@@ -356,11 +356,11 @@ namespace storm {
              * Encodes the given index with the given number of variables from the given variables.
              *
              * @param index The index to encode.
-             * @param offset The offset at which to start encoding.
-             * @param numberOfVariables The total number of variables to use.
+             * @param start The index of the first variable to use for the encoding.
+             * @param end The index of the variable past the end of the range to use for the encoding.
              * @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 offset, uint_fast64_t numberOfVariables, std::vector<storm::dd::Bdd<DdType>> const& variables) const;
+            storm::dd::Bdd<DdType> encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector<storm::dd::Bdd<DdType>> const& variables) const;
                         
             // The expression related data.
             

src/abstraction/BottomStateResult.cpp

@@ -0,0 +1,14 @@
+#include "src/abstraction/BottomStateResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType DdType>
+        BottomStateResult<DdType>::BottomStateResult(storm::dd::Bdd<DdType> const& states, storm::dd::Bdd<DdType> const& transitions) : states(states), transitions(transitions) {
+            // Intentionally left empty.
+        }
+        
+        template class BottomStateResult<storm::dd::DdType::CUDD>;
+        template class BottomStateResult<storm::dd::DdType::Sylvan>;
+    }
+}

src/abstraction/BottomStateResult.h

@@ -0,0 +1,19 @@
+#pragma once
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/Bdd.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType DdType>
+        struct BottomStateResult {
+        public:
+            BottomStateResult(storm::dd::Bdd<DdType> const& states, storm::dd::Bdd<DdType> const& transitions);
+            
+            storm::dd::Bdd<DdType> states;
+            storm::dd::Bdd<DdType> transitions;
+        };
+        
+    }
+}

src/abstraction/MenuGame.cpp

@@ -28,6 +28,7 @@ namespace storm {
                                             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.
+            this->getTransitionMatrix().exportToDot("trans.dot");
         }
         
         template<storm::dd::DdType Type, typename ValueType>

src/abstraction/StateSetAbstractor.cpp

@@ -125,6 +125,8 @@ namespace storm {
             // Create a new backtracking point before adding the constraint.
             smtSolver->push();
             
+            constraint.template toAdd<ValueType>().exportToDot("constraint.dot");
+            
             // Create the constraint.
             std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<uint_fast64_t, storm::expressions::Variable>> result = constraint.toExpression(this->getAbstractionInformation().getExpressionManager());
             

src/abstraction/prism/AbstractCommand.cpp

@@ -3,6 +3,7 @@
 #include <boost/iterator/transform_iterator.hpp>
 
 #include "src/abstraction/AbstractionInformation.h"
+#include "src/abstraction/BottomStateResult.h"
 
 #include "src/storage/dd/DdManager.h"
 #include "src/storage/dd/Add.h"
@@ -17,7 +18,7 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), guardIsPredicate(guardIsPredicate), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) {
+            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0, 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) {
 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@@ -37,9 +38,6 @@ namespace storm {
                     allPredicateIndices[index] = index;
                 }
                 this->refine(allPredicateIndices);
-                
-                // Refine the bottom state abstractor. 
-                bottomStateAbstractor.refine(allPredicateIndices);
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -97,8 +95,15 @@ namespace storm {
                 
                 // Finally, build overall result.
                 storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();
+                if (!guardIsPredicate) {
+                    abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero();
+                }
                 uint_fast64_t sourceStateIndex = 0;
                 for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    if (!guardIsPredicate) {
+                        abstractGuard |= sourceDistributionsPair.first;
+                    }
+                    
                     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 = this->getAbstractionInformation().getDdManager().getBddZero();
@@ -236,7 +241,7 @@ namespace storm {
                         } else {
                             updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
                         }
-                        updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
+                        updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount());
                     }
                     
                     result |= updateBdd;
@@ -275,7 +280,7 @@ namespace storm {
                         }
                     }
                     
-                    result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
+                    result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount());
                 }
                 return result;
             }
@@ -301,11 +306,32 @@ namespace storm {
                 return cachedDd;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            BottomStateResult<DdType> AbstractCommand<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
+                BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
+
+                // Use the state abstractor to compute the set of abstract states that has this command enabled but
+                // still has a transition to a bottom state.
+                bottomStateAbstractor.constrain(reachableStates && abstractGuard);
+                result.states = bottomStateAbstractor.getAbstractStates();
+                
+                // Now equip all these states with an actual transition to a bottom state.
+                result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities();
+                
+                // Add the command encoding and the next free player 2 encoding.
+                result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables);
+                
+                result.states.template toAdd<ValueType>().exportToDot("bottom_" + std::to_string(command.get().getGlobalIndex()) + ".dot");
+                result.transitions.template toAdd<ValueType>().exportToDot("bottom_trans_" + std::to_string(command.get().getGlobalIndex()) + ".dot");
+                
+                return result;
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Add<DdType, ValueType> AbstractCommand<DdType, ValueType>::getCommandUpdateProbabilitiesAdd() const {
                 storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
                 for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
-                    result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
+                    result += this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression()));
                 }
                 result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
                 return result;

src/abstraction/prism/AbstractCommand.h

@@ -40,7 +40,10 @@ namespace storm {
     namespace abstraction {
         template <storm::dd::DdType DdType>
         class AbstractionInformation;
-        
+
+        template <storm::dd::DdType DdType>
+        class BottomStateResult;
+
         namespace prism {
             template<storm::dd::DdType DdType>
             struct GameBddResult;
@@ -73,6 +76,15 @@ namespace storm {
                  */
                 GameBddResult<DdType> getAbstractBdd();
                 
+                /*!
+                 * Retrieves the transitions to bottom states of this command.
+                 *
+                 * @param reachableStates A BDD representing the reachable states.
+                 * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2.
+                 * @return The bottom state transitions in the form of a BDD.
+                 */
+                BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);
+
                 /*!
                  * Retrieves an ADD that maps the encoding of the command and its updates to their probabilities.
                  *
@@ -201,6 +213,10 @@ namespace storm {
                 // is no need to compute bottom states.
                 bool guardIsPredicate;
                 
+                // The abstract guard of the command. This is only used if the guard is not a predicate, because it can
+                // then be used to constrain the bottom state abstractor.
+                storm::dd::Bdd<DdType> abstractGuard;
+                
                 // A state-set abstractor used to determine the bottom states if not all guards were added.
                 StateSetAbstractor<DdType, ValueType> bottomStateAbstractor;
             };

src/abstraction/prism/AbstractModule.cpp

@@ -1,6 +1,7 @@
 #include "src/abstraction/prism/AbstractModule.h"
 
 #include "src/abstraction/AbstractionInformation.h"
+#include "src/abstraction/BottomStateResult.h"
 #include "src/abstraction/prism/GameBddResult.h"
 
 #include "src/storage/dd/DdManager.h"
@@ -50,11 +51,13 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> AbstractModule<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
-                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
+            BottomStateResult<DdType> AbstractModule<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
+                BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
                 
                 for (auto& command : commands) {
-                    result |= command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables);
+                    BottomStateResult<DdType> commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables);
+                    result.states |= commandBottomStateResult.states;
+                    result.transitions |= commandBottomStateResult.transitions;
                 }
                 
                 return result;

src/abstraction/prism/AbstractModule.h

@@ -17,12 +17,14 @@ namespace storm {
     namespace abstraction {
         template <storm::dd::DdType DdType>
         class AbstractionInformation;
+
+        template<storm::dd::DdType DdType>
+        struct BottomStateResult;
         
         namespace prism {
             template<storm::dd::DdType DdType>
             struct GameBddResult;
             
-            
             template <storm::dd::DdType DdType, typename ValueType>
             class AbstractModule {
             public:
@@ -60,9 +62,9 @@ namespace storm {
                  *
                  * @param reachableStates A BDD representing the reachable states.
                  * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2.
-                 * @return The bottom state transitions in the form of a BDD.
+                 * @return The bottom states and the necessary transitions.
                  */
-                storm::dd::Bdd<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);
+                BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);
                 
                 /*!
                  * Retrieves an ADD that maps the encodings of commands and their updates to their probabilities.

src/abstraction/prism/AbstractProgram.cpp

@@ -1,5 +1,7 @@
 #include "src/abstraction/prism/AbstractProgram.h"
 
+#include "src/abstraction/BottomStateResult.h"
+
 #include "src/storage/prism/Program.h"
 
 #include "src/storage/dd/DdManager.h"
@@ -54,7 +56,7 @@ namespace storm {
                 // NOTE: currently we assume that 100 player 2 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.
-                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
+                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))) + 1);
                 
                 // Now that we have created all other DD variables, we create the DD variables for the predicates.
                 std::vector<uint_fast64_t> allPredicateIndices;
@@ -127,31 +129,18 @@ namespace storm {
                 std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
                 auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables);
                 variablesToAbstract.insert(player2Variables.begin(), player2Variables.end());
-                auto probBranchingVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
-                variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end());
+                auto auxVariables = abstractionInformation.getAuxVariableSet(1, abstractionInformation.getAuxVariableCount());
+                variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
+                std::cout << "vars" << std::endl;
+                for (auto const& var : auxVariables) {
+                    std::cout << var.getName() << std::endl;
+                }
                 
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
                 storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStates, transitionRelation);
                 
-                storm::dd::Bdd<DdType> bottomStateTransitions = abstractionInformation.getDdManager().getBddZero();
-                storm::dd::Bdd<DdType> bottomStates = bottomStateTransitions;
-                if (addedAllGuards) {
-                    bottomStateTransitions = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables);
-                    
-                    // If there are transitions to the bottom states, add them and register the new states as well.
-                    transitionRelation |= bottomStateTransitions;
-                }
-                
-                // Determine the bottom states.
-                if (addedAllGuards) {
-                    bottomStates = abstractionInformation.getDdManager().getBddZero();
-                } else {
-                    bottomStateAbstractor.constrain(reachableStates);
-                    bottomStates = bottomStateAbstractor.getAbstractStates();
-                }
-                
                 // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states,
                 // as the bottom states are not contained in the reachable states.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());
@@ -163,15 +152,22 @@ namespace storm {
                     deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd<ValueType>();
                 }
 
+                // Compute bottom states and the appropriate transitions if necessary.
+                BottomStateResult<DdType> bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero());
+                if (!addedAllGuards) {
+                    bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables);
+                }
+                
                 // Construct the transition matrix by cutting away the transitions of unreachable states.
-                storm::dd::Add<DdType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>() * commandUpdateProbabilitiesAdd + deadlockTransitions;
+                storm::dd::Add<DdType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>() * commandUpdateProbabilitiesAdd + deadlockTransitions;// + bottomStateResult.transitions.template toAdd<ValueType>();
+                transitionMatrix.exportToDot("trans_upd.dot");
             
                 std::set<storm::expressions::Variable> usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables);
                 
                 std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
                 allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
 
-                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.getAuxVariables().begin(), abstractionInformation.getAuxVariables().end()), abstractionInformation.getPredicateToBddMap());
+                return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/abstraction/prism/GameBddResult.cpp

@@ -13,7 +13,9 @@ namespace storm {
             GameBddResult<DdType>::GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables), nextFreePlayer2Index(nextFreePlayer2Index) {
                 // Intentionally left empty.
             }
-            
+         
+            template class GameBddResult<storm::dd::DdType::CUDD>;
+            template class GameBddResult<storm::dd::DdType::Sylvan>;
         }
     }
 }