fix for decomposition

src/storm/abstraction/AbstractionInformation.cpp

@@ -64,6 +64,7 @@ namespace storm {
             sourceVariables.insert(newMetaVariable.first);
             successorVariables.insert(newMetaVariable.second);
             sourcePredicateVariables.insert(newMetaVariable.first);
+            successorPredicateVariables.insert(newMetaVariable.second);
             orderedSourcePredicateVariables.push_back(newMetaVariable.first);
             orderedSuccessorPredicateVariables.push_back(newMetaVariable.second);
             ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex;
@@ -223,16 +224,6 @@ namespace storm {
         uint_fast64_t AbstractionInformation<DdType>::decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const {
             return decodeChoice(valuation, start, end, auxVariables);
         }
-
-        template<storm::dd::DdType DdType>
-        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 = start; index < end; ++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 {
@@ -283,7 +274,12 @@ namespace storm {
         std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getSourcePredicateVariables() const {
             return sourcePredicateVariables;
         }
-        
+
+        template<storm::dd::DdType DdType>
+        std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getSuccessorPredicateVariables() const {
+            return successorPredicateVariables;
+        }
+
         template<storm::dd::DdType DdType>
         std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getOrderedSourcePredicateVariables() const {
             return orderedSourcePredicateVariables;

src/storm/abstraction/AbstractionInformation.h

@@ -241,16 +241,6 @@ namespace storm {
              * @return The decoded auxiliary index.
              */
             uint_fast64_t decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) 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.
@@ -347,7 +337,14 @@ namespace storm {
              * @return All source predicate meta variables.
              */
             std::set<storm::expressions::Variable> const& getSourcePredicateVariables() const;
-            
+
+            /*!
+             * Retrieves the set of successor predicate meta variables.
+             *
+             * @return All successor predicate meta variables.
+             */
+            std::set<storm::expressions::Variable> const& getSuccessorPredicateVariables() const;
+
             /*!
              * Retrieves a BDD representing the identities of all predicates.
              *
@@ -570,7 +567,10 @@ namespace storm {
 
             /// The set of all source predicate variables.
             std::set<storm::expressions::Variable> sourcePredicateVariables;
-            
+
+            /// The set of all successor predicate variables.
+            std::set<storm::expressions::Variable> successorPredicateVariables;
+
             /// An ordered collection of the source variables.
             std::vector<storm::expressions::Variable> orderedSourcePredicateVariables;
 

src/storm/abstraction/MenuGameAbstractor.cpp

@@ -0,0 +1,140 @@
+#include "storm/abstraction/MenuGameAbstractor.h"
+
+#include "storm/abstraction/AbstractionInformation.h"
+
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/Bdd.h"
+#include "storm/utility/dd.h"
+
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <typename ValueType>
+        std::string getStateName(std::pair<storm::expressions::SimpleValuation, ValueType> const& stateValue, std::set<storm::expressions::Variable> const& locationVariables, std::set<storm::expressions::Variable> const& predicateVariables, storm::expressions::Variable const& bottomVariable) {
+            std::stringstream stateName;
+
+            if (!locationVariables.empty()) {
+                stateName << "loc";
+            }
+
+            for (auto const& variable : locationVariables) {
+                stateName << stateValue.first.getIntegerValue(variable);
+            }
+            
+            if (!locationVariables.empty() && !predicateVariables.empty()) {
+                stateName << "_";
+            }
+            
+            for (auto const& variable : predicateVariables) {
+                if (stateValue.first.getBooleanValue(variable)) {
+                    stateName << "1";
+                } else {
+                    stateName << "0";
+                }
+            }
+            
+            if (stateValue.first.getBooleanValue(bottomVariable)) {
+                stateName << "bot";
+            }
+            return stateName.str();
+        }
+        
+        template <storm::dd::DdType DdType, typename ValueType>
+        void MenuGameAbstractor<DdType, ValueType>::exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
+
+            std::ofstream out(filename);
+            AbstractionInformation<DdType> const& abstractionInformation = this->getAbstractionInformation();
+            
+            storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame.getTransitionMatrix();
+            storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame.getNondeterminismVariables());
+            storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame.getInitialStates(), filteredTransitionsBdd, currentGame.getRowVariables(), currentGame.getColumnVariables());
+            filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
+            
+            // Determine all initial states so we can color them blue.
+            std::unordered_set<std::string> initialStates;
+            storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame.getInitialStates().template toAdd<ValueType>();
+            for (auto stateValue : initialStatesAsAdd) {
+                initialStates.insert(getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true)));
+            }
+            
+            // Determine all highlight states so we can color them red.
+            std::unordered_set<std::string> highlightStates;
+            storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
+            for (auto stateValue : highlightStatesAdd) {
+                highlightStates.insert(getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true)));
+            }
+            
+            out << "digraph game {" << std::endl;
+            
+            // Create the player 1 nodes.
+            storm::dd::Add<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
+            for (auto stateValue : statesAsAdd) {
+                out << "\tpl1_";
+                std::string stateName = getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true));
+                out << stateName;
+                out << " [ label=\"";
+                if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) {
+                    out << "*\", margin=0, width=0, height=0, shape=\"none\"";
+                } else {
+                    out << stateName << "\", margin=0, width=0, height=0, shape=\"oval\"";
+                }
+                bool isInitial = initialStates.find(stateName) != initialStates.end();
+                bool isHighlight = highlightStates.find(stateName) != highlightStates.end();
+                if (isInitial && isHighlight) {
+                    out << ", style=\"filled\", fillcolor=\"yellow\"";
+                } else if (isInitial) {
+                    out << ", style=\"filled\", fillcolor=\"blue\"";
+                } else if (isHighlight) {
+                    out << ", style=\"filled\", fillcolor=\"red\"";
+                }
+                out << " ];" << std::endl;
+            }
+            
+            // Create the nodes of the second player.
+            storm::dd::Add<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame.getColumnVariables()).existsAbstract(currentGame.getPlayer2Variables()).template toAdd<ValueType>();
+            for (auto stateValue : player2States) {
+                out << "\tpl2_";
+                std::string stateName = getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true));
+                uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                out << stateName << "_" << index;
+                out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl;
+                out << "\tpl1_" << stateName << " -> " << "pl2_" << stateName << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
+            }
+            
+            // Create the nodes of the probabilistic player.
+            storm::dd::Add<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame.getColumnVariables()).template toAdd<ValueType>();
+            for (auto stateValue : playerPStates) {
+                out << "\tplp_";
+                std::stringstream stateNameStream;
+                stateNameStream << getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true));
+                uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                stateNameStream << "_" << index;
+                std::string stateName = stateNameStream.str();
+                index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame.getPlayer2Variables().size());
+                out << stateName << "_" << index;
+                out << " [ shape=\"point\", label=\"\" ];" << std::endl;
+                out << "\tpl2_" << stateName << " -> " << "plp_" << stateName << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
+            }
+            
+            for (auto stateValue : filteredTransitions) {
+                std::string sourceStateName = getStateName(stateValue, abstractionInformation.getSourceLocationVariables(), abstractionInformation.getSourcePredicateVariables(), abstractionInformation.getBottomStateVariable(true));
+                std::string successorStateName = getStateName(stateValue, abstractionInformation.getSuccessorLocationVariables(), abstractionInformation.getSuccessorPredicateVariables(), abstractionInformation.getBottomStateVariable(false));
+                uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame.getPlayer2Variables().size());
+                out << "\tplp_" << sourceStateName << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName << " [ label=\"" << stateValue.second << "\"];" << std::endl;
+            }
+            
+            out << "}" << std::endl;
+        }
+        
+        template class MenuGameAbstractor<storm::dd::DdType::CUDD, double>;
+        template class MenuGameAbstractor<storm::dd::DdType::Sylvan, double>;
+        
+#ifdef STORM_HAVE_CARL
+        template class MenuGameAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#endif
+    }
+}

src/storm/abstraction/MenuGameAbstractor.h

@@ -42,9 +42,12 @@ namespace storm {
             
             /// Methods to refine the abstraction.
             virtual void refine(RefinementCommand const& command) = 0;
-            
+
             /// Exports a representation of the current abstraction state in the dot format.
-            virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const = 0;
+            virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const = 0;
+
+        protected:
+            void exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const;
         };
         
     }

src/storm/abstraction/MenuGameRefiner.cpp

@@ -438,6 +438,7 @@ namespace storm {
             
             std::map<storm::expressions::Variable, storm::expressions::Variable> oldToNewVariables;
             for (auto const& variable : oldVariables) {
+                std::cout << "got old variable " << variable.getName() << std::endl;
                 oldToNewVariables[variable] = expressionManager.getVariable(variable.getName());
             }
             std::map<storm::expressions::Variable, storm::expressions::Expression> lastSubstitution;
@@ -470,6 +471,7 @@ namespace storm {
                 // Retrieve the variable updates that the predecessor needs to perform to get to the current state.
                 auto variableUpdates = abstractor.get().getVariableUpdates(std::get<1>(decodedPredecessor), std::get<2>(decodedPredecessor));
                 for (auto const& update : variableUpdates) {
+                    std::cout << "looking up old variable " << update.first.getName() << std::endl;
                     storm::expressions::Variable newVariable = oldToNewVariables.at(update.first);
                     if (update.second.hasBooleanType()) {
                         predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(oldToNewVariables.at(update.first)), update.second.changeManager(expressionManager).substitute(substitution)));

src/storm/abstraction/jani/AutomatonAbstractor.cpp

@@ -69,7 +69,7 @@ namespace storm {
                 // DDs use the same amount DD variable encoding the choices of player 2.
                 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
                 for (auto const& edgeDd : edgeDdsAndUsedOptionVariableCounts) {
-                    result |= edgeDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(edgeDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
+                    result |= edgeDd.bdd && this->getAbstractionInformation().encodePlayer2Choice(1, edgeDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
                 }
                 return GameBddResult<DdType>(result, maximalNumberOfUsedOptionVariables);
             }

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -81,7 +81,7 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void EdgeAbstractor<DdType, ValueType>::recomputeCachedBddWithDecomposition() {
-                STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard() << " using the decomposition.");
+                STORM_LOG_TRACE("Recomputing BDD for edge with id " << edgeId << " and guard " << edge.get().getGuard() << " using the decomposition.");
                 auto start = std::chrono::high_resolution_clock::now();
                 
                 // compute a decomposition of the command
@@ -369,7 +369,7 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void EdgeAbstractor<DdType, ValueType>::recomputeCachedBddWithoutDecomposition() {
-                STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard());
+                STORM_LOG_TRACE("Recomputing BDD for edge with id " << edgeId << " and guard " << edge.get().getGuard());
                 auto start = std::chrono::high_resolution_clock::now();
                 
                 // Create a mapping from source state DDs to their distributions.

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -32,7 +32,7 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
+            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression({model.getAutomaton(0)})}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
                 
                 // 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.
@@ -125,7 +125,7 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::expressions::Expression JaniMenuGameAbstractor<DdType, ValueType>::getInitialExpression() const {
-                return model.get().getInitialStatesExpression();
+                return model.get().getInitialStatesExpression({model.get().getAutomaton(0)});
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -199,139 +199,8 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void JaniMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
-                std::ofstream out(filename);
-                
-                storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame->getTransitionMatrix();
-                storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables());
-                storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables());
-                filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
-                
-                // Determine all initial states so we can color them blue.
-                std::unordered_set<std::string> initialStates;
-                storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame->getInitialStates().template toAdd<ValueType>();
-                for (auto stateValue : initialStatesAsAdd) {
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    initialStates.insert(stateName.str());
-                }
-                
-                // Determine all highlight states so we can color them red.
-                std::unordered_set<std::string> highlightStates;
-                storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
-                for (auto stateValue : highlightStatesAdd) {
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    highlightStates.insert(stateName.str());
-                }
-                
-                out << "digraph game {" << std::endl;
-                
-                // Create the player 1 nodes.
-                storm::dd::Add<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
-                for (auto stateValue : statesAsAdd) {
-                    out << "\tpl1_";
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    std::string stateNameAsString = stateName.str();
-                    out << stateNameAsString;
-                    out << " [ label=\"";
-                    if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) {
-                        out << "*\", margin=0, width=0, height=0, shape=\"none\"";
-                    } else {
-                        out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\"";
-                    }
-                    bool isInitial = initialStates.find(stateNameAsString) != initialStates.end();
-                    bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end();
-                    if (isInitial && isHighlight) {
-                        out << ", style=\"filled\", fillcolor=\"yellow\"";
-                    } else if (isInitial) {
-                        out << ", style=\"filled\", fillcolor=\"blue\"";
-                    } else if (isHighlight) {
-                        out << ", style=\"filled\", fillcolor=\"red\"";
-                    }
-                    out << " ];" << std::endl;
-                }
-                
-                // Create the nodes of the second player.
-                storm::dd::Add<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
-                for (auto stateValue : player2States) {
-                    out << "\tpl2_";
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
-                    out << stateName.str() << "_" << index;
-                    out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl;
-                    out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
-                }
-                
-                // Create the nodes of the probabilistic player.
-                storm::dd::Add<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
-                for (auto stateValue : playerPStates) {
-                    out << "\tplp_";
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
-                    stateName << "_" << index;
-                    index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
-                    out << stateName.str() << "_" << index;
-                    out << " [ shape=\"point\", label=\"\" ];" << std::endl;
-                    out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
-                }
-                
-                for (auto stateValue : filteredTransitions) {
-                    std::stringstream sourceStateName;
-                    std::stringstream successorStateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            sourceStateName << "1";
-                        } else {
-                            sourceStateName << "0";
-                        }
-                    }
-                    for (auto const& var : currentGame->getColumnVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            successorStateName << "1";
-                        } else {
-                            successorStateName << "0";
-                        }
-                    }
-                    uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
-                    uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
-                    out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl;
-                }
-                
-                out << "}" << std::endl;
+            void JaniMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const {
+                this->exportToDot(*currentGame, filename, highlightStates, filter);
             }
             
             // Explicitly instantiate the class.

src/storm/abstraction/jani/JaniMenuGameAbstractor.h

@@ -109,6 +109,9 @@ namespace storm {
                  */
                 void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
                 
+            protected:
+                using MenuGameAbstractor<DdType, ValueType>::exportToDot;
+                
             private:                
                 /*!
                  * Builds the stochastic game representing the abstraction of the program.

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -64,7 +64,7 @@ namespace storm {
                 // DDs use the same amount DD variable encoding the choices of player 2.
                 storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
                 for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) {
-                    result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
+                    result |= commandDd.bdd && this->getAbstractionInformation().encodePlayer2Choice(1, commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
                 }
                 return GameBddResult<DdType>(result, maximalNumberOfUsedOptionVariables);
             }

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -199,139 +199,8 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
-                std::ofstream out(filename);
-                
-                storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame->getTransitionMatrix();
-                storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables());
-                storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables());
-                filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
-                
-                // Determine all initial states so we can color them blue.
-                std::unordered_set<std::string> initialStates;
-                storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame->getInitialStates().template toAdd<ValueType>();
-                for (auto stateValue : initialStatesAsAdd) {
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    initialStates.insert(stateName.str());
-                }
-                
-                // Determine all highlight states so we can color them red.
-                std::unordered_set<std::string> highlightStates;
-                storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
-                for (auto stateValue : highlightStatesAdd) {
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    highlightStates.insert(stateName.str());
-                }
-                
-                out << "digraph game {" << std::endl;
-                
-                // Create the player 1 nodes.
-                storm::dd::Add<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
-                for (auto stateValue : statesAsAdd) {
-                    out << "\tpl1_";
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    std::string stateNameAsString = stateName.str();
-                    out << stateNameAsString;
-                    out << " [ label=\"";
-                    if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) {
-                        out << "*\", margin=0, width=0, height=0, shape=\"none\"";
-                    } else {
-                        out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\"";
-                    }
-                    bool isInitial = initialStates.find(stateNameAsString) != initialStates.end();
-                    bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end();
-                    if (isInitial && isHighlight) {
-                        out << ", style=\"filled\", fillcolor=\"yellow\"";
-                    } else if (isInitial) {
-                        out << ", style=\"filled\", fillcolor=\"blue\"";
-                    } else if (isHighlight) {
-                        out << ", style=\"filled\", fillcolor=\"red\"";
-                    }
-                    out << " ];" << std::endl;
-                }
-                
-                // Create the nodes of the second player.
-                storm::dd::Add<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
-                for (auto stateValue : player2States) {
-                    out << "\tpl2_";
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
-                    out << stateName.str() << "_" << index;
-                    out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl;
-                    out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
-                }
-                
-                // Create the nodes of the probabilistic player.
-                storm::dd::Add<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
-                for (auto stateValue : playerPStates) {
-                    out << "\tplp_";
-                    std::stringstream stateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            stateName << "1";
-                        } else {
-                            stateName << "0";
-                        }
-                    }
-                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
-                    stateName << "_" << index;
-                    index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
-                    out << stateName.str() << "_" << index;
-                    out << " [ shape=\"point\", label=\"\" ];" << std::endl;
-                    out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
-                }
-                
-                for (auto stateValue : filteredTransitions) {
-                    std::stringstream sourceStateName;
-                    std::stringstream successorStateName;
-                    for (auto const& var : currentGame->getRowVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            sourceStateName << "1";
-                        } else {
-                            sourceStateName << "0";
-                        }
-                    }
-                    for (auto const& var : currentGame->getColumnVariables()) {
-                        if (stateValue.first.getBooleanValue(var)) {
-                            successorStateName << "1";
-                        } else {
-                            successorStateName << "0";
-                        }
-                    }
-                    uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
-                    uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
-                    out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl;
-                }
-                
-                out << "}" << std::endl;
+            void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const {
+                this->exportToDot(*currentGame, filename, highlightStates, filter);
             }
             
             // Explicitly instantiate the class.

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -107,9 +107,12 @@ namespace storm {
                  * @param highlightStates A BDD characterizing states that will be highlighted.
                  * @param filter A filter that is applied to select which part of the game to export.
                  */
-                void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
+                virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
+
+            protected:
+                using MenuGameAbstractor<DdType, ValueType>::exportToDot;
                 
-            private:                
+            private:
                 /*!
                  * Builds the stochastic game representing the abstraction of the program.
                  *

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -368,7 +368,7 @@ namespace storm {
                 }
                 
                 // #ifdef LOCAL_DEBUG
-                // abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
+                abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
                 // #endif
                 
                 // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).

src/storm/utility/graph.cpp

@@ -1008,7 +1008,7 @@ namespace storm {
                 boost::optional<storm::dd::Bdd<Type>> consideredPlayer1States;
                 boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
                 boost::optional<storm::dd::Bdd<Type>> consideredPlayer2States;
-
+                
                 bool maybeStatesDone = false;
                 uint_fast64_t maybeStateIterations = 0;
                 while (!maybeStatesDone || produceStrategiesInIteration) {
@@ -1032,7 +1032,6 @@ namespace storm {
                     while (!solutionStatesDone) {
                         // Start by computing the transitions that have only maybe states as successors. Note that at
                         // this point, there may be illegal transitions.
-                        // FIXME: use getIllegalSuccessorMask instead of !transitionMatrix?
                         storm::dd::Bdd<Type> distributionsStayingInMaybe = (!transitionMatrix || maybePlayer1States.swapVariables(model.getRowColumnMetaVariablePairs())).universalAbstract(model.getColumnVariables());
                         
                         // Then, determine all distributions that have at least one successor in the states that have