some fixes and more refactoring

src/storm/abstraction/MenuGameRefiner.cpp

@@ -0,0 +1,22 @@
+#include "storm/abstraction/MenuGameRefiner.h"
+
+#include "storm/abstraction/MenuGameAbstractor.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor) : abstractor(abstractor) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        void MenuGameRefiner<Type, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) const {
+            abstractor.get().refine(predicates);
+        }
+        
+        template class MenuGameRefiner<storm::dd::DdType::CUDD, double>;
+        template class MenuGameRefiner<storm::dd::DdType::Sylvan, double>;
+        
+    }
+}

src/storm/abstraction/MenuGameRefiner.h

@@ -0,0 +1,37 @@
+#pragma once
+
+#include <functional>
+#include <vector>
+
+#include "storm/storage/expressions/Expression.h"
+
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+    namespace abstraction {
+
+        template <storm::dd::DdType DdType, typename ValueType>
+        class MenuGameAbstractor;
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        class MenuGameRefiner {
+        public:
+            /*!
+             * Creates a refiner for the provided abstractor.
+             */
+            MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor);
+            
+            /*!
+             * Refines the abstractor with the given set of predicates.
+             */
+            void refine(std::vector<storm::expressions::Expression> const& predicates) const;
+            
+            
+            
+        private:
+            /// The underlying abstractor to refine.
+            std::reference_wrapper<MenuGameAbstractor<Type, ValueType>> abstractor;
+        };
+        
+    }
+}

src/storm/abstraction/StateSetAbstractor.cpp

@@ -14,7 +14,7 @@ namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType DdType, typename ValueType>
-        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) {
+        StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) {
             
             // Assert all state predicates.
             for (auto const& predicate : statePredicates) {
@@ -101,8 +101,7 @@ namespace storm {
             STORM_LOG_TRACE("Recomputing BDD for state set abstraction.");
             
             storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
-            uint_fast64_t modelCounter = 0;
+            smtSolver->allSat(decisionVariables, [&result,this] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } );
-            smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; return true; } );
             
             cachedBdd = result;
         }

src/storm/abstraction/prism/AbstractCommand.cpp

@@ -23,7 +23,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), abstractGuard(abstractionInformation.getDdManager().getBddZero()), 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), decisionVariables(), guardIsPredicate(guardIsPredicate), forceRecomputation(true), 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());
@@ -36,17 +36,10 @@ namespace storm {
                 
                 // Assert the guard of the command.
                 smtSolver->add(command.getGuardExpression());
-
-                // Refine the command based on all initial predicates.
-                std::vector<uint_fast64_t> allPredicateIndices(abstractionInformation.getNumberOfPredicates());
-                for (uint_fast64_t index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
-                    allPredicateIndices[index] = index;
-                }
-                this->refine(allPredicateIndices, true);
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates, bool forceRecomputation) {
+            void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
                 // Add all predicates to the variable partition.
                 for (auto predicateIndex : predicates) {
                     localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
@@ -69,6 +62,9 @@ namespace storm {
                     
                     // Finally recompute the cached BDD.
                     this->recomputeCachedBdd();
+                    
+                    // Disable forcing recomputation until it is set again.
+                    forceRecomputation = false;
                 }
                 
                 // Refine bottom state abstractor. Note that this does not trigger a recomputation yet.
@@ -322,6 +318,7 @@ namespace storm {
 
                 // If the guard of this command is a predicate, there are not bottom states/transitions.
                 if (guardIsPredicate) {
+                    STORM_LOG_TRACE("Guard is predicate, no bottom state transitions for this command.");
                     return result;
                 }
                 
@@ -329,7 +326,7 @@ namespace storm {
                 // 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() && this->getAbstractionInformation().getBottomStateBdd(false, false);
                 

src/storm/abstraction/prism/AbstractCommand.h

@@ -65,9 +65,8 @@ namespace storm {
                  * Refines the abstract command with the given predicates.
                  *
                  * @param predicates The new predicates.
-                 * @param forceRecomputation If set, the BDD is recomputed even if the relevant predicates have not changed.
                  */
-                void refine(std::vector<uint_fast64_t> const& predicates, bool forceRecomputation = false);
+                void refine(std::vector<uint_fast64_t> const& predicates);
                 
                 /*!
                  * Computes the abstraction of the command wrt. to the current set of predicates.
@@ -227,6 +226,9 @@ namespace storm {
                 // is no need to compute bottom states.
                 bool guardIsPredicate;
                 
+                // A flag remembering whether we need to force recomputation of the BDD.
+                bool forceRecomputation;
+                
                 // 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;

src/storm/abstraction/prism/AbstractProgram.cpp

@@ -29,7 +29,6 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
-                                                                std::vector<storm::expressions::Expression> const& initialPredicates,
                                                                 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory,
                                                                 bool addAllGuards, bool splitPredicates)
             : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), splitPredicates(splitPredicates), splitter(), equivalenceChecker(smtSolverFactory->create(abstractionInformation.getExpressionManager()), abstractionInformation.getExpressionManager().boolean(true)), addedAllGuards(addAllGuards), currentGame(nullptr) {
@@ -58,7 +57,7 @@ namespace storm {
                         }
                         maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
                     }
-                
+                    
                     totalNumberOfCommands += module.getNumberOfCommands();
                 }
                 
@@ -76,23 +75,19 @@ namespace storm {
                 commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
                 
                 // Now that we have created all other DD variables, we create the DD variables for the predicates.
-                std::vector<std::pair<storm::expressions::Expression, bool>> allPredicates;
+                std::vector<std::pair<storm::expressions::Expression, bool>> initialPredicates;
-                for (auto const& predicate : initialPredicates) {
-                    allPredicates.push_back(std::make_pair(predicate, false));
-                }
                 if (addAllGuards) {
                     for (auto const& guard : allGuards) {
-                        allPredicates.push_back(std::make_pair(guard, true));
+                        initialPredicates.push_back(std::make_pair(guard, true));
                     }
                 }
+                
                 // Finally, refine using the all predicates and build game as a by-product.
-                this->refine(allPredicates);
+                this->refine(initialPredicates);
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::refine(std::vector<std::pair<storm::expressions::Expression, bool>> const& predicates) {
-                STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates.");
-                
                 // Add the predicates to the global list of predicates.
                 std::vector<uint_fast64_t> newPredicateIndices;
                 for (auto const& predicateAllowSplitPair : predicates) {
@@ -132,7 +127,7 @@ namespace storm {
                 
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(newPredicateIndices);
-                                
+                
                 // Finally, we rebuild the game.
                 currentGame = buildGame();
             }
@@ -240,7 +235,7 @@ namespace storm {
 #endif
                     std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
                     STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
-
+                    
 #ifdef LOCAL_DEBUG
                     std::cout << "lower" << std::endl;
                     for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) {
@@ -268,6 +263,9 @@ namespace storm {
                             for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
                                 if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
                                     // Now we know the point of the deviation (command, update, predicate).
+                                    std::cout << "ref" << std::endl;
+                                    std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl;
+                                    std::cout << concreteCommand.getUpdate(updateIndex) << std::endl;
                                     newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
                                     break;
                                 }
@@ -298,12 +296,12 @@ namespace storm {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
                 return abstractionInformation.getPredicateSourceVariable(predicate);
             }
-                        
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::unique_ptr<MenuGame<DdType, ValueType>> AbstractProgram<DdType, ValueType>::buildGame() {
                 // As long as there is only one module, we only build its game representation.
                 GameBddResult<DdType> game = modules.front().getAbstractBdd();
-
+                
                 // Construct a set of all unnecessary variables, so we can abstract from it.
                 std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
                 auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables);
@@ -326,7 +324,7 @@ namespace storm {
                 if (!deadlockStates.isZero()) {
                     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());
                 bool hasBottomStates = false;
@@ -345,17 +343,17 @@ namespace storm {
                 reachableStates &= abstractionInformation.getBottomStateBdd(true, true);
                 initialStates &= abstractionInformation.getBottomStateBdd(true, true);
                 
-                // If there are bottom transitions, exnted the transition matrix and reachable states now. 
+                // If there are bottom transitions, exnted the transition matrix and reachable states now.
                 if (hasBottomStates) {
                     transitionMatrix += bottomStateResult.transitions.template toAdd<ValueType>();
                     reachableStates |= bottomStateResult.states;
                 }
-            
+                
                 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());
-
+                
                 std::set<storm::expressions::Variable> allSourceVariables(abstractionInformation.getSourceVariables());
                 allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true));
                 std::set<storm::expressions::Variable> allSuccessorVariables(abstractionInformation.getSuccessorVariables());
@@ -363,7 +361,7 @@ namespace storm {
                 
                 return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
             }
-                        
+            
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
                 std::ofstream out(filename);
@@ -402,7 +400,7 @@ namespace storm {
                     }
                     highlightStates.insert(stateName.str());
                 }
-
+                
                 out << "digraph game {" << std::endl;
                 
                 // Create the player 1 nodes.
@@ -504,7 +502,7 @@ namespace storm {
             template class AbstractProgram<storm::dd::DdType::CUDD, double>;
             template class AbstractProgram<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL
-			template class AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+            template class AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 #endif
         }
     }

src/storm/abstraction/prism/AbstractProgram.h

@@ -42,12 +42,11 @@ namespace storm {
                  *
                  * @param expressionManager The manager responsible for the expressions of the program.
                  * @param program The concrete program for which to build the abstraction.
-                 * @param initialPredicates The initial set of predicates.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates.
                  * @param splitPredicates A flag that indicates whether the predicates are to be split into atoms before being added.
                  */
-                AbstractProgram(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false, bool splitPredicates = false);
+                AbstractProgram(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false, bool splitPredicates = false);
                 
                 AbstractProgram(AbstractProgram const&) = default;
                 AbstractProgram& operator=(AbstractProgram const&) = default;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -10,7 +10,7 @@ namespace storm {
         namespace prism {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()) {
+            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()) {
                 // Intentionally left empty.
             }
             

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -11,7 +11,7 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
             public:
-                PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
+                PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
                 
                 virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -12,6 +12,7 @@
 #include "storm/storage/dd/DdManager.h"
 
 #include "storm/abstraction/prism/PrismMenuGameAbstractor.h"
+#include "storm/abstraction/MenuGameRefiner.h"
 
 #include "storm/logic/FragmentSpecification.h"
 
@@ -261,6 +262,7 @@ namespace storm {
             if (lowerChoicesDifferent) {
                 STORM_LOG_TRACE("Refining based on lower choice.");
                 auto refinementStart = std::chrono::high_resolution_clock::now();
+                
                 abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
                 auto refinementEnd = std::chrono::high_resolution_clock::now();
                 STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
@@ -466,9 +468,11 @@ namespace storm {
             storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask);
             
             // Create the abstractor.
-            storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedModel.asPrismProgram(), initialPredicates, smtSolverFactory);
+            storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedModel.asPrismProgram(), smtSolverFactory);
             
-            // TODO: create refiner and move initial predicates there.
+            // Create a refiner that can be used to refine the abstraction when needed.
+            storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(abstractor);
+            refiner.refine(initialPredicates);
             
             // Enter the main-loop of abstraction refinement.
             for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
@@ -526,6 +530,7 @@ namespace storm {
                     }
                 }
                 
+                // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
                 if (!qualitativeRefinement) {
                     // At this point, we know that we cannot answer the query without further numeric computation.
 
@@ -534,14 +539,14 @@ namespace storm {
                     STORM_LOG_TRACE("Starting numerical solution step.");
                     auto quantitativeStart = std::chrono::high_resolution_clock::now();
 
-                    // Solve the min values and check whether we can give the answer already.
+                    // (7) Solve the min values and check whether we can give the answer already.
                     QuantitativeResult<Type, ValueType> minResult = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin);
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, minResult.initialStateValue);
                     if (result) {
                         return result;
                     }
                     
-                    // Solve the max values and check whether we can give the answer already.
+                    // (8) Solve the max values and check whether we can give the answer already.
                     QuantitativeResult<Type, ValueType> maxResult = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(minResult));
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, maxResult.initialStateValue);
                     if (result) {
@@ -551,27 +556,20 @@ namespace storm {
                     auto quantitativeEnd = std::chrono::high_resolution_clock::now();
                     STORM_LOG_DEBUG("Obtained quantitative bounds [" << minResult.initialStateValue << ", " << maxResult.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
 
+                    // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, minResult.initialStateValue, maxResult.initialStateValue);
                     if (result) {
                         return result;
                     }
 
-                    // If we arrived at this point, it means that we have all qualitative and quantitative information
-                    // about the game, but we could not yet answer the query. In this case, we need to refine.
-                    
                     // Make sure that all strategies are still valid strategies.
                     STORM_LOG_ASSERT(minResult.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
                     STORM_LOG_ASSERT(maxResult.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
                     STORM_LOG_ASSERT(minResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
                     STORM_LOG_ASSERT(maxResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
 
-#ifdef LOCAL_DEBUG
+                    // (10) If we arrived at this point, it means that we have all qualitative and quantitative
-					// Check whether the strategies coincide over the reachable parts.
+                    // information about the game, but we could not yet answer the query. In this case, we need to refine.
-//					storm::dd::Bdd<Type> tmp = game.getTransitionMatrix().toBdd() && (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy);
-//					storm::dd::Bdd<Type> commonReach = storm::utility::dd::computeReachableStates(initialStates, tmp.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables());
-//					STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide.");
-#endif
-
                     refineAfterQuantitativeCheck(abstractor, game, transitionMatrixBdd, minResult, maxResult);
                 }
                 auto iterationEnd = std::chrono::high_resolution_clock::now();
@@ -632,7 +630,11 @@ namespace storm {
                 result = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true);
             }
             
-            STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+            if (prob0) {
+                STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+            } else {
+                STORM_LOG_ASSERT(result.hasPlayer1Strategy() && ((result.getPlayer1States() && !targetStates).isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+            }
             STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy.");
 
             STORM_LOG_TRACE("Computed states with probability " << (prob0 ? "0" : "1") << " (player 1: " << player1Direction << ", player 2: " << player2Direction << "): " << result.getPlayer1States().getNonZeroCount() << " '" << (prob0 ? "no" : "yes") << "' states.");

src/storm/utility/graph.cpp

@@ -961,7 +961,10 @@ namespace storm {
                 
                 // Since we have determined the complements of the desired sets, we need to complement it now.
                 player1States = !player1States && model.getReachableStates();
-                player2States = !player2States && model.getReachableStates();
+                std::set<storm::expressions::Variable> variablesToAbstract(model.getColumnVariables());
+                variablesToAbstract.insert(model.getPlayer2Variables().begin(), model.getPlayer2Variables().end());
+                player2States = !player2States && transitionMatrix.existsAbstract(variablesToAbstract);
 
                 // Determine all transitions between prob0 states.
                 storm::dd::Bdd<Type> transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs()));