added decomposition to JANI abstractor, fixed wrong assertion

8 years ago · 16f3b06f53
15 changed files with 437 additions and 238 deletions
--- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp
+++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp
@ -23,17 +23,12 @@ namespace storm {
            using storm::settings::modules::AbstractionSettings;
            template <storm::dd::DdType DdType, typename ValueType>
            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) {
                bool allowInvalidSuccessorsInCommands = false;
                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
                    allowInvalidSuccessorsInCommands = true;
                }
            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) {
                // For each concrete command, we create an abstract counterpart.
                uint64_t edgeId = 0;
                for (auto const& edge : automaton.getEdges()) {
                    edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands);
                    edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition);
                    ++edgeId;
                }
            }
--- a/src/storm/abstraction/jani/AutomatonAbstractor.h
+++ b/src/storm/abstraction/jani/AutomatonAbstractor.h
@ -33,8 +33,9 @@ namespace storm {
                 * @param automaton The concrete automaton for which to build the abstraction.
                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                 * @param useDecomposition A flag indicating whether to use the decomposition during abstraction.
                 */
                AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy);
                AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
                AutomatonAbstractor(AutomatonAbstractor const&) = default;
                AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default;
--- a/src/storm/abstraction/jani/EdgeAbstractor.cpp
+++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp
@ -23,8 +23,8 @@ namespace storm {
    namespace abstraction {
        namespace jani {
            template <storm::dd::DdType DdType, typename ValueType>
            EdgeAbstractor<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) {
            EdgeAbstractor<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) {
                // Make the second component of relevant predicates have the right size.
                relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations());
@ -44,7 +44,7 @@ namespace storm {
                for (auto predicateIndex : predicates) {
                    localExpressionInformation.addExpression(predicateIndex);
                }
                // Next, we check whether there is work to be done by recomputing the relevant predicates and checking
                // whether they changed.
                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();
@ -72,6 +72,303 @@ namespace storm {
            template <storm::dd::DdType DdType, typename ValueType>
            void EdgeAbstractor<DdType, ValueType>::recomputeCachedBdd() {
                if (useDecomposition) {
                    recomputeCachedBddWithDecomposition();
                } else {
                    recomputeCachedBddWithoutDecomposition();
                }
            }
            template <storm::dd::DdType DdType, typename ValueType>
            void EdgeAbstractor<DdType, ValueType>::recomputeCachedBddWithDecomposition() {
                STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard() << " using the decomposition.");
                auto start = std::chrono::high_resolution_clock::now();
                // compute a decomposition of the command
                //  * start with all relevant blocks: blocks of assignment variables and variables in the rhs of assignments
                //  * go through all assignments of all updates and merge relevant blocks that are related via an assignment
                //  * repeat this until nothing changes anymore
                //  * the resulting blocks are the decomposition
                // Start by constructing the relevant blocks.
                std::set<uint64_t> allRelevantBlocks;
                std::map<storm::expressions::Variable, uint64_t> variableToBlockIndex;
                for (auto const& destination : edge.get().getDestinations()) {
                    for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
                        allRelevantBlocks.insert(localExpressionInformation.getBlockIndexOfVariable(assignment.getExpressionVariable()));
                        auto rhsVariableBlocks = localExpressionInformation.getBlockIndicesOfVariables(assignment.getAssignedExpression().getVariables());
                        allRelevantBlocks.insert(rhsVariableBlocks.begin(), rhsVariableBlocks.end());
                    }
                }
                STORM_LOG_TRACE("Found " << allRelevantBlocks.size() << " relevant block(s).");
                // Create a block partition.
                std::vector<std::set<uint64_t>> relevantBlockPartition;
                std::map<storm::expressions::Variable, uint64_t> variableToLocalBlockIndex;
                uint64_t index = 0;
                for (auto const& blockIndex : allRelevantBlocks) {
                    relevantBlockPartition.emplace_back(std::set<uint64_t>({blockIndex}));
                    for (auto const& variable : localExpressionInformation.getVariableBlockWithIndex(blockIndex)) {
                        variableToLocalBlockIndex[variable] = index;
                    }
                    ++index;
                }
                // Merge all blocks that are related via the right-hand side of assignments.
                for (auto const& destination : edge.get().getDestinations()) {
                    for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
                        std::set<storm::expressions::Variable> rhsVariables = assignment.getAssignedExpression().getVariables();
                        if (!rhsVariables.empty()) {
                            uint64_t blockToKeep = variableToLocalBlockIndex.at(*rhsVariables.begin());
                            for (auto const& variable : rhsVariables) {
                                uint64_t block = variableToLocalBlockIndex.at(variable);
                                if (block != blockToKeep) {
                                    for (auto const& blockIndex : relevantBlockPartition[block]) {
                                        for (auto const& variable : localExpressionInformation.getVariableBlockWithIndex(blockIndex)) {
                                            variableToLocalBlockIndex[variable] = blockToKeep;
                                        }
                                    }
                                    relevantBlockPartition[blockToKeep].insert(relevantBlockPartition[block].begin(), relevantBlockPartition[block].end());
                                    relevantBlockPartition[block].clear();
                                }
                            }
                        }
                    }
                }
                // Proceed by relating the blocks via assignment-variables and the expressions of their assigned expressions.
                bool changed = false;
                do {
                    changed = false;
                    for (auto const& destination : edge.get().getDestinations()) {
                        for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
                            std::set<storm::expressions::Variable> rhsVariables = assignment.getAssignedExpression().getVariables();
                            if (!rhsVariables.empty()) {
                                storm::expressions::Variable const& representativeVariable = *rhsVariables.begin();
                                uint64_t representativeBlock = variableToLocalBlockIndex.at(representativeVariable);
                                uint64_t assignmentVariableBlock = variableToLocalBlockIndex.at(assignment.getExpressionVariable());
                                // If the blocks are different, we merge them now
                                if (assignmentVariableBlock != representativeBlock) {
                                    changed = true;
                                    for (auto const& blockIndex : relevantBlockPartition[assignmentVariableBlock]) {
                                        for (auto const& variable : localExpressionInformation.getVariableBlockWithIndex(blockIndex)) {
                                            variableToLocalBlockIndex[variable] = representativeBlock;
                                        }
                                    }
                                    relevantBlockPartition[representativeBlock].insert(relevantBlockPartition[assignmentVariableBlock].begin(), relevantBlockPartition[assignmentVariableBlock].end());
                                    relevantBlockPartition[assignmentVariableBlock].clear();
                                }
                            }
                        }
                    }
                } while (changed);
                // Now remove all blocks that are empty and obtain the partition.
                std::vector<std::set<uint64_t>> cleanedRelevantBlockPartition;
                for (auto& element : relevantBlockPartition) {
                    if (!element.empty()) {
                        cleanedRelevantBlockPartition.emplace_back(std::move(element));
                    }
                }
                relevantBlockPartition = std::move(cleanedRelevantBlockPartition);
                // if the decomposition has size 1, use the plain technique from before
                if (relevantBlockPartition.size() == 1) {
                    STORM_LOG_TRACE("Relevant block partition size is one, falling back to regular computation.");
                    recomputeCachedBddWithoutDecomposition();
                } else {
                    std::set<storm::expressions::Variable> variablesContainedInGuard = edge.get().getGuard().getVariables();
                    // Check whether we need to enumerate the guard. This is the case if the blocks related by the guard
                    // are not contained within a single block of our decomposition.
                    bool enumerateAbstractGuard = true;
                    std::set<uint64_t> guardBlocks = localExpressionInformation.getBlockIndicesOfVariables(variablesContainedInGuard);
                    for (auto const& block : relevantBlockPartition) {
                        bool allContained = true;
                        for (auto const& guardBlock : guardBlocks) {
                            if (block.find(guardBlock) == block.end()) {
                                allContained = false;
                                break;
                            }
                        }
                        if (allContained) {
                            enumerateAbstractGuard = false;
                        }
                    }
                    uint64_t numberOfSolutions = 0;
                    if (enumerateAbstractGuard) {
                        // otherwise, enumerate the abstract guard so we do this only once
                        std::set<uint64_t> relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard);
                        std::vector<storm::expressions::Variable> guardDecisionVariables;
                        std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> guardVariablesAndPredicates;
                        for (auto const& element : relevantPredicatesAndVariables.first) {
                            if (relatedGuardPredicates.find(element.second) != relatedGuardPredicates.end()) {
                                guardDecisionVariables.push_back(element.first);
                                guardVariablesAndPredicates.push_back(element);
                            }
                        }
                        abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero();
                        smtSolver->allSat(guardDecisionVariables, [this,&guardVariablesAndPredicates,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) {
                            abstractGuard |= getSourceStateBdd(model, guardVariablesAndPredicates);
                            ++numberOfSolutions;
                            return true;
                        });
                        STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " for abstract guard.");
                        // now that we have the abstract guard, we can add it as an assertion to the solver before enumerating
                        // the other solutions.
                        // Create a new backtracking point before adding the guard.
                        smtSolver->push();
                        // Create the guard constraint.
                        std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<uint_fast64_t, storm::expressions::Variable>> result = abstractGuard.toExpression(this->getAbstractionInformation().getExpressionManager());
                        // Then add it to the solver.
                        for (auto const& expression : result.first) {
                            smtSolver->add(expression);
                        }
                        // Finally associate the level variables with the predicates.
                        for (auto const& indexVariablePair : result.second) {
                            smtSolver->add(storm::expressions::iff(indexVariablePair.second, this->getAbstractionInformation().getPredicateForDdVariableIndex(indexVariablePair.first)));
                        }
                    }
                    // then enumerate the solutions for each of the blocks of the decomposition
                    uint64_t usedNondeterminismVariables = 0;
                    uint64_t blockCounter = 0;
                    std::vector<storm::dd::Bdd<DdType>> blockBdds;
                    for (auto const& block : relevantBlockPartition) {
                        std::set<uint64_t> relevantPredicates;
                        for (auto const& innerBlock : block) {
                            relevantPredicates.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end());
                        }
                        std::vector<storm::expressions::Variable> transitionDecisionVariables;
                        std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> sourceVariablesAndPredicates;
                        for (auto const& element : relevantPredicatesAndVariables.first) {
                            if (relevantPredicates.find(element.second) != relevantPredicates.end()) {
                                transitionDecisionVariables.push_back(element.first);
                                sourceVariablesAndPredicates.push_back(element);
                            }
                        }
                        std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>> destinationVariablesAndPredicates;
                        for (uint64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) {
                            destinationVariablesAndPredicates.emplace_back();
                            for (auto const& assignment : edge.get().getDestination(destinationIndex).getOrderedAssignments().getAllAssignments()) {
                                uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getExpressionVariable());
                                std::set<uint64_t> const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex);
                                if (block.find(assignmentVariableBlockIndex) != block.end()) {
                                    for (auto const& element : relevantPredicatesAndVariables.second[destinationIndex]) {
                                        if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) {
                                            destinationVariablesAndPredicates.back().push_back(element);
                                            transitionDecisionVariables.push_back(element.first);
                                        }
                                    }
                                }
                            }
                        }
                        std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
                        numberOfSolutions = 0;
                        smtSolver->allSat(transitionDecisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions,&sourceVariablesAndPredicates,&destinationVariablesAndPredicates] (storm::solver::SmtSolver::ModelReference const& model) {
                            sourceToDistributionsMap[getSourceStateBdd(model, sourceVariablesAndPredicates)].push_back(getDistributionBdd(model, destinationVariablesAndPredicates));
                            ++numberOfSolutions;
                            return true;
                        });
                        STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions for block " << blockCounter << ".");
                        numberOfSolutions = 0;
                        // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
                        // need to encode the nondeterminism.
                        uint_fast64_t maximalNumberOfChoices = 0;
                        for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
                            maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast<uint_fast64_t>(sourceDistributionsPair.second.size()));
                        }
                        // We now compute how many variables we need to encode the choices. We add one to the maximal number of
                        // choices to account for a possible transition to a bottom state.
                        uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + 1)));
                        // Finally, build overall result.
                        storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();
                        uint_fast64_t sourceStateIndex = 0;
                        for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
                            STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
                            STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty.");
                            // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice.
                            uint_fast64_t distributionIndex = 1;
                            storm::dd::Bdd<DdType> allDistributions = this->getAbstractionInformation().getDdManager().getBddZero();
                            for (auto const& distribution : sourceDistributionsPair.second) {
                                allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, usedNondeterminismVariables, usedNondeterminismVariables + numberOfVariablesNeeded);
                                ++distributionIndex;
                                STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty.");
                            }
                            resultBdd |= sourceDistributionsPair.first && allDistributions;
                            ++sourceStateIndex;
                            STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty.");
                        }
                        usedNondeterminismVariables += numberOfVariablesNeeded;
                        blockBdds.push_back(resultBdd);
                        ++blockCounter;
                    }
                    if (enumerateAbstractGuard) {
                        smtSolver->pop();
                    }
                    // multiply the results
                    storm::dd::Bdd<DdType> resultBdd = getAbstractionInformation().getDdManager().getBddOne();
                    for (auto const& blockBdd : blockBdds) {
                        resultBdd &= blockBdd;
                    }
                    // if we did not explicitly enumerate the guard, we can construct it from the result BDD.
                    if (!enumerateAbstractGuard) {
                        std::set<storm::expressions::Variable> allVariables(getAbstractionInformation().getSuccessorVariables());
                        auto player2Variables = getAbstractionInformation().getPlayer2VariableSet(usedNondeterminismVariables);
                        allVariables.insert(player2Variables.begin(), player2Variables.end());
                        auto auxVariables = getAbstractionInformation().getAuxVariableSet(0, getAbstractionInformation().getAuxVariableCount());
                        allVariables.insert(auxVariables.begin(), auxVariables.end());
                        std::set<storm::expressions::Variable> variablesToAbstract;
                        std::set_intersection(allVariables.begin(), allVariables.end(), resultBdd.getContainedMetaVariables().begin(), resultBdd.getContainedMetaVariables().end(), std::inserter(variablesToAbstract, variablesToAbstract.begin()));
                        abstractGuard = resultBdd.existsAbstract(variablesToAbstract);
                    } else {
                        // Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks.
                        resultBdd &= abstractGuard;
                    }
                    // multiply with missing identities
                    resultBdd &= computeMissingIdentities();
                    // cache and return result
                    resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount());
                    // Cache the result.
                    cachedDd = GameBddResult<DdType>(resultBdd, usedNondeterminismVariables);
                    auto end = std::chrono::high_resolution_clock::now();
                    STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                    forceRecomputation = false;
                }
            }
            template <storm::dd::DdType DdType, typename ValueType>
            void EdgeAbstractor<DdType, ValueType>::recomputeCachedBddWithoutDecomposition() {
                STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard());
                auto start = std::chrono::high_resolution_clock::now();
@ -79,7 +376,7 @@ namespace storm {
                std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
                uint64_t numberOfSolutions = 0;
                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) {
                    sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model));
                    sourceToDistributionsMap[getSourceStateBdd(model, relevantPredicatesAndVariables.first)].push_back(getDistributionBdd(model, relevantPredicatesAndVariables.second));
                    ++numberOfSolutions;
                    return true;
                });
@ -152,10 +449,8 @@ namespace storm {
                    assignedVariables.insert(assignedVariable);
                }
                if (!allowInvalidSuccessors) {
                    auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
                    result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
                }
                auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
                result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
                return result;
            }
@ -163,7 +458,7 @@ namespace storm {
            template <storm::dd::DdType DdType, typename ValueType>
            std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> EdgeAbstractor<DdType, ValueType>::computeRelevantPredicates() const {
                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
                // To start with, all predicates related to the guard are relevant source predicates.
                result.first = localExpressionInformation.getExpressionsUsingVariables(edge.get().getGuard().getVariables());
@ -221,9 +516,9 @@ namespace storm {
            }
            template <storm::dd::DdType DdType, typename ValueType>
            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& variablePredicates) const {
                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
                for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
                for (auto const& variableIndexPair : variablePredicates) {
                    if (model.getBooleanValue(variableIndexPair.first)) {
                        result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                    } else {
@ -236,20 +531,20 @@ namespace storm {
            }
            template <storm::dd::DdType DdType, typename ValueType>
            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>> const& variablePredicates) const {
                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
                for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) {
                for (uint_fast64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) {
                    storm::dd::Bdd<DdType> updateBdd = this->getAbstractionInformation().getDdManager().getBddOne();
                    // Translate block variables for this update into a successor block.
                    for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) {
                    for (auto const& variableIndexPair : variablePredicates[destinationIndex]) {
                        if (model.getBooleanValue(variableIndexPair.first)) {
                            updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
                        } else {
                            updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
                        }
                        updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
                        updateBdd &= this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
                    }
                    result |= updateBdd;
@ -276,27 +571,17 @@ namespace storm {
                    auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end();
                    storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
                    if (allowInvalidSuccessors) {
                        for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                            if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) {
                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                            } else {
                                ++updateRelevantIt;
                            }
                        }
                    } else {
                        auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
                        auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
                        // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
                        // relevant successor predicates for any update.
                        for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
                            // If the predicates do not match, there is a predicate missing, so we need to add its identity.
                            if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
                            } else {
                                ++updateRelevantIt;
                            }
                    auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
                    auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
                    // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
                    // relevant successor predicates for any update.
                    for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
                        // If the predicates do not match, there is a predicate missing, so we need to add its identity.
                        if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
                            updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
                        } else {
                            ++updateRelevantIt;
                        }
                    }
@ -308,34 +593,21 @@ namespace storm {
            template <storm::dd::DdType DdType, typename ValueType>
            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::computeMissingGlobalIdentities() const {
                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
                if (allowInvalidSuccessors) {
                    auto allRelevantIt = allRelevantPredicates.cbegin();
                    auto allRelevantIte = allRelevantPredicates.cend();
                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                        if (allRelevantIt == allRelevantIte || *allRelevantIt != predicateIndex) {
                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                        } else {
                            ++allRelevantIt;
                        }
                    }
                } else {
                    auto relevantIt = relevantPredicatesAndVariables.first.begin();
                    auto relevantIte = relevantPredicatesAndVariables.first.end();
                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                        if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                        } else {
                            ++relevantIt;
                        }
                auto relevantIt = relevantPredicatesAndVariables.first.begin();
                auto relevantIte = relevantPredicatesAndVariables.first.end();
                for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                    if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
                        result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                    } else {
                        ++relevantIt;
                    }
                }
                return result;
            }
            template <storm::dd::DdType DdType, typename ValueType>
            GameBddResult<DdType> EdgeAbstractor<DdType, ValueType>::abstract() {
                if (forceRecomputation) {
@ -351,7 +623,7 @@ namespace storm {
            BottomStateResult<DdType> EdgeAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
                STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard());
                BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
                // If the guard of this edge is a predicate, there are not bottom states/transitions.
                if (skipBottomStates) {
                    STORM_LOG_TRACE("Skipping bottom state computation for this edge.");
@ -367,7 +639,7 @@ namespace storm {
                if (result.states.isZero()) {
                    skipBottomStates = true;
                }
                // 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);
@ -408,7 +680,7 @@ namespace storm {
            template class EdgeAbstractor<storm::dd::DdType::CUDD, double>;
            template class EdgeAbstractor<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL
 			template class EdgeAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
            template class EdgeAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 #endif
        }
    }
--- a/src/storm/abstraction/jani/EdgeAbstractor.h
+++ b/src/storm/abstraction/jani/EdgeAbstractor.h
@ -56,9 +56,9 @@ namespace storm {
                 * @param edge The concrete edge for which to build the abstraction.
                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                 * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors.
                 * @param useDecomposition A flag indicating whether to use an edge decomposition during abstraction.
                 */
                EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors);
                EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
                /*!
                 * Refines the abstract edge with the given predicates.
@ -149,7 +149,7 @@ namespace storm {
                 * @param model The model to translate.
                 * @return The source state encoded as a DD.
                 */
                storm::dd::Bdd<DdType> getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const;
                storm::dd::Bdd<DdType> getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& variablePredicates) const;
                /*!
                 * Translates the given model to a distribution over successor states.
@ -157,13 +157,23 @@ namespace storm {
                 * @param model The model to translate.
                 * @return The source state encoded as a DD.
                 */
                storm::dd::Bdd<DdType> getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const;
                storm::dd::Bdd<DdType> getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>> const& variablePredicates) const;
                /*!
                 * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change.
                 */
                void recomputeCachedBdd();
                /*!
                 * Recomputes the cached BDD without the decomposition\.
                 */
                void recomputeCachedBddWithoutDecomposition();
                /*!
                 * Recomputes the cached BDD using the decomposition.
                 */
                void recomputeCachedBddWithDecomposition();
                /*!
                 * Computes the missing state identities.
                 *
@ -232,11 +242,9 @@ namespace storm {
                // All relevant decision variables over which to perform AllSat.
                std::vector<storm::expressions::Variable> decisionVariables;
                // A flag indicating whether it is allowed to enumerate invalid successors. Invalid successors may be
                // enumerated if the predicates that are (indirectly) related to an assignment variable are not
                // considered as source predicates.
                bool allowInvalidSuccessors;
                // A flag indicating whether to use the decomposition when abstracting.
                bool useDecomposition;
                // A flag indicating whether the computation of bottom states can be skipped (for example, if the bottom
                // states become empty at some point).
                bool skipBottomStates;
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
@ -31,7 +31,7 @@ namespace storm {
            using storm::settings::modules::AbstractionSettings;
            template <storm::dd::DdType DdType, typename ValueType>
            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false), invalidBlockDetectionStrategy(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getInvalidBlockDetectionStrategy()) {
            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) {
                // For now, we assume that there is a single module. If the program has more than one module, it needs
                // to be flattened before the procedure.
@ -60,8 +60,9 @@ namespace storm {
                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
                // For each module of the concrete program, we create an abstract counterpart.
                bool useDecomposition = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseDecompositionSet();
                for (auto const& automaton : model.getAutomata()) {
                    automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy);
                    automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition);
                }
                // Retrieve the edge-update probability ADD, so we can multiply it with the abstraction BDD later.
@ -136,15 +137,6 @@ namespace storm {
                // As long as there is only one module, we only build its game representation.
                GameBddResult<DdType> game = automata.front().abstract();
                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
                    auto validBlockStart = std::chrono::high_resolution_clock::now();
                    storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
                    // Cut away all invalid successor blocks.
                    game.bdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs());
                    auto validBlockEnd = std::chrono::high_resolution_clock::now();
                    STORM_LOG_DEBUG("Global invalid block detection completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(validBlockEnd - validBlockStart).count() << "ms.");
                }
                // 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);
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
+++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
@ -158,9 +158,6 @@ namespace storm {
                // A flag storing whether a refinement was performed.
                bool refinementPerformed;
                // The strategy to use for detecting invalid blocks.
                storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy;
            };
        }
    }
--- a/src/storm/abstraction/prism/CommandAbstractor.cpp
+++ b/src/storm/abstraction/prism/CommandAbstractor.cpp
@ -23,8 +23,8 @@ namespace storm {
    namespace abstraction {
        namespace prism {
            template <storm::dd::DdType DdType, typename ValueType>
            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory) {
            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory) {
                // Make the second component of relevant predicates have the right size.
                relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@ -44,7 +44,7 @@ namespace storm {
                for (auto predicateIndex : predicates) {
                    localExpressionInformation.addExpression(predicateIndex);
                }
                // Next, we check whether there is work to be done by recomputing the relevant predicates and checking
                // whether they changed.
                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();
@ -69,12 +69,21 @@ namespace storm {
            std::map<storm::expressions::Variable, storm::expressions::Expression> CommandAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t auxiliaryChoice) const {
                return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap();
            }
            template <storm::dd::DdType DdType, typename ValueType>
            void CommandAbstractor<DdType, ValueType>::recomputeCachedBddUsingDecomposition() {
            void CommandAbstractor<DdType, ValueType>::recomputeCachedBdd() {
                if (useDecomposition) {
                    recomputeCachedBddWithDecomposition();
                } else {
                    recomputeCachedBddWithoutDecomposition();
                }
            }
            template <storm::dd::DdType DdType, typename ValueType>
            void CommandAbstractor<DdType, ValueType>::recomputeCachedBddWithDecomposition() {
                STORM_LOG_TRACE("Recomputing BDD for command " << command.get() << " using the decomposition.");
                auto start = std::chrono::high_resolution_clock::now();
                // compute a decomposition of the command
                //  * start with all relevant blocks: blocks of assignment variables and variables in the rhs of assignments
                //  * go through all assignments of all updates and merge relevant blocks that are related via an assignment
@ -87,13 +96,13 @@ namespace storm {
                for (auto const& update : command.get().getUpdates()) {
                    for (auto const& assignment : update.getAssignments()) {
                        allRelevantBlocks.insert(localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()));
                        auto rhsVariableBlocks = localExpressionInformation.getBlockIndicesOfVariables(assignment.getExpression().getVariables());
                        allRelevantBlocks.insert(rhsVariableBlocks.begin(), rhsVariableBlocks.end());
                    }
                }
                STORM_LOG_TRACE("Found " << allRelevantBlocks.size() << " relevant block(s).");
                // Create a block partition.
                std::vector<std::set<uint64_t>> relevantBlockPartition;
                std::map<storm::expressions::Variable, uint64_t> variableToLocalBlockIndex;
@ -110,7 +119,7 @@ namespace storm {
                for (auto const& update : command.get().getUpdates()) {
                    for (auto const& assignment : update.getAssignments()) {
                        std::set<storm::expressions::Variable> rhsVariables = assignment.getExpression().getVariables();
                        if (!rhsVariables.empty()) {
                            uint64_t blockToKeep = variableToLocalBlockIndex.at(*rhsVariables.begin());
                            for (auto const& variable : rhsVariables) {
@ -172,7 +181,7 @@ namespace storm {
                // if the decomposition has size 1, use the plain technique from before
                if (relevantBlockPartition.size() == 1) {
                    STORM_LOG_TRACE("Relevant block partition size is one, falling back to regular computation.");
                    recomputeCachedBdd();
                    recomputeCachedBddWithoutDecomposition();
                } else {
                    std::set<storm::expressions::Variable> variablesContainedInGuard = command.get().getGuardExpression().getVariables();
@ -192,9 +201,9 @@ namespace storm {
                            enumerateAbstractGuard = false;
                        }
                    }
                    uint64_t numberOfSolutions = 0;
                    if (enumerateAbstractGuard) {
                        // otherwise, enumerate the abstract guard so we do this only once
                        std::set<uint64_t> relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard);
@ -243,7 +252,7 @@ namespace storm {
                        for (auto const& innerBlock : block) {
                            relevantPredicates.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end());
                        }
                        std::vector<storm::expressions::Variable> transitionDecisionVariables;
                        std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> sourceVariablesAndPredicates;
                        for (auto const& element : relevantPredicatesAndVariables.first) {
@ -269,7 +278,7 @@ namespace storm {
                                }
                            }
                        }
                        std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
                        numberOfSolutions = 0;
                        smtSolver->allSat(transitionDecisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions,&sourceVariablesAndPredicates,&destinationVariablesAndPredicates] (storm::solver::SmtSolver::ModelReference const& model) {
@ -279,21 +288,21 @@ namespace storm {
                        });
                        STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions for block " << blockCounter << ".");
                        numberOfSolutions = 0;
                        // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
                        // need to encode the nondeterminism.
                        uint_fast64_t maximalNumberOfChoices = 0;
                        for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
                            maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast<uint_fast64_t>(sourceDistributionsPair.second.size()));
                        }
                        // We now compute how many variables we need to encode the choices. We add one to the maximal number of
                        // choices to account for a possible transition to a bottom state.
                        uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + 1)));
                        // Finally, build overall result.
                        storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();
                        uint_fast64_t sourceStateIndex = 0;
                        for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
                            STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
@ -311,12 +320,14 @@ namespace storm {
                            STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty.");
                        }
                        usedNondeterminismVariables += numberOfVariablesNeeded;
                        blockBdds.push_back(resultBdd);
                        ++blockCounter;
                    }
                    smtSolver->pop();
                    if (enumerateAbstractGuard) {
                        smtSolver->pop();
                    }
                    // multiply the results
                    storm::dd::Bdd<DdType> resultBdd = getAbstractionInformation().getDdManager().getBddOne();
@ -357,7 +368,7 @@ namespace storm {
            }
            template <storm::dd::DdType DdType, typename ValueType>
            void CommandAbstractor<DdType, ValueType>::recomputeCachedBdd() {
            void CommandAbstractor<DdType, ValueType>::recomputeCachedBddWithoutDecomposition() {
                STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
                auto start = std::chrono::high_resolution_clock::now();
@ -390,7 +401,7 @@ namespace storm {
                    if (!skipBottomStates) {
                        abstractGuard |= sourceDistributionsPair.first;
                    }
                    STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
                    STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty.");
                    // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice.
@ -436,10 +447,8 @@ namespace storm {
                    assignedVariables.insert(assignedVariable);
                }
                if (!allowInvalidSuccessors) {
                    auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
                    result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
                }
                auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
                result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
                return result;
            }
@ -447,7 +456,7 @@ namespace storm {
            template <storm::dd::DdType DdType, typename ValueType>
            std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> CommandAbstractor<DdType, ValueType>::computeRelevantPredicates() const {
                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
                // To start with, all predicates related to the guard are relevant source predicates.
                result.first = localExpressionInformation.getRelatedExpressions(command.get().getGuardExpression().getVariables());
@ -525,7 +534,7 @@ namespace storm {
                for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
                    storm::dd::Bdd<DdType> updateBdd = this->getAbstractionInformation().getDdManager().getBddOne();
                    // Translate block variables for this update into a successor block.
                    for (auto const& variableIndexPair : variablePredicates[updateIndex]) {
                        if (model.getBooleanValue(variableIndexPair.first)) {
@ -560,27 +569,17 @@ namespace storm {
                    auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end();
                    storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
                    if (allowInvalidSuccessors) {
                        for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                            if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) {
                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                            } else {
                                ++updateRelevantIt;
                            }
                        }
                    } else {
                        auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
                        auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
                        // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
                        // relevant successor predicates for any update.
                        for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
                            // If the predicates do not match, there is a predicate missing, so we need to add its identity.
                            if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
                            } else {
                                ++updateRelevantIt;
                            }
                    auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
                    auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
                    // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
                    // relevant successor predicates for any update.
                    for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
                        // If the predicates do not match, there is a predicate missing, so we need to add its identity.
                        if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
                            updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
                        } else {
                            ++updateRelevantIt;
                        }
                    }
@ -592,48 +591,31 @@ namespace storm {
            template <storm::dd::DdType DdType, typename ValueType>
            storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingGlobalIdentities() const {
                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
                if (allowInvalidSuccessors) {
                    auto allRelevantIt = allRelevantPredicates.cbegin();
                    auto allRelevantIte = allRelevantPredicates.cend();
                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                        if (allRelevantIt == allRelevantIte || *allRelevantIt != predicateIndex) {
                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                        } else {
                            ++allRelevantIt;
                        }
                    }
                } else {
                    auto relevantIt = relevantPredicatesAndVariables.first.begin();
                    auto relevantIte = relevantPredicatesAndVariables.first.end();
                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                        if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                        } else {
                            ++relevantIt;
                        }
                auto relevantIt = relevantPredicatesAndVariables.first.begin();
                auto relevantIte = relevantPredicatesAndVariables.first.end();
                for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
                    if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
                        result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
                    } else {
                        ++relevantIt;
                    }
                }
                return result;
            }
            template <storm::dd::DdType DdType, typename ValueType>
            GameBddResult<DdType> CommandAbstractor<DdType, ValueType>::abstract() {
                if (forceRecomputation) {
                    if (useDecomposition) {
                        this->recomputeCachedBddUsingDecomposition();
                    } else {
                        this->recomputeCachedBdd();
                    }
                    this->recomputeCachedBdd();
                } else {
                    cachedDd.bdd &= computeMissingGlobalIdentities();
                }
                STORM_LOG_TRACE("Command produces " << cachedDd.bdd.getNonZeroCount() << " transitions.");
                return cachedDd;
            }
@ -641,7 +623,7 @@ namespace storm {
            BottomStateResult<DdType> CommandAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
                STORM_LOG_TRACE("Computing bottom state transitions of command " << command.get());
                BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
                // If the guard of this command is a predicate, there are not bottom states/transitions.
                if (skipBottomStates) {
                    STORM_LOG_TRACE("Skipping bottom state computation for this command.");
@ -657,7 +639,7 @@ namespace storm {
                if (result.states.isZero()) {
                    skipBottomStates = true;
                }
                // 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);
@ -698,7 +680,7 @@ namespace storm {
            template class CommandAbstractor<storm::dd::DdType::CUDD, double>;
            template class CommandAbstractor<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL
 			template class CommandAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
            template class CommandAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 #endif
        }
    }
--- a/src/storm/abstraction/prism/CommandAbstractor.h
+++ b/src/storm/abstraction/prism/CommandAbstractor.h
@ -54,10 +54,9 @@ namespace storm {
                 * @param command The concrete command for which to build the abstraction.
                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                 * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors.
                 * @param useDecomposition A flag indicating whether to use the decomposition during abstraction.
                 */
                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors, bool useDecomposition);
                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
                /*!
                 * Refines the abstract command with the given predicates.
@ -164,9 +163,14 @@ namespace storm {
                void recomputeCachedBdd();
                /*!
                 * Recomputes the cached BDD using a decomposition. This needs to be triggered if any relevant predicates change.
                 * Recomputes the cached BDD without using the decomposition.
                 */
                void recomputeCachedBddUsingDecomposition();
                void recomputeCachedBddWithoutDecomposition();
                /*!
                 * Recomputes the cached BDD using th decomposition.
                 */
                void recomputeCachedBddWithDecomposition();
                /*!
                 * Computes the missing state identities.
@ -233,11 +237,6 @@ namespace storm {
                // All relevant decision variables over which to perform AllSat.
                std::vector<storm::expressions::Variable> decisionVariables;
                // A flag indicating whether it is allowed to enumerate invalid successors. Invalid successors may be
                // enumerated if the predicates that are (indirectly) related to an assignment variable are not
                // considered as source predicates.
                bool allowInvalidSuccessors;
                // A flag indicating whether to use the decomposition when abstracting.
                bool useDecomposition;
--- a/src/storm/abstraction/prism/ModuleAbstractor.cpp
+++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp
@ -23,16 +23,11 @@ namespace storm {
            using storm::settings::modules::AbstractionSettings;
            template <storm::dd::DdType DdType, typename ValueType>
            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
                bool allowInvalidSuccessorsInCommands = false;
                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
                    allowInvalidSuccessorsInCommands = true;
                }
            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
                // For each concrete command, we create an abstract counterpart.
                for (auto const& command : module.getCommands()) {
                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands, useDecomposition);
                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition);
                }
            }
--- a/src/storm/abstraction/prism/ModuleAbstractor.h
+++ b/src/storm/abstraction/prism/ModuleAbstractor.h
@ -36,10 +36,9 @@ namespace storm {
                 * @param module The concrete module for which to build the abstraction.
                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                 * @param invalidBlockDetectionStrategy The strategy to use for detecting invalid blocks.
                 * @param useDecomposition A flag that governs whether to use the decomposition in the abstraction.
                 */
                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy, bool useDecomposition);
                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition);
                ModuleAbstractor(ModuleAbstractor const&) = default;
                ModuleAbstractor& operator=(ModuleAbstractor const&) = default;
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
@ -33,7 +33,7 @@ namespace storm {
            template <storm::dd::DdType DdType, typename ValueType>
            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program,
                                                                std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory)
            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, {program.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false), invalidBlockDetectionStrategy(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getInvalidBlockDetectionStrategy()) {
            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager(), program.getAllExpressionVariables(), smtSolverFactory->create(program.getManager())), modules(), initialStateAbstractor(abstractionInformation, {program.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) {
                // For now, we assume that there is a single module. If the program has more than one module, it needs
                // to be flattened before the procedure.
@ -64,7 +64,7 @@ namespace storm {
                // For each module of the concrete program, we create an abstract counterpart.
                bool useDecomposition = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseDecompositionSet();
                for (auto const& module : program.getModules()) {
                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy, useDecomposition);
                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition);
                }
                // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
@ -138,16 +138,7 @@ namespace storm {
            std::unique_ptr<MenuGame<DdType, ValueType>> PrismMenuGameAbstractor<DdType, ValueType>::buildGame() {
                // As long as there is only one module, we only build its game representation.
                GameBddResult<DdType> game = modules.front().abstract();
                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
                    auto validBlockStart = std::chrono::high_resolution_clock::now();
                    storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
                    // Cut away all invalid successor blocks.
                    game.bdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs());
                    auto validBlockEnd = std::chrono::high_resolution_clock::now();
                    STORM_LOG_DEBUG("Global invalid block detection completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(validBlockEnd - validBlockStart).count() << "ms.");
                }
                // 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);
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
@ -158,9 +158,6 @@ namespace storm {
                // A flag storing whether a refinement was performed.
                bool refinementPerformed;
                // The strategy to use for detecting invalid blocks.
                storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy;
            };
        }
    }
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@ -269,7 +269,7 @@ namespace storm {
                // Construct an ADD holding the initial values of initial states and check it for validity.
                storm::dd::Add<Type, ValueType> initialStateValueAdd = initialStatesAdd * result.values;
                // For min, we can only require a non-zero count of *at most* one, because the result may actually be 0.
                STORM_LOG_ASSERT((!min || initialStateValueAdd.getNonZeroCount() == 1) && (min || initialStateValueAdd.getNonZeroCount() <= 1), "Wrong number of results for initial states. Expected " << (min ? "<= 1" : "1") << ", but got " << initialStateValueAdd.getNonZeroCount() << ".");
                STORM_LOG_ASSERT((!min && initialStateValueAdd.getNonZeroCount() == 1) || (min && initialStateValueAdd.getNonZeroCount() <= 1), "Wrong number of results for initial states. Expected " << (min ? "<= 1" : "1") << ", but got " << initialStateValueAdd.getNonZeroCount() << ".");
                result.initialStateValue = result.initialStateValue = initialStateValueAdd.getMax();
                result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy);
--- a/src/storm/settings/modules/AbstractionSettings.cpp
+++ b/src/storm/settings/modules/AbstractionSettings.cpp
@ -19,7 +19,6 @@ namespace storm {
            const std::string AbstractionSettings::splitAllOptionName = "split-all";
            const std::string AbstractionSettings::precisionOptionName = "precision";
            const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic";
            const std::string AbstractionSettings::invalidBlockStrategyOptionName = "invalid-blocks";
            const std::string AbstractionSettings::reuseQualitativeResultsOptionName = "reuse-qualitative";
            const std::string AbstractionSettings::reuseQuantitativeResultsOptionName = "reuse-quantitative";
            const std::string AbstractionSettings::reuseAllResultsOptionName = "reuse-all";
@ -38,10 +37,6 @@ namespace storm {
                this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.")
                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(pivotHeuristic)).setDefaultValueString("nearest-max-dev").build()).build());
                std::vector<std::string> invalidBlockStrategies = {"none", "local", "global"};
                this->addOption(storm::settings::OptionBuilder(moduleName, invalidBlockStrategyOptionName, true, "Sets the strategy to detect invalid blocks.")
                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("local").build()).build());
                this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build());
                this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build());
                this->addOption(storm::settings::OptionBuilder(moduleName, reuseAllResultsOptionName, true, "Sets whether to reuse all results.").build());
@ -88,18 +83,6 @@ namespace storm {
                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown pivot selection heuristic '" << heuristicName << "'.");
            }
            AbstractionSettings::InvalidBlockDetectionStrategy AbstractionSettings::getInvalidBlockDetectionStrategy() const {
                std::string strategyName = this->getOption(invalidBlockStrategyOptionName).getArgumentByName("name").getValueAsString();
                if (strategyName == "none") {
                    return AbstractionSettings::InvalidBlockDetectionStrategy::None;
                } else if (strategyName == "local") {
                    return AbstractionSettings::InvalidBlockDetectionStrategy::Local;
                } else if (strategyName == "global") {
                    return AbstractionSettings::InvalidBlockDetectionStrategy::Global;
                }
                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown invalid block detection strategy '" << strategyName << "'.");
            }
            bool AbstractionSettings::isReuseQualitativeResultsSet() const {
                return this->getOption(reuseQualitativeResultsOptionName).getHasOptionBeenSet();
            }
--- a/src/storm/settings/modules/AbstractionSettings.h
+++ b/src/storm/settings/modules/AbstractionSettings.h
@ -15,10 +15,6 @@ namespace storm {
                    NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation
                };
                enum class InvalidBlockDetectionStrategy {
                    None, Local, Global
                };
                /*!
                 * Creates a new set of abstraction settings.
                 */
@ -79,14 +75,7 @@ namespace storm {
                 * @return The selected heuristic.
                 */
                PivotSelectionHeuristic getPivotSelectionHeuristic() const;
                /*!
                 * Retrieves the strategy to use for invalid block detection.
                 *
                 * @return The strategy to use
                 */
                InvalidBlockDetectionStrategy getInvalidBlockDetectionStrategy() const;
                /*!
                 * Retrieves whether the option to reuse the qualitative results was set.
                 *
@ -127,7 +116,6 @@ namespace storm {
                const static std::string splitAllOptionName;
                const static std::string precisionOptionName;
                const static std::string pivotHeuristicOptionName;
                const static std::string invalidBlockStrategyOptionName;
                const static std::string reuseQualitativeResultsOptionName;
                const static std::string reuseQuantitativeResultsOptionName;
                const static std::string reuseAllResultsOptionName;