more work towards closing the refinement loop

Former-commit-id: 1579e73036

src/abstraction/AbstractionInformation.cpp

@@ -119,6 +119,11 @@ namespace storm {
             return predicateBdds[indexIt->second].first;
         }
         
+        template<storm::dd::DdType DdType>
+        bool AbstractionInformation<DdType>::hasPredicate(storm::expressions::Expression const& predicate) const {
+            return predicateToIndexMap.find(predicate) != predicateToIndexMap.end();
+        }
+
         template<storm::dd::DdType DdType>
         std::size_t AbstractionInformation<DdType>::getNumberOfPredicates() const {
             return predicates.size();
@@ -164,16 +169,31 @@ namespace storm {
             return encodeChoice(index, 0, end, player1VariableBdds);
         }
         
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const {
+            return decodeChoice(valuation, 0, end, player1Variables);
+        }
+        
         template<storm::dd::DdType DdType>
         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>
+        uint_fast64_t AbstractionInformation<DdType>::decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const {
+            return decodeChoice(valuation, 0, end, player2Variables);
+        }
+
         template<storm::dd::DdType DdType>
         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>
+        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();
@@ -353,6 +373,18 @@ namespace storm {
             return result;
         }
         
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end, std::vector<storm::expressions::Variable> const& variables) const {
+            uint_fast64_t result = 0;
+            for (uint_fast64_t variableIndex = start; variableIndex < end; ++variableIndex) {
+                result <<= 1;
+                if (valuation.getBooleanValue(variables[variableIndex])) {
+                    result |= 1;
+                }
+            }
+            return result;
+        }
+        
         template class AbstractionInformation<storm::dd::DdType::CUDD>;
         template class AbstractionInformation<storm::dd::DdType::Sylvan>;
     }

src/abstraction/AbstractionInformation.h

@@ -147,6 +147,13 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> getPredicateSourceVariable(storm::expressions::Expression const& predicate) const;
             
+            /*!
+             * Determines whether the given predicate is in the set of known predicates.
+             *
+             * @param predicate The predicate for which to query membership.
+             */
+            bool hasPredicate(storm::expressions::Expression const& predicate) const;
+            
             /*!
              * Retrieves the number of predicates.
              *
@@ -179,6 +186,15 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const;
             
+            /*!
+             * Decodes the player 1 choice in the given valuation.
+             *
+             * @param valuation The valuation to decode.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
+             * @return The decoded player 1 choice.
+             */
+            uint_fast64_t decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const;
+            
             /*!
              * Encodes the given index using the indicated player 2 variables.
              *
@@ -189,7 +205,16 @@ namespace storm {
             storm::dd::Bdd<DdType> encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const;
 
             /*!
-             * Encodes the given index using the indicated probabilistic branching variables.
+             * Decodes the player 2 choice in the given valuation.
+             *
+             * @param valuation The valuation to decode.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
+             * @return The decoded player 2 choice.
+             */
+            uint_fast64_t decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const;
+            
+            /*!
+             * Encodes the given index using the indicated auxiliary variables.
              *
              * @param index The index to encode.
              * @param start The index of the first variable of the range that is used to encode the index.
@@ -198,6 +223,16 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const;
             
+            /*!
+             * Decodes the auxiliary index in the given valuation.
+             *
+             * @param valuation The valuation to decode.
+             * @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 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).
              *
@@ -391,16 +426,27 @@ namespace storm {
              * @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.
+             * @return The BDD encoding the index.
              */
             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;
-                        
+
+            /*!
+             * Decodes the index encoded in the valuation using the given variables.
+             *
+             * @param valuation The valuation to decode.
+             * @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 variables used to encode the index.
+             * @return The encoded index.
+             */
+            uint_fast64_t decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end, std::vector<storm::expressions::Variable> const& variables) const;
+
             // The expression related data.
             
             /// The manager responsible for the expressions of the program and the SMT solvers.
             std::reference_wrapper<storm::expressions::ExpressionManager> expressionManager;
             
             /// A mapping from predicates to their indices in the predicate list.
-            // FIXME: Does this properly store the expressions? What about equality checking?
             std::unordered_map<storm::expressions::Expression, uint64_t> predicateToIndexMap;
             
             /// The current set of predicates used in the abstraction.

src/abstraction/MenuGame.cpp

@@ -26,7 +26,7 @@ namespace storm {
                                             std::set<storm::expressions::Variable> const& player2Variables,
                                             std::set<storm::expressions::Variable> const& allNondeterminismVariables,
                                             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) {
+                                            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), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
             // Intentionally left empty.
         }
         
@@ -61,6 +61,16 @@ namespace storm {
             return bottomStates;
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> const& MenuGame<Type, ValueType>::getExtendedTransitionMatrix() const {
+            return extendedTransitionMatrix;
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        std::set<storm::expressions::Variable> const& MenuGame<Type, ValueType>::getProbabilisticBranchingVariables() const {
+            return probabilisticBranchingVariables;
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         bool MenuGame<Type, ValueType>::hasLabel(std::string const& label) const {
             return false;

src/abstraction/MenuGame.h

@@ -84,9 +84,28 @@ namespace storm {
                  */
                 storm::dd::Bdd<Type> getBottomStates() const;
                 
+                /*!
+                 * Retrieves the transition matrix extended by variables that encode additional information for the
+                 * probabilistic branching.
+                 *
+                 * @reutrn Th extended transition matrix.
+                 */
+                storm::dd::Add<Type, ValueType> const& getExtendedTransitionMatrix() const;
+                
+                /*!
+                 * Retrieves the variables used to encode additional information for the probabilistic branching in the
+                 * extended transition matrix.
+                 *
+                 * @return The probabilistic branching variables.
+                 */
+                std::set<storm::expressions::Variable> const& getProbabilisticBranchingVariables() const;
+                
                 virtual bool hasLabel(std::string const& label) const override;
                 
             private:
+                // The transition relation extended byt the probabilistic branching variables.
+                storm::dd::Add<Type, ValueType> extendedTransitionMatrix;
+                
                 // The meta variables used to probabilistic branching.
                 std::set<storm::expressions::Variable> probabilisticBranchingVariables;
                 

src/abstraction/MenuGameAbstractor.h

@@ -12,6 +12,7 @@ namespace storm {
         public:
             virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() = 0;
             virtual void refine(std::vector<storm::expressions::Expression> const& predicates) = 0;
+            virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) = 0;
         };
         
     }

src/abstraction/prism/AbstractCommand.cpp

@@ -337,6 +337,16 @@ namespace storm {
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::prism::Command const& AbstractCommand<DdType, ValueType>::getConcreteCommand() const {
+                return command.get();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractCommand<DdType, ValueType>::notifyGuardIsPredicate() {
+                guardIsPredicate = true;
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractionInformation<DdType> const& AbstractCommand<DdType, ValueType>::getAbstractionInformation() const {
                 return abstractionInformation.get();

src/abstraction/prism/AbstractCommand.h

@@ -92,6 +92,19 @@ namespace storm {
                  */
                 storm::dd::Add<DdType, ValueType> getCommandUpdateProbabilitiesAdd() const;
                 
+                /*!
+                 * Retrieves the concrete command that is abstracted by this abstract command.
+                 *
+                 * @return The concrete command.
+                 */
+                storm::prism::Command const& getConcreteCommand() const;
+                
+                /*!
+                 * Notifies this abstract command that its guard is now a predicate. This affects the computation of the
+                 * bottom states.
+                 */
+                void notifyGuardIsPredicate();
+                
             private:
                 /*!
                  * Determines the relevant predicates for source as well as successor states wrt. to the given assignments

src/abstraction/prism/AbstractModule.cpp

@@ -72,6 +72,16 @@ namespace storm {
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<AbstractCommand<DdType, ValueType>> const& AbstractModule<DdType, ValueType>::getCommands() const {
+                return commands;
+            }
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<AbstractCommand<DdType, ValueType>>& AbstractModule<DdType, ValueType>::getCommands() {
+                return commands;
+            }
+
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractionInformation<DdType> const& AbstractModule<DdType, ValueType>::getAbstractionInformation() const {
                 return abstractionInformation.get();

src/abstraction/prism/AbstractModule.h

@@ -73,6 +73,20 @@ namespace storm {
                  */
                 storm::dd::Add<DdType, ValueType> getCommandUpdateProbabilitiesAdd() const;
                 
+                /*!
+                 * Retrieves the abstract commands of this abstract module.
+                 *
+                 * @return The abstract commands.
+                 */
+                std::vector<AbstractCommand<DdType, ValueType>> const& getCommands() const;
+
+                /*!
+                 * Retrieves the abstract commands of this abstract module.
+                 *
+                 * @return The abstract commands.
+                 */
+                std::vector<AbstractCommand<DdType, ValueType>>& getCommands();
+
             private:
                 /*!
                  * Retrieves the abstraction information.

src/abstraction/prism/AbstractProgram.cpp

@@ -9,6 +9,7 @@
 
 #include "src/models/symbolic/StandardRewardModel.h"
 
+#include "src/utility/dd.h"
 #include "src/utility/macros.h"
 #include "src/utility/solver.h"
 #include "src/exceptions/WrongFormatException.h"
@@ -108,6 +109,33 @@ namespace storm {
                 currentGame = buildGame();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractProgram<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
+//                std::cout << "refining in program!" << std::endl;
+//                lowerChoice.template toAdd<ValueType>().exportToDot("lchoice.dot");
+//                upperChoice.template toAdd<ValueType>().exportToDot("uchoice.dot");
+//                player1Choice.template toAdd<ValueType>().exportToDot("pl1_choice.dot");
+//                pivotState.template toAdd<ValueType>().exportToDot("pivotstate.dot");
+                
+                // Decode the index of the command chosen by player 1.
+                storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>();
+                auto pl1It = player1ChoiceAsAdd.begin();
+                uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount());
+                
+                bool bottomSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero();
+                if (bottomSuccessor) {
+                    storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
+                    abstractCommand.notifyGuardIsPredicate();
+                    storm::expressions::Expression newPredicate = abstractCommand.getConcreteCommand().getGuardExpression();
+                    STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
+                    this->refine({newPredicate});
+                } else {
+                    exit(-1);
+                }
+                
+                storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = lowerChoice.template toAdd<ValueType>();
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             MenuGame<DdType, ValueType> AbstractProgram<DdType, ValueType>::getAbstractGame() {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
@@ -135,7 +163,7 @@ namespace storm {
                 // 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> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
                 
                 // 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.
@@ -164,6 +192,7 @@ namespace storm {
                     transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd<ValueType>();
                     transitionMatrix += bottomStateResult.transitions.template toAdd<ValueType>();
                     reachableStates &= abstractionInformation.getBottomStateBdd(true, true);
+                    initialStates &= abstractionInformation.getBottomStateBdd(true, true);
                     reachableStates |= bottomStateResult.states;
                 }
             
@@ -183,25 +212,7 @@ namespace storm {
                 
                 return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, hasBottomStates ? abstractionInformation.getExtendedSourceSuccessorVariablePairs() : 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>
-            storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation) {
-                storm::dd::Bdd<DdType> frontier = initialStates;
-
-                storm::dd::Bdd<DdType> reachableStates = initialStates;
-                uint_fast64_t reachabilityIteration = 0;
-                while (!frontier.isZero()) {
-                    ++reachabilityIteration;
-                    frontier = frontier.andExists(transitionRelation, abstractionInformation.getSourceVariables());
-                    frontier = frontier.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs());
-                    frontier &= !reachableStates;
-                    reachableStates |= frontier;
-                    STORM_LOG_TRACE("Iteration " << reachabilityIteration << " of reachability analysis.");
-                }
-                
-                return reachableStates;
-            }
-            
+                        
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename) const {
                 std::ofstream out(filename);
@@ -241,13 +252,7 @@ namespace storm {
                             stateName << "0";
                         }
                     }
-                    uint_fast64_t index = 0;
-                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
-                        index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
-                            index |= 1;
-                        }
-                    }
+                    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;
@@ -265,21 +270,9 @@ namespace storm {
                             stateName << "0";
                         }
                     }
-                    uint_fast64_t index = 0;
-                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
-                        index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
-                            index |= 1;
-                        }
-                    }
+                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
                     stateName << "_" << index;
-                    index = 0;
-                    for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) {
-                        index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) {
-                            index |= 1;
-                        }
-                    }
+                    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;
@@ -302,20 +295,8 @@ namespace storm {
                             successorStateName << "0";
                         }
                     }
-                    uint_fast64_t pl1Index = 0;
-                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
-                        pl1Index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
-                            pl1Index |= 1;
-                        }
-                    }
-                    uint_fast64_t pl2Index = 0;
-                    for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) {
-                        pl2Index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) {
-                            pl2Index |= 1;
-                        }
-                    }
+                    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;
                 }
                 

src/abstraction/prism/AbstractProgram.h

@@ -75,23 +75,24 @@ namespace storm {
                 void refine(std::vector<storm::expressions::Expression> const& predicates);
                 
                 /*!
-                 * Exports the current state of the abstraction in the dot format to the given file.
+                 * Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that
+                 * the two provided choices are not possible from the same pivot state using the given player 1 choice.
                  *
-                 * @param filename The name of the file to which to write the dot output.
+                 * @param pivotState The pivot state on which to base the refinement.
+                 * @param player1Choice The player 1 choice that needs to be refined.
+                 * @param lowerChoice The first of the two choices on which to base the refinement.
+                 * @param upperChoice The first of the two choices on which to base the refinement.
                  */
-                void exportToDot(std::string const& filename) const;
+                void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice);
                 
-            private:
                 /*!
-                 * Computes the reachable states of the transition relation.
+                 * Exports the current state of the abstraction in the dot format to the given file.
                  *
-                 * @param initialStates The BDD representing the initial states of the model.
-                 * @param transitionRelation The BDD representing the transition relation that does only contain state
-                 * and successor variables.
-                 * @return The BDD representing the reachable states.
+                 * @param filename The name of the file to which to write the dot output.
                  */
-                storm::dd::Bdd<DdType> getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation);
+                void exportToDot(std::string const& filename) const;
                 
+            private:                
                 /*!
                  * Builds the stochastic game representing the abstraction of the program.
                  *

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -24,6 +24,11 @@ namespace storm {
                 abstractProgram.refine(predicates);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
+                abstractProgram.refine(pivotState, player1Choice, lowerChoice, upperChoice);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename) const {
                 abstractProgram.exportToDot(filename);

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -15,6 +15,7 @@ namespace storm {
                 
                 virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
+                virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) override;
 
                 void exportToDot(std::string const& filename) const;
                 

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -13,6 +13,7 @@
 
 #include "src/logic/FragmentSpecification.h"
 
+#include "src/utility/dd.h"
 #include "src/utility/macros.h"
 
 #include "src/exceptions/NotSupportedException.h"
@@ -92,16 +93,68 @@ namespace storm {
             }
         }
         
+        template<storm::dd::DdType Type>
+        storm::dd::Bdd<Type> pickPivotState(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Bdd<Type> const& pivotStates) {
+            // Perform a BFS and pick the first pivot state we encounter.
+            storm::dd::Bdd<Type> pivotState;
+            storm::dd::Bdd<Type> frontier = initialStates;
+            storm::dd::Bdd<Type> frontierPivotStates = frontier && pivotStates;
+
+            bool foundPivotState = !frontierPivotStates.isZero();
+            if (foundPivotState) {
+                pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
+            } else {
+                while (!foundPivotState) {
+                    frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables);
+                    frontierPivotStates = frontier && pivotStates;
+                
+                    if (!frontierPivotStates.isZero()) {
+                        pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
+                        foundPivotState = true;
+                    }
+                }
+            }
+            
+            return pivotState;
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
-        void refineAfterQualitativeCheck(storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
+        void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
+            storm::dd::Bdd<Type> transitionsInIntersection = transitionMatrixBdd && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy();
+            
             // First, we have to find the pivot state candidates. Start by constructing the reachable fragment of the
             // state space *under both* strategy pairs.
-            storm::dd::Bdd<Type> pivotStateCandidates = transitionMatrixBdd.existsAbstract(game.getColumnVariables());
-            pivotStateCandidates &= prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy();
-            pivotStateCandidates = pivotStateCandidates.existsAbstract(game.getNondeterminismVariables());
+            storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), transitionsInIntersection.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables());
+            
+            // Then constrain this set by requiring that the two stratey pairs resolve the nondeterminism differently.
+            pivotStates &= (prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy()).exclusiveOr(prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables());
+            STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates.");
             
+            // Now that we have the pivot state candidates, we need to pick one.
+            storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables(), pivotStates);
             
-            std::cout << "found pivot state candidates" << std::endl;
+            // Compute the lower and the upper choice for the pivot state.
+            std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
+            variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
+            storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.min.first.getPlayer1Strategy();
+            storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+            storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+                        
+            bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
+            if (lowerChoicesDifferent) {
+                abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
+            }
+            
+            storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy();
+            storm::dd::Bdd<Type> upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+            storm::dd::Bdd<Type> upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+            upperChoice1.template toAdd<ValueType>().exportToDot("uchoice1.dot");
+            upperChoice2.template toAdd<ValueType>().exportToDot("uchoice2.dot");
+
+            bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
+            if (upperChoicesDifferent) {
+                abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
+            }
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -155,7 +208,7 @@ namespace storm {
                 
                 // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
                 // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
-                refineAfterQualitativeCheck(game, prob01, transitionMatrixBdd);
+                refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd);
             }
             
             
@@ -187,6 +240,7 @@ namespace storm {
             // Now compute the states with probability 0/1 when player 2 maximizes.
             storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false, false);
             storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
+            prob1Max.getPlayer1Strategy().template toAdd<ValueType>().exportToDot("prob1maxstrat.dot");
             
             STORM_LOG_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy.");
             STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy.");

src/utility/dd.cpp

@@ -27,7 +27,6 @@ namespace storm {
                         changed = true;
                     }
                     
-                    
                     reachableStates |= newReachableStates;
 
                     ++iteration;

src/utility/graph.cpp

@@ -989,7 +989,6 @@ namespace storm {
                 // Create two sets of states. Those states for which we definitely know that their probability is 1 and
                 // those states that potentially have a probability of 1.
                 storm::dd::Bdd<Type> maybeStates = model.getReachableStates();
-                storm::dd::Bdd<Type> solution = psiStates;
 
                 // A flag that governs whether strategies are produced in the current iteration.
                 bool produceStrategiesInIteration = false;
@@ -1012,6 +1011,7 @@ namespace storm {
                         consideredPlayer2States = model.getManager().getBddZero();
                     }
                     
+                    storm::dd::Bdd<Type> solution = psiStates;
                     while (!solutionStatesDone) {
                         // Start by computing the transitions that have only maybe states as successors. Note that at
                         // this point, there may be illegal transitions.
@@ -1024,7 +1024,7 @@ namespace storm {
                         // The valid distributions are then those that emanate from phi states, stay completely in the
                         // maybe states and have at least one successor with probability 1.
                         storm::dd::Bdd<Type> valid = phiStates && distributionsStayingInMaybe && distributionsWithProb1Successor;
-                        
+
                         // Depending on the strategy of player 2, we need to check whether all choices are valid or
                         // there exists a valid choice.
                         if (player2Strategy == OptimizationDirection::Minimize) {
@@ -1088,11 +1088,13 @@ namespace storm {
                     ++maybeStateIterations;
                 }
                 
+                // From now on, the solution is stored in maybeStates (as it coincides with the previous solution).
+                
                 // If we were asked to produce strategies that do not need to pick a certain successor but are
                 // 'arbitrary', do so now.
                 bool strategiesToCompute = (producePlayer1Strategy && !player1StrategyBdd) || (producePlayer2Strategy && !player2StrategyBdd);
                 if (strategiesToCompute) {
-                    storm::dd::Bdd<Type> relevantStates = (transitionMatrix && solution).existsAbstract(model.getColumnVariables());
+                    storm::dd::Bdd<Type> relevantStates = (transitionMatrix && maybeStates).existsAbstract(model.getColumnVariables());
                     if (producePlayer2Strategy && !player2StrategyBdd) {
                         player2StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer2Variables());
                     }
@@ -1102,7 +1104,7 @@ namespace storm {
                     }
                 }
                 
-                return GameProb01Result<Type>(solution, player1StrategyBdd, player2StrategyBdd);
+                return GameProb01Result<Type>(maybeStates, player1StrategyBdd, player2StrategyBdd);
             }
             
             template <typename T>