fixes and improvements for game-based abstraction

src/storm/abstraction/ExpressionTranslator.cpp

@@ -118,7 +118,7 @@ namespace storm {
                 
                 // At this point, none of the predicates was found to be equivalent, but there is no need to split as the subexpressions are not valid predicates.
                 
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator.");
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator (" << expression << ").");
             }
             return boost::any();
         }

src/storm/abstraction/MenuGameRefiner.cpp

@@ -63,14 +63,17 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseInterpolationSet()), splitAll(false), splitPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) {
+        MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseInterpolationSet()), splitAll(false), splitPredicates(false), rankPredicates(false), addedAllGuardsFlag(false), pivotSelectionHeuristic(), splitter(), equivalenceChecker(std::move(smtSolver)) {
             
-            equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints());
+            auto const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
             
+            pivotSelectionHeuristic = abstractionSettings.getPivotSelectionHeuristic();
             AbstractionSettings::SplitMode splitMode = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSplitMode();
             splitAll = splitMode == AbstractionSettings::SplitMode::All;
             splitPredicates = splitMode == AbstractionSettings::SplitMode::NonGuard;
+            rankPredicates = abstractionSettings.isRankRefinementPredicatesSet();
             
+            equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints());
             if (storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
                 std::vector<storm::expressions::Expression> guards;
                 
@@ -82,7 +85,7 @@ namespace storm {
                     }
                 }
                 performRefinement(createGlobalRefinement(preprocessPredicates(guards, RefinementPredicates::Source::InitialGuard)));
-                
+
                 addedAllGuardsFlag = true;
             }
         }
@@ -298,6 +301,9 @@ namespace storm {
                         for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) {
                             if (lower[predicateIndex] != upper[predicateIndex]) {
                                 possibleRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(variableUpdates).simplify());
+                                if (!rankPredicates) {
+                                    break;
+                                }
                             }
                         }
                         ++orderedUpdateIndex;
@@ -307,49 +313,54 @@ namespace storm {
                 
                 STORM_LOG_ASSERT(!possibleRefinementPredicates.empty(), "Expected refinement predicates.");
                 
-                // Since we can choose any of the deviation predicates to perform the split, we go through the remaining
-                // updates and build all deviation predicates. We can then check whether any of the possible refinement
-                // predicates also eliminates another deviation.
-                std::vector<storm::expressions::Expression> otherRefinementPredicates;
-                for (; orderedUpdateIndex < updateIndicesAndMasses.size(); ++orderedUpdateIndex) {
-                    storm::storage::BitVector const& lower = lowerChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
-                    storm::storage::BitVector const& upper = upperChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
-                    
-                    bool deviates = lower != upper;
-                    if (deviates) {
-                        std::map<storm::expressions::Variable, storm::expressions::Expression> newVariableUpdates = abstractor.get().getVariableUpdates(player1Index, updateIndicesAndMasses[orderedUpdateIndex].first);
-                        for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) {
-                            if (lower[predicateIndex] != upper[predicateIndex]) {
-                                otherRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(newVariableUpdates).simplify());
+                if (rankPredicates) {
+                    // Since we can choose any of the deviation predicates to perform the split, we go through the remaining
+                    // updates and build all deviation predicates. We can then check whether any of the possible refinement
+                    // predicates also eliminates another deviation.
+                    std::vector<storm::expressions::Expression> otherRefinementPredicates;
+                    for (; orderedUpdateIndex < updateIndicesAndMasses.size(); ++orderedUpdateIndex) {
+                        storm::storage::BitVector const& lower = lowerChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
+                        storm::storage::BitVector const& upper = upperChoiceUpdateToSuccessorMapping.at(updateIndicesAndMasses[orderedUpdateIndex].first).first;
+                        
+                        bool deviates = lower != upper;
+                        if (deviates) {
+                            std::map<storm::expressions::Variable, storm::expressions::Expression> newVariableUpdates = abstractor.get().getVariableUpdates(player1Index, updateIndicesAndMasses[orderedUpdateIndex].first);
+                            for (uint64_t predicateIndex = 0; predicateIndex < lower.size(); ++predicateIndex) {
+                                if (lower[predicateIndex] != upper[predicateIndex]) {
+                                    otherRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(newVariableUpdates).simplify());
+                                }
                             }
                         }
                     }
-                }
-                
-                // Finally, go through the refinement predicates and see how many deviations they cover.
-                std::vector<uint64_t> refinementPredicateIndexToCount(possibleRefinementPredicates.size(), 0);
-                for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
-                    refinementPredicateIndexToCount[index] = 1;
-                }
-                for (auto const& otherPredicate : otherRefinementPredicates) {
+                    
+                    // Finally, go through the refinement predicates and see how many deviations they cover.
+                    std::vector<uint64_t> refinementPredicateIndexToCount(possibleRefinementPredicates.size(), 0);
                     for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
-                        if (equivalenceChecker.areEquivalentModuloNegation(otherPredicate, possibleRefinementPredicates[index])) {
-                            ++refinementPredicateIndexToCount[index];
+                        refinementPredicateIndexToCount[index] = 1;
+                    }
+                    for (auto const& otherPredicate : otherRefinementPredicates) {
+                        for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
+                            if (equivalenceChecker.areEquivalentModuloNegation(otherPredicate, possibleRefinementPredicates[index])) {
+                                ++refinementPredicateIndexToCount[index];
+                            }
                         }
                     }
-                }
-
-                // Find predicate that covers the most deviations.
-                uint64_t chosenPredicateIndex = 0;
-                for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
-                    if (refinementPredicateIndexToCount[index] > refinementPredicateIndexToCount[chosenPredicateIndex]) {
-                        chosenPredicateIndex = index;
+                    
+                    // Find predicate that covers the most deviations.
+                    uint64_t chosenPredicateIndex = 0;
+                    for (uint64_t index = 0; index < possibleRefinementPredicates.size(); ++index) {
+                        if (refinementPredicateIndexToCount[index] > refinementPredicateIndexToCount[chosenPredicateIndex]) {
+                            chosenPredicateIndex = index;
+                        }
                     }
+                    newPredicate = possibleRefinementPredicates[chosenPredicateIndex];
+                    STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << ", (equivalent to " << (refinementPredicateIndexToCount[chosenPredicateIndex] - 1) << " other refinement predicates).");
+                } else {
+                    newPredicate = possibleRefinementPredicates.front();
+                    STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << ".");
                 }
-                newPredicate = possibleRefinementPredicates[chosenPredicateIndex];
 
                 STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation.");
-                STORM_LOG_DEBUG("Derived new predicate (based on weakest-precondition): " << newPredicate << ", (equivalent to " << (refinementPredicateIndexToCount[chosenPredicateIndex] - 1) << " other refinement predicates)");
             }
             
             return RefinementPredicates(fromGuard ? RefinementPredicates::Source::Guard : RefinementPredicates::Source::WeakestPrecondition, {newPredicate});
@@ -633,6 +644,9 @@ namespace storm {
 
         template<storm::dd::DdType Type>
         boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation<Type> const& abstractionInformation, std::vector<std::vector<storm::expressions::Expression>> const& trace, std::map<storm::expressions::Variable, storm::expressions::Expression> const& variableSubstitution) {
+            
+            auto start = std::chrono::high_resolution_clock::now();
+            boost::optional<RefinementPredicates> predicates;
 
             // Create solver and interpolation groups.
             storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true));
@@ -671,16 +685,15 @@ namespace storm {
                         STORM_LOG_DEBUG("Derived new predicate (based on interpolation at step " << step << " out of " << stepCounter << "): " << interpolant);
                         interpolants.push_back(interpolant);
                     }
-//                    else {
-//                        STORM_LOG_ASSERT(step == 0false, "The found interpolant (based on interpolation at step " << step << " out of " << stepCounter << ") is '" << interpolant << "', which shouldn't happen.");
-//                    }
                 }
-                return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants));
+                predicates = boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants));
             } else {
                 STORM_LOG_TRACE("Trace formula is satisfiable, not using interpolation.");
             }
-            
-            return boost::none;
+            auto end = std::chrono::high_resolution_clock::now();
+            STORM_LOG_TRACE("Deriving predicates using interpolation from witness of size " << trace.size() << " took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+
+            return predicates;
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -843,6 +856,8 @@ namespace storm {
             bool foundPivotState = false;
             ValueType pivotStateDeviation = storm::utility::zero<ValueType>();
             auto const& player2Grouping = transitionMatrix.getRowGroupIndices();
+
+            uint64_t pivotStates = 0;
             
             while (!dijkstraQueue.empty()) {
                 auto distanceStatePair = *dijkstraQueue.begin();
@@ -878,6 +893,7 @@ namespace storm {
                 }                
                 // If it is indeed a pivot state, we can abort the search here.
                 if (isPivotState) {
+                    
                     if (considerDeviation && foundPivotState) {
                         ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState];
                         if (deviationOfCurrentState > pivotStateDeviation) {
@@ -913,7 +929,7 @@ namespace storm {
                         }
                         
                         ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
-                        if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
+                        if (probabilityDistances ? alternateDistance > distances[player1Successor] : alternateDistance < distances[player1Successor]) {
                             distances[player1Successor] = alternateDistance;
                             if (generatePredecessors) {
                                 result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[minPlayer2Successor]);
@@ -934,7 +950,7 @@ namespace storm {
                         }
                         
                         ValueType alternateDistance = probabilityDistances ? currentDistance * entry.getValue() : currentDistance + storm::utility::one<ValueType>();
-                        if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
+                        if (probabilityDistances ? alternateDistance > distances[player1Successor] : !probabilityDistances && alternateDistance < distances[player1Successor]) {
                             distances[player1Successor] = alternateDistance;
                             if (generatePredecessors) {
                                 result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[maxPlayer2Successor]);
@@ -945,6 +961,12 @@ namespace storm {
                 }
             }
             
+            std::cout << "found " << pivotStates << " pivots" << std::endl;
+            
+            if (foundPivotState) {
+                return result;
+            }
+
             // If we arrived at this point, we have explored all relevant states, but none of them was a pivot state,
             // which can happen when trying to refine using the qualitative result only.
             return boost::none;
@@ -1004,6 +1026,7 @@ namespace storm {
                     maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
                 }
             }
+            auto end = std::chrono::high_resolution_clock::now();
 
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
@@ -1012,6 +1035,7 @@ namespace storm {
             if (!predicates) {
                 predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             }
+            end = std::chrono::high_resolution_clock::now();
             STORM_LOG_THROW(static_cast<bool>(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue.");
             
             std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates(predicates.get().getPredicates(), predicates.get().getSource());
@@ -1027,11 +1051,7 @@ namespace storm {
             
             boost::optional<ExplicitPivotStateResult<ValueType>> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, minStrategyPair, maxStrategyPair, &quantitativeResult.getMin().getValues(), &quantitativeResult.getMax().getValues());
             
-            // If there was no pivot state, continue the search.
-            if (!optionalPivotStateResult) {
-                STORM_LOG_TRACE("Did not find pivot state in qualitative fragment.");
-                return false;
-            }
+            STORM_LOG_THROW(optionalPivotStateResult, storm::exceptions::InvalidStateException, "Did not find pivot state to proceed.");
             
             // Otherwise, we can refine.
             auto const& pivotStateResult = optionalPivotStateResult.get();
@@ -1121,6 +1141,12 @@ namespace storm {
             return true;
         }
         
+        struct VariableSetHash {
+            std::size_t operator()(std::set<storm::expressions::Variable> const& set) const {
+                return set.size();
+            }
+        };
+        
         template<storm::dd::DdType Type, typename ValueType>
         std::vector<storm::expressions::Expression> MenuGameRefiner<Type, ValueType>::preprocessPredicates(std::vector<storm::expressions::Expression> const& predicates, RefinementPredicates::Source const& source) const {
             bool split = source == RefinementPredicates::Source::WeakestPrecondition && splitPredicates;
@@ -1128,37 +1154,80 @@ namespace storm {
             split |= splitAll;
             
             if (split) {
+                auto start = std::chrono::high_resolution_clock::now();
                 AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
                 std::vector<storm::expressions::Expression> cleanedAtoms;
                 
+                std::unordered_map<std::set<storm::expressions::Variable>, std::vector<storm::expressions::Expression>, VariableSetHash> predicateClasses;
+                
                 for (auto const& predicate : predicates) {
-                    
                     // Split the predicates.
                     std::vector<storm::expressions::Expression> atoms = splitter.split(predicate);
                     
-                    // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have.
+                    // Put the atoms into the right class.
                     for (auto const& atom : atoms) {
-                        // Check whether the newly found atom is equivalent to an atom we already have in the predicate
-                        // set or in the set that is to be added.
-                        bool addAtom = true;
-                        for (auto const& oldPredicate : abstractionInformation.getPredicates()) {
-                            if (equivalenceChecker.areEquivalent(atom, oldPredicate) || equivalenceChecker.areEquivalent(atom, !oldPredicate)) {
-                                addAtom = false;
+                        std::set<storm::expressions::Variable> vars = atom.getVariables();
+                        predicateClasses[vars].push_back(atom);
+                    }
+                }
+                
+                // Now clean the classes in the sense that redundant predicates are cleaned.
+                for (auto& predicateClass : predicateClasses) {
+                    std::vector<storm::expressions::Expression> cleanedAtomsOfClass;
+                    
+                    for (auto const& predicate : predicateClass.second) {
+                        bool addPredicate = true;
+                        for (auto const& atom : cleanedAtomsOfClass) {
+                            if (predicate.areSame(atom)) {
+                                addPredicate = false;
                                 break;
                             }
-                        }
-                        for (auto const& addedAtom : cleanedAtoms) {
-                            if (equivalenceChecker.areEquivalent(addedAtom, atom) || equivalenceChecker.areEquivalent(addedAtom, !atom)) {
-                                addAtom = false;
+                            
+                            if (addPredicate && equivalenceChecker.areEquivalentModuloNegation(predicate, atom)) {
+                                addPredicate = false;
                                 break;
                             }
                         }
-                        
-                        if (addAtom) {
-                            cleanedAtoms.push_back(atom);
+                        if (addPredicate) {
+                            cleanedAtomsOfClass.push_back(predicate);
                         }
                     }
+                    
+                    predicateClass.second = std::move(cleanedAtomsOfClass);
+                }
+
+                std::unordered_map<std::set<storm::expressions::Variable>, std::vector<storm::expressions::Expression>, VariableSetHash> oldPredicateClasses;
+                for (auto const& oldPredicate : abstractionInformation.getPredicates()) {
+                    std::set<storm::expressions::Variable> vars = oldPredicate.getVariables();
+                    
+                    oldPredicateClasses[vars].push_back(oldPredicate);
+                }
+                
+                for (auto const& predicateClass : predicateClasses) {
+                    auto oldPredicateClassIt = oldPredicateClasses.find(predicateClass.first);
+                    if (oldPredicateClassIt != oldPredicateClasses.end()) {
+                        for (auto const& newAtom : predicateClass.second) {
+                            for (auto const& oldPredicate : oldPredicateClassIt->second) {
+                                bool addAtom = true;
+                                if (newAtom.areSame(oldPredicate)) {
+                                    addAtom = false;
+                                    break;
+                                }
+                                if (equivalenceChecker.areEquivalentModuloNegation(newAtom, oldPredicate)) {
+                                    addAtom = false;
+                                    break;
+                                }
+                                if (addAtom) {
+                                    cleanedAtoms.push_back(newAtom);
+                                }
+                            }
+                        }
+                    } else {
+                        cleanedAtoms.insert(cleanedAtoms.end(), predicateClass.second.begin(), predicateClass.second.end());
+                    }
                 }
+                auto end = std::chrono::high_resolution_clock::now();
+                STORM_LOG_TRACE("Preprocessing predicates took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                 
                 return cleanedAtoms;
             } else {

src/storm/abstraction/MenuGameRefiner.h

@@ -78,7 +78,7 @@ namespace storm {
             ExplicitPivotStateResult() = default;
             
             uint64_t pivotState;
-            
+                        
             /// The distance with which the state in question is reached.
             ValueType distance;
             
@@ -177,6 +177,9 @@ namespace storm {
             /// A flag indicating whether predicates derived from weakest preconditions shall be split before using them for refinement.
             bool splitPredicates;
             
+            /// A flag indicating whether predicates are to be ranked.
+            bool rankPredicates;
+            
             /// A flag indicating whether all guards have been used to refine the abstraction.
             bool addedAllGuardsFlag;
 

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -81,7 +81,7 @@ namespace storm {
                     STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool.");
                     predicateIndices.push_back(abstractionInformation.getOrAddPredicate(predicate));
                 }
-                
+
                 // Refine all abstract modules.
                 for (auto& module : modules) {
                     module.refine(predicateIndices);
@@ -171,27 +171,29 @@ namespace storm {
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
-                
+
+                // Cut transition relation to the reachable states for backward search.
+                transitionRelation &= reachableStates;
+
                 relevantStatesWatch.start();
                 if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) {
-                    // Cut transition relation to the reachable states for backward search.
-                    transitionRelation &= reachableStates;
-                
+
                     // Get the target state BDD.
                     storm::dd::Bdd<DdType> targetStates = reachableStates && this->getStates(this->getTargetStateExpression());
-                    
+
                     // In the presence of target states, we keep only states that can reach the target states.
                     reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates;
-                 
+
+                    // Include all successors of reachable states, because the backward search otherwise potentially
+                    // cuts probability 0 choices of these states.
+                    reachableStates = reachableStates || reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
+
                     // Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self-
                     // loops of (now) deadlock states.
                     transitionRelation &= reachableStates;
-                    
-                    // Include all successors of reachable states, because the backward search otherwise potentially
-                    // cuts probability 0 choices of these states.
-                    reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
+
                     relevantStatesWatch.stop();
-                    
+
                     STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms.");
                 }
                 
@@ -212,7 +214,7 @@ namespace storm {
                 bool hasBottomStates = !bottomStateResult.states.isZero();
                 
                 // Construct the transition matrix by cutting away the transitions of unreachable states.
-                storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>();
+                storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd<ValueType>();
                 transitionMatrix *= commandUpdateProbabilitiesAdd;
                 transitionMatrix += deadlockTransitions;
                 

src/storm/adapters/GmmxxAdapter.cpp

@@ -13,7 +13,7 @@ namespace storm {
         template<typename T>
         std::unique_ptr<gmm::csr_matrix<T>> GmmxxAdapter<T>::toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
             uint_fast64_t realNonZeros = matrix.getEntryCount();
-            STORM_LOG_DEBUG("Converting " << matrix.getRowCount() << "x" << matrix.getColumnCount() << " matrix with " << realNonZeros << " non-zeros to gmm++ format.");
+            STORM_LOG_TRACE("Converting " << matrix.getRowCount() << "x" << matrix.getColumnCount() << " matrix with " << realNonZeros << " non-zeros to gmm++ format.");
             
             // Prepare the resulting matrix.
             std::unique_ptr<gmm::csr_matrix<T>> result(new gmm::csr_matrix<T>(matrix.getRowCount(), matrix.getColumnCount()));
@@ -37,7 +37,7 @@ namespace storm {
             std::swap(result->ir, columns);
             std::swap(result->pr, values);
             
-            STORM_LOG_DEBUG("Done converting matrix to gmm++ format.");
+            STORM_LOG_TRACE("Done converting matrix to gmm++ format.");
             
             return result;
         }

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -54,6 +54,7 @@ namespace storm {
         using storm::abstraction::ExplicitQuantitativeResult;
         using storm::abstraction::ExplicitQuantitativeResultMinMax;
         using storm::abstraction::ExplicitGameStrategyPair;
+        using detail::PreviousExplicitResult;
 
         template<storm::dd::DdType Type, typename ModelType>
         GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()) {
@@ -62,13 +63,16 @@ namespace storm {
                 storm::prism::Program const& originalProgram = model.asPrismProgram();
                 STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
                 
+                auto flattenStart = std::chrono::high_resolution_clock::now();
                 // Flatten the modules if there is more than one.
                 if (originalProgram.getNumberOfModules() > 1) {
                     preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory);
                 } else {
                     preprocessedModel = originalProgram;
                 }
-                
+                auto flattenEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Flattened model in " << std::chrono::duration_cast<std::chrono::milliseconds>(flattenEnd - flattenStart).count() << "ms.");
+
                 STORM_LOG_TRACE("Game-based model checker got program " << preprocessedModel.asPrismProgram());
             } else {
                 storm::jani::Model const& originalModel = model.asJaniModel();
@@ -391,22 +395,31 @@ namespace storm {
         }
         
         template<typename ValueType>
-        ExplicitQuantitativeResult<ValueType> computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& strategyPair, ExplicitQuantitativeResult<ValueType> const* startingQuantitativeResult = nullptr, ExplicitGameStrategyPair const* startingStrategyPair = nullptr) {
+        ExplicitQuantitativeResult<ValueType> computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& strategyPair, storm::dd::Odd const& odd, ExplicitQuantitativeResult<ValueType> const* startingQuantitativeResult = nullptr, ExplicitGameStrategyPair const* startingStrategyPair = nullptr, boost::optional<PreviousExplicitResult<ValueType>> const& previousResult = boost::none) {
 
             bool player2Min = player2Direction == storm::OptimizationDirection::Minimize;
             auto const& player1Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer1States();
             auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States();
             auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States();
             
-            // If there are no maybe states, we construct the quantitative result from the qualitative result alone.
+            ExplicitQuantitativeResult<ValueType> result(maybeStates.size());
+            storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one<ValueType>());
+
+            // If there are no maybe states, there is nothing we need to solve.
             if (maybeStates.empty()) {
-                ExplicitQuantitativeResult<ValueType> result(maybeStates.size());
-                storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one<ValueType>());
                 return result;
             }
+
+            // If there is a previous result, unpack the previous values with respect to the new ODD.
+            if (previousResult) {
+                previousResult.get().odd.oldToNewIndex(odd, [&previousResult,&result,player2Min] (uint64_t oldOffset, uint64_t newOffset) {
+                    result.getValues()[newOffset] = player2Min ? previousResult.get().values.getMin().getValues()[oldOffset] : previousResult.get().values.getMax().getValues()[oldOffset];
+                });
+            }
             
             // Otherwise, we need to solve a (sub)game.
-            
+            STORM_LOG_TRACE("Solving " << maybeStates.getNumberOfSetBits()<< " maybe states.");
+
             // Create the game by selecting all maybe player 2 states (non-prob0/1) of all maybe player 1 states.
             std::vector<uint64_t> subPlayer1Groups(maybeStates.getNumberOfSetBits() + 1);
             uint64_t position = 0;
@@ -440,6 +453,10 @@ namespace storm {
             if (startingQuantitativeResult) {
                 storm::utility::vector::selectVectorValues(values, maybeStates, startingQuantitativeResult->getValues());
             }
+            if (previousResult) {
+                STORM_LOG_ASSERT(!startingQuantitativeResult, "Cannot take two different hints.");
+                storm::utility::vector::selectVectorValues(values, maybeStates, result.getValues());
+            }
             
             // Prepare scheduler storage.
             std::vector<uint64_t> player1Scheduler(subPlayer1Groups.size() - 1);
@@ -473,9 +490,7 @@ namespace storm {
             // Solve actual game and track schedulers.
             gameSolver->solveGame(env, player1Direction, player2Direction, values, b, &player1Scheduler, &player2Scheduler);
             
-            // Create combined result for all states.
-            ExplicitQuantitativeResult<ValueType> result(maybeStates.size());
-            storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one<ValueType>());
+            // Set values according to quantitative result (qualitative result has already been taken care of).
             storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values);
                         
             // Obtain strategies from solver and fuse them with the pre-existing strategy pair for the qualitative result.
@@ -526,19 +541,19 @@ namespace storm {
             }
             abstractor->addTerminalStates(targetStateExpression);
             abstractor->setTargetStates(targetStateExpression);
+
             
             // Create a refiner that can be used to refine the abstraction when needed.
             storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()));
             refiner.refine(initialPredicates);
-            
+
             storm::dd::Bdd<Type> globalConstraintStates = abstractor->getStates(constraintExpression);
             storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);
             
             // Enter the main-loop of abstraction refinement.
             boost::optional<SymbolicQualitativeGameResultMinMax<Type>> previousSymbolicQualitativeResult = boost::none;
             boost::optional<SymbolicQuantitativeGameResult<Type, ValueType>> previousSymbolicMinQuantitativeResult = boost::none;
-            boost::optional<ExplicitQualitativeGameResultMinMax> previousExplicitQualitativeResult = boost::none;
-            // boost::optional<ExplicitQuantitativeGameResult<ValueType>> previousExplicitMinQuantitativeResult = boost::none;
+            boost::optional<PreviousExplicitResult<ValueType>> previousExplicitResult = boost::none;
             for (uint_fast64_t iterations = 0; iterations < maximalNumberOfAbstractions; ++iterations) {
                 auto iterationStart = std::chrono::high_resolution_clock::now();
                 STORM_LOG_TRACE("Starting iteration " << iterations << ".");
@@ -568,7 +583,7 @@ namespace storm {
                 if (solveMode == storm::settings::modules::AbstractionSettings::SolveMode::Dd) {
                     result = performSymbolicAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousSymbolicQualitativeResult, previousSymbolicMinQuantitativeResult);
                 } else {
-                    result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousExplicitQualitativeResult);
+                    result = performExplicitAbstractionSolutionStep(env, checkTask, game, player1Direction, initialStates, constraintStates, targetStates, refiner, previousExplicitResult);
                 }
 
                 if (result) {
@@ -684,7 +699,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ModelType>
-        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStatesBdd, storm::dd::Bdd<Type> const& constraintStatesBdd, storm::dd::Bdd<Type> const& targetStatesBdd, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<ExplicitQualitativeGameResultMinMax>& previousQualitativeResult) {
+        std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStatesBdd, storm::dd::Bdd<Type> const& constraintStatesBdd, storm::dd::Bdd<Type> const& targetStatesBdd, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<PreviousExplicitResult<ValueType>>& previousResult) {
             STORM_LOG_TRACE("Using sparse solving.");
 
             // (0) Start by transforming the necessary symbolic elements to explicit ones.
@@ -749,7 +764,7 @@ namespace storm {
             
             // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
             auto qualitativeStart = std::chrono::high_resolution_clock::now();
-            ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair);
+            ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousResult, odd, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair);
             std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<ValueType>(checkTask, initialStates, qualitativeResult);
             if (result) {
                 return result;
@@ -782,22 +797,23 @@ namespace storm {
                 return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), ValueType(0.5));
             }
             
+            ExplicitQuantitativeResultMinMax<ValueType> quantitativeResult;
+
             // (4) 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.
                 STORM_LOG_TRACE("Starting numerical solution step.");
-                ExplicitQuantitativeResultMinMax<ValueType> quantitativeResult;
-
+                
                 // (7) Solve the min values and check whether we can give the answer already.
                 auto quantitativeStart = std::chrono::high_resolution_clock::now();
-                quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair));
+                quantitativeResult.setMin(computeQuantitativeResult<ValueType>(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair, odd, nullptr, nullptr, this->reuseQuantitativeResults ? previousResult : boost::none));
                 result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates));
                 if (result) {
                     return result;
                 }
 
                 // (8) Solve the max values and check whether we can give the answer already.
-                quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, &quantitativeResult.getMin(), &minStrategyPair));
+                quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair));
                 result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates));
                 if (result) {
                     return result;
@@ -821,6 +837,33 @@ namespace storm {
                 refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair);
                 auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
                 STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
+
+                if (this->reuseQuantitativeResults) {
+                    PreviousExplicitResult<ValueType> nextPreviousResult;
+                    nextPreviousResult.values = std::move(quantitativeResult);
+                    nextPreviousResult.odd = odd;
+                    
+                    // We transform the offset choices for the states to their labels, so we can more easily identify
+                    // them in the next iteration.
+                    nextPreviousResult.minPlayer1Labels.resize(odd.getTotalOffset());
+                    nextPreviousResult.maxPlayer1Labels.resize(odd.getTotalOffset());
+                    for (uint64_t player1State = 0; player1State < odd.getTotalOffset(); ++player1State) {
+                        if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(player1State)) {
+                            nextPreviousResult.minPlayer1Labels[player1State] = player1Labeling[minStrategyPair.getPlayer1Strategy().getChoice(player1State)];
+                        } else {
+                            nextPreviousResult.minPlayer1Labels[player1State] = std::numeric_limits<uint64_t>::max();
+                        }
+                        if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(player1State)) {
+                            nextPreviousResult.maxPlayer1Labels[player1State] = player1Labeling[maxStrategyPair.getPlayer1Strategy().getChoice(player1State)];
+                        } else {
+                            nextPreviousResult.minPlayer1Labels[player1State] = std::numeric_limits<uint64_t>::max();
+                        }
+                    }
+                    
+                    previousResult = std::move(nextPreviousResult);
+                    
+                    STORM_LOG_TRACE("Prepared next previous result to reuse values.");
+                }
             }
             
             return nullptr;
@@ -885,64 +928,17 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ModelType>
-        ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair) {
+        ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<PreviousExplicitResult<ValueType>> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair) {
             
             ExplicitQualitativeGameResultMinMax result;
-            
-//            if (reuseQualitativeResults) {
-//                // Depending on the player 1 direction, we choose a different order of operations.
-//                if (player1Direction == storm::OptimizationDirection::Minimize) {
-//                    // (1) min/min: compute prob0 using the game functions
-//                    result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
-//
-//                    // (2) min/min: compute prob1 using the MDP functions
-//                    storm::dd::Bdd<Type> candidates = game.getReachableStates() && !result.prob0Min.player1States;
-//                    storm::dd::Bdd<Type> prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates);
-//
-//                    // (3) min/min: compute prob1 using the game functions
-//                    result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp));
-//
-//                    // (4) min/max: compute prob 0 using the game functions
-//                    result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
-//
-//                    // (5) min/max: compute prob 1 using the game functions
-//                    // We know that only previous prob1 states can now be prob 1 states again, because the upper bound
-//                    // values can only decrease over iterations.
-//                    boost::optional<storm::dd::Bdd<Type>> prob1Candidates;
-//                    if (previousQualitativeResult) {
-//                        prob1Candidates = previousQualitativeResult.get().prob1Max.player1States;
-//                    }
-//                    result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, prob1Candidates);
-//                } else {
-//                    // (1) max/max: compute prob0 using the game functions
-//                    result.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
-//
-//                    // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states.
-//                    storm::dd::Bdd<Type> candidates = game.getReachableStates() && !result.prob0Max.player1States;
-//                    if (previousQualitativeResult) {
-//                        candidates &= previousQualitativeResult.get().prob1Max.player1States;
-//                    }
-//                    storm::dd::Bdd<Type> prob1MaxMaxMdp = storm::utility::graph::performProb1E(game, transitionMatrixBdd, constraintStates, targetStates, candidates);
-//
-//                    // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation
-//                    result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, boost::make_optional(prob1MaxMaxMdp));
-//
-//                    // (4) max/min: compute prob0 using the game functions
-//                    result.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
-//
-//                    // (5) max/min: compute prob1 using the game functions, use prob1 from max/max as the candidate set
-//                    result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp));
-//                }
-//            } else {
-                result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy());
-                result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy());
-                result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy());
-                result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy());
-//            }
-            
-            STORM_LOG_TRACE("Qualitative precomputation completed.");
-            STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNumberOfSetBits()<< " 'no', " << result.prob1Min.player1States.getNumberOfSetBits() << " 'yes'.");
-            STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNumberOfSetBits() << " 'no', " << result.prob1Max.player1States.getNumberOfSetBits() << " 'yes'.");
+
+            result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair);
+            result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair);
+            result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair);
+            result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair);
+
+            STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNumberOfSetBits()<< " 'no', " << result.prob1Min.player1States.getNumberOfSetBits() << " 'yes'.");
+            STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNumberOfSetBits() << " 'no', " << result.prob1Max.player1States.getNumberOfSetBits() << " 'yes'.");
             
             return result;
         }
@@ -1003,9 +999,8 @@ namespace storm {
                 result.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
             }
             
-            STORM_LOG_TRACE("Qualitative precomputation completed.");
-            STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNonZeroCount() << " 'no', " << result.prob1Min.player1States.getNonZeroCount() << " 'yes'.");
-            STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNonZeroCount() << " 'no', " << result.prob1Max.player1States.getNonZeroCount() << " 'yes'.");
+            STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNonZeroCount() << " 'no', " << result.prob1Min.player1States.getNonZeroCount() << " 'yes'.");
+            STORM_LOG_DEBUG("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNonZeroCount() << " 'no', " << result.prob1Max.player1States.getNonZeroCount() << " 'yes'.");
             
             STORM_LOG_ASSERT(checkQualitativeStrategies(result, targetStates), "Qualitative strategies appear to be broken.");
             return result;

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -6,11 +6,13 @@
 #include "storm/storage/prism/Program.h"
 
 #include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Odd.h"
 
 #include "storm/storage/SymbolicModelDescription.h"
 
 #include "storm/abstraction/SymbolicQualitativeGameResult.h"
 #include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h"
+#include "storm/abstraction/ExplicitQuantitativeResult.h"
 
 #include "storm/logic/Bound.h"
 
@@ -40,9 +42,6 @@ namespace storm {
         class ExplicitQualitativeGameResult;
         class ExplicitQualitativeGameResultMinMax;
         
-        template<typename ValueType>
-        class ExplicitQuantitativeResult;
-
         template<typename ValueType>
         class ExplicitQuantitativeResultMinMax;
         
@@ -56,6 +55,18 @@ namespace storm {
         using storm::abstraction::SymbolicQualitativeGameResultMinMax;
         using storm::abstraction::ExplicitQualitativeGameResult;
         using storm::abstraction::ExplicitQualitativeGameResultMinMax;
+        using storm::abstraction::ExplicitQuantitativeResult;
+        using storm::abstraction::ExplicitQuantitativeResultMinMax;
+
+        namespace detail {
+            template<typename ValueType>
+            struct PreviousExplicitResult {
+                ExplicitQuantitativeResultMinMax<ValueType> values;
+                std::vector<uint64_t> minPlayer1Labels;
+                std::vector<uint64_t> maxPlayer1Labels;
+                storm::dd::Odd odd;
+            };
+        }
         
         template<storm::dd::DdType Type, typename ModelType>
         class GameBasedMdpModelChecker : public AbstractModelChecker<ModelType> {
@@ -75,7 +86,7 @@ namespace storm {
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(Environment const& env, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
-            
+    
         private:
             /*!
              * Performs the core part of the abstraction-refinement loop.
@@ -83,7 +94,7 @@ namespace storm {
             std::unique_ptr<CheckResult> performGameBasedAbstractionRefinement(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
             
             std::unique_ptr<CheckResult> performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<SymbolicQualitativeGameResultMinMax<Type>>& previousQualitativeResult, boost::optional<abstraction::SymbolicQuantitativeGameResult<Type, ValueType>>& previousMinQuantitativeResult);
-            std::unique_ptr<CheckResult> performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<ExplicitQualitativeGameResultMinMax>& previousQualitativeResult);
+            std::unique_ptr<CheckResult> performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<detail::PreviousExplicitResult<ValueType>>& previousResult);
 
             /*!
              * Retrieves the initial predicates for the abstraction.
@@ -101,7 +112,7 @@ namespace storm {
              */
             SymbolicQualitativeGameResultMinMax<Type> computeProb01States(boost::optional<SymbolicQualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
             
-            ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair);
+            ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<detail::PreviousExplicitResult<ValueType>> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair);
             
             void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;
             

src/storm/settings/modules/AbstractionSettings.cpp

@@ -24,6 +24,7 @@ namespace storm {
             const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant";
             const std::string AbstractionSettings::solveModeOptionName = "solve";
             const std::string AbstractionSettings::maximalAbstractionOptionName = "maxabs";
+            const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred";
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@@ -80,6 +81,11 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, rankRefinementPredicatesOptionName, true, "Sets whether to rank the refinement predicates if there are multiple.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
+                                             .setDefaultValueString("off").build())
+                                .build());
             }
             
             AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
@@ -166,6 +172,10 @@ namespace storm {
                 return this->getOption(maximalAbstractionOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool AbstractionSettings::isRankRefinementPredicatesSet() const {
+                return this->getOption(rankRefinementPredicatesOptionName).getArgumentByName("value").getValueAsString() == "on";
+            }
+            
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -116,6 +116,13 @@ namespace storm {
                  */
                 uint_fast64_t getMaximalAbstractionCount() const;
                 
+                /*
+                 * Determines whether refinement predicates are to be ranked.
+                 *
+                 * @return True iff the refinement predicates are to be ranked.
+                 */
+                bool isRankRefinementPredicatesSet() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -130,6 +137,7 @@ namespace storm {
                 const static std::string restrictToRelevantStatesOptionName;
                 const static std::string solveModeOptionName;
                 const static std::string maximalAbstractionOptionName;
+                const static std::string rankRefinementPredicatesOptionName;
             };
             
         }

src/storm/storage/SparseMatrix.cpp

@@ -970,6 +970,7 @@ namespace storm {
             // Copy over selected entries.
             rowGroupCount = 0;
             index_type rowCount = 0;
+            subEntries = 0;
             for (auto index : rowGroupConstraint) {
                 if (!this->hasTrivialRowGrouping()) {
                     matrixBuilder.newRowGroup(rowCount);
@@ -985,6 +986,7 @@ namespace storm {
                                 matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
                                 insertedDiagonalElement = true;
                             }
+                            ++subEntries;
                             matrixBuilder.addNextValue(rowCount, columnBitsSetBeforeIndex[it->getColumn()], it->getValue());
                         }
                     }

src/storm/storage/dd/Odd.cpp

@@ -90,6 +90,33 @@ namespace storm {
                 expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues);
             }
         }
+
+        void Odd::oldToNewIndex(storm::dd::Odd const& newOdd, std::function<void (uint64_t oldOffset, uint64_t newOffset)> const& callback) const {
+            STORM_LOG_ASSERT(this->getHeight() < newOdd.getHeight(), "Expected increase in height.");
+            oldToNewIndexRec(0, *this, 0, newOdd, callback);
+        }
+        
+        void Odd::oldToNewIndexRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::function<void (uint64_t oldOffset, uint64_t newOffset)> const& callback) {
+            if (oldOdd.getTotalOffset() == 0 || newOdd.getTotalOffset() == 0) {
+                return;
+            }
+            
+            if (oldOdd.isTerminalNode()) {
+                if (oldOdd.getThenOffset() != 0) {
+                    if (newOdd.isTerminalNode()) {
+                        if (newOdd.getThenOffset() != 0) {
+                            callback(oldOffset, newOffset);
+                        }
+                    } else {
+                        oldToNewIndexRec(oldOffset, oldOdd, newOffset, newOdd.getElseSuccessor(), callback);
+                        oldToNewIndexRec(oldOffset, oldOdd, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), callback);
+                    }
+                }
+            } else {
+                oldToNewIndexRec(oldOffset, oldOdd.getElseSuccessor(), newOffset, newOdd.getElseSuccessor(), callback);
+                oldToNewIndexRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), callback);
+            }
+        }
         
         void Odd::exportToDot(std::string const& filename) const {
             std::ofstream dotFile;

src/storm/storage/dd/Odd.h

@@ -5,6 +5,7 @@
 #include <map>
 #include <memory>
 #include <unordered_set>
+#include <functional>
 
 namespace storm {
     namespace storage {
@@ -116,6 +117,16 @@ namespace storm {
             template <typename ValueType>
             void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector<ValueType> const& oldValues, std::vector<ValueType>& newValues) const;
             
+            /*!
+             * Translates the indices of the old ODD to that of the new ODD by calling the callback for each old-new
+             * offset pair. Note that for each old offset, there may be multiple new offsets. The new ODD is expected
+             * to extend the old ODD by adding layers *at the bottom*.
+             *
+             * @param newOdd The new ODD to use.
+             * @param callback The callback function.
+             */
+            void oldToNewIndex(storm::dd::Odd const& newOdd, std::function<void (uint64_t oldOffset, uint64_t newOffset)> const& callback) const;
+            
             /*!
              * Exports the ODD in the dot format to the given file.
              *
@@ -155,6 +166,8 @@ namespace storm {
             template <typename ValueType>
             static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector<ValueType> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector<ValueType>& newValues);
             
+            static void oldToNewIndexRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::function<void (uint64_t oldOffset, uint64_t newOffset)> const& callback);
+            
             // The then- and else-nodes.
             std::shared_ptr<Odd> elseNode;
             std::shared_ptr<Odd> thenNode;

src/storm/storage/expressions/EquivalenceChecker.cpp

@@ -21,14 +21,26 @@ namespace storm {
         
         bool EquivalenceChecker::areEquivalent(storm::expressions::Expression const& first, storm::expressions::Expression const& second) {
             this->smtSolver->push();
-            this->smtSolver->add((first && !second) || (!first && second));
+            this->smtSolver->add(!storm::expressions::iff(first, second));
             bool equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat;
             this->smtSolver->pop();
             return equivalent;
         }
         
         bool EquivalenceChecker::areEquivalentModuloNegation(storm::expressions::Expression const& first, storm::expressions::Expression const& second) {
-            return this->areEquivalent(first, second) || this->areEquivalent(first, !second);
+            this->smtSolver->push();
+            this->smtSolver->add(!storm::expressions::iff(first, second));
+            bool equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat;
+            if (equivalent) {
+                this->smtSolver->pop();
+                return true;
+            }
+            this->smtSolver->pop();
+            this->smtSolver->push();
+            this->smtSolver->add(!storm::expressions::iff(first, !second));
+            equivalent = smtSolver->check() == storm::solver::SmtSolver::CheckResult::Unsat;
+            this->smtSolver->pop();
+            return equivalent;
         }
         
     }

src/storm/utility/graph.cpp

@@ -9,7 +9,7 @@
 #include "storm/storage/dd/Add.h"
 #include "storm/storage/dd/DdManager.h"
 
-#include "storm/abstraction/ExplicitGameStrategy.h"
+#include "storm/abstraction/ExplicitGameStrategyPair.h"
 #include "storm/storage/StronglyConnectedComponentDecomposition.h"
 
 #include "storm/models/symbolic/DeterministicModel.h"
@@ -1085,7 +1085,7 @@ namespace storm {
             }
 
             template <typename ValueType>
-            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy) {
+            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair) {
              
                 ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount()));
                 
@@ -1163,7 +1163,7 @@ namespace storm {
                 result.player2States.complement();
                 
                 // Generate player 1 strategy if required.
-                if (player1Strategy) {
+                if (strategyPair) {
                     for (auto player1State : result.player1States) {
                         if (player1Direction == storm::OptimizationDirection::Minimize) {
                             // At least one player 2 successor is a state with probability 0, find it.
@@ -1176,16 +1176,16 @@ namespace storm {
                                 }
                             }
                             STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0.");
-                            player1Strategy->setChoice(player1State, player2State);
+                            strategyPair->getPlayer1Strategy().setChoice(player1State, player2State);
                         } else {
                             // Since all player 2 successors are states with probability 0, just pick any.
-                            player1Strategy->setChoice(player1State, player1Groups[player1State]);
+                            strategyPair->getPlayer1Strategy().setChoice(player1State, player1Groups[player1State]);
                         }
                     }
                 }
 
                 // Generate player 2 strategy if required.
-                if (player2Strategy) {
+                if (strategyPair) {
                     for (auto player2State : result.player2States) {
                         if (player2Direction == storm::OptimizationDirection::Minimize) {
                             // At least one distribution only has successors with probability 0, find it.
@@ -1207,10 +1207,10 @@ namespace storm {
                             }
                             
                             STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0.");
-                            player2Strategy->setChoice(player2State, row);
+                            strategyPair->getPlayer2Strategy().setChoice(player2State, row);
                         } else {
                             // Since all player 1 successors are states with probability 0, just pick any.
-                            player2Strategy->setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]);
+                            strategyPair->getPlayer2Strategy().setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]);
                         }
                     }
                 }
@@ -1286,7 +1286,7 @@ namespace storm {
             }
             
             template <typename ValueType>
-            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates) {
+            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional<storm::storage::BitVector> const& player1Candidates) {
                 
                 // During the execution, the two state sets in the result hold the potential player 1/2 states.
                 ExplicitGameProb01Result result;
@@ -1349,8 +1349,8 @@ namespace storm {
                                 
                                 if (addPlayer2State) {
                                     player2Solution.set(player2Predecessor);
-                                    if (produceStrategiesInIteration && player2Strategy) {
-                                        player2Strategy->setChoice(player2Predecessor, validChoice);
+                                    if (produceStrategiesInIteration) {
+                                        strategyPair->getPlayer2Strategy().setChoice(player2Predecessor, validChoice);
                                     }
                                     
                                     // Check whether the addition of the player 2 state changes the state of the (single)
@@ -1377,8 +1377,8 @@ namespace storm {
                                         if (addPlayer1State) {
                                             player1Solution.set(player1Predecessor);
                                             
-                                            if (produceStrategiesInIteration && player1Strategy) {
-                                                player1Strategy->setChoice(player1Predecessor, validChoice);
+                                            if (produceStrategiesInIteration) {
+                                                strategyPair->getPlayer1Strategy().setChoice(player1Predecessor, validChoice);
                                             }
                                             
                                             stack.emplace_back(player1Predecessor);
@@ -1395,7 +1395,7 @@ namespace storm {
                         
                         // If we were asked to produce strategies, we propagate that by triggering another iteration.
                         // We only do this if at least one strategy will be produced.
-                        produceStrategiesInIteration = !produceStrategiesInIteration && (player1Strategy || player2Strategy);
+                        produceStrategiesInIteration = !produceStrategiesInIteration && strategyPair;
                     } else {
                         result.player1States = player1Solution;
                         result.player2States = player2Solution;
@@ -1680,9 +1680,9 @@ namespace storm {
 			template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
 #endif
             
-            template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy);
+            template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair);
             
-            template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates);
+            template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional<storm::storage::BitVector> const& player1Candidates);
             
             template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
             

src/storm/utility/graph.h

@@ -50,7 +50,7 @@ namespace storm {
     }
     
     namespace abstraction {
-        class ExplicitGameStrategy;
+        class ExplicitGameStrategyPair;
     }
     
     namespace utility {
@@ -651,13 +651,11 @@ namespace storm {
              * @param psiStates The psi states of the model.
              * @param player1Direction The optimization direction of player 1.
              * @param player2Direction The optimization direction of player 2.
-             * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices
-             * are written to this strategy.
-             * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices
+             * @param strategyPair If not null, player 1 and t2 strategies are synthesized and the corresponding choices
              * are written to this strategy.
              */
             template <typename ValueType>
-            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr);
+            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair = nullptr);
             
             /*!
              * Computes the set of states that have probability 1 given the strategies of the two players.
@@ -670,14 +668,12 @@ namespace storm {
              * @param psiStates The psi states of the model.
              * @param player1Direction The optimization direction of player 1.
              * @param player2Direction The optimization direction of player 2.
-             * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices
-             * are written to this strategy.
-             * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices
+             * @param strategyPair If not null, player 1 and t2 strategies are synthesized and the corresponding choices
              * are written to this strategy.
              * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered.
              */
             template <typename ValueType>
-            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr, boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
+            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair = nullptr, boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
             
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.