diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index e9cb479a6..7fd9a9d16 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -510,6 +510,19 @@ namespace storm { return result; } + template + template + std::vector>> AbstractionInformation::decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const { + std::vector> splitChoices = choices.split(player2Variables); + + std::vector>> result; + for (auto const& choice : splitChoices) { + result.emplace_back(this->decodeChoiceToUpdateSuccessorMapping(choice)); + } + + return result; + } + template std::tuple AbstractionInformation::decodeStatePlayer1ChoiceAndUpdate(storm::dd::Bdd const& stateChoiceAndUpdate) const { STORM_LOG_ASSERT(stateChoiceAndUpdate.getNonZeroCount() == 1, "Wrong number of non-zero entries."); @@ -601,5 +614,8 @@ namespace storm { template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + + template std::vector>> AbstractionInformation::decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const; + template std::vector>> AbstractionInformation::decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const; } } diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index 4256f2149..e47e7ab2b 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -456,6 +456,13 @@ namespace storm { template std::map> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + /*! + * Decodes the choices in the form of BDD over the destination variables where the choices are distinguished + * by player 2 variables. + */ + template + std::vector>> decodeChoicesToUpdateSuccessorMapping(std::set const& player2Variables, storm::dd::Bdd const& choices) const; + /*! * Decodes the given BDD (over source, player 1 and aux variables) into a bit vector indicating the truth * values of the predicates in the state and the choice/update indices. diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 888b534b4..84ac8e7af 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -73,6 +73,7 @@ namespace storm { splitAll = splitMode == AbstractionSettings::SplitMode::All; splitPredicates = splitMode == AbstractionSettings::SplitMode::NonGuard; rankPredicates = abstractionSettings.isRankRefinementPredicatesSet(); + addPredicatesEagerly = abstractionSettings.isUseEagerRefinementSet(); equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints()); if (storm::settings::getModule().isAddAllGuardsSet()) { @@ -253,7 +254,7 @@ namespace storm { storm::expressions::Expression newPredicate; bool fromGuard = false; - // Get abstraction informatin for easier access. + // Get abstraction information for easier access. AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); // Decode the index of the command chosen by player 1. @@ -308,13 +309,17 @@ namespace storm { } } } - ++orderedUpdateIndex; break; } } STORM_LOG_ASSERT(!possibleRefinementPredicates.empty(), "Expected refinement predicates."); + STORM_LOG_TRACE("Possible refinement predicates:"); + for (auto const& pred : possibleRefinementPredicates) { + STORM_LOG_TRACE(pred); + } + 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 @@ -368,6 +373,88 @@ namespace storm { return RefinementPredicates(fromGuard ? RefinementPredicates::Source::Guard : RefinementPredicates::Source::WeakestPrecondition, {newPredicate}); } + template + RefinementPredicates MenuGameRefiner::derivePredicatesFromChoice(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& choice, storm::dd::Bdd const& choiceSuccessors) const { + // Prepare result. + storm::expressions::Expression newPredicate; + bool fromGuard = false; + + // Get abstraction information for easier access. + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + + // Decode the index of the command chosen by player 1. + storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); + auto pl1It = player1ChoiceAsAdd.begin(); + uint_fast64_t player1Index = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); + + // Check whether there are bottom states in the game and whether the choice actually picks the bottom state + // as the successor. + bool buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && choiceSuccessors)).isZero(); + + std::vector possibleRefinementPredicates; + + // If the choice picks the bottom state, the new predicate is based on the guard of the appropriate command + // (that is the player 1 choice). + if (buttomStateSuccessor) { + STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); + possibleRefinementPredicates.emplace_back(abstractor.get().getGuard(player1Index)); + fromGuard = true; + STORM_LOG_DEBUG("Derived new predicate (based on guard): " << possibleRefinementPredicates.back()); + } else { + STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); + + // Decode the choice successors. + std::map> choiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(choiceSuccessors); + std::vector> sortedChoiceUpdateIndicesAndMasses; + for (auto const& e : choiceUpdateToSuccessorMapping) { + sortedChoiceUpdateIndicesAndMasses.emplace_back(e.first, e.second.second); + } + std::sort(sortedChoiceUpdateIndicesAndMasses.begin(), sortedChoiceUpdateIndicesAndMasses.end(), [] (std::pair const& a, std::pair const& b) { return a.second > b.second; }); + + // Compute all other (not taken) choices. + std::set variablesToAbstract = game.getRowVariables(); + variablesToAbstract.insert(game.getPlayer1Variables().begin(), game.getPlayer1Variables().end()); + + storm::dd::Bdd otherChoices = (pivotState && !choice && player1Choice && game.getExtendedTransitionMatrix().toBdd()).existsAbstract(variablesToAbstract); + STORM_LOG_ASSERT(!otherChoices.isZero(), "Expected other choices."); + + // Decode the other choices. + std::vector>> otherChoicesUpdateToSuccessorMappings = abstractionInformation.template decodeChoicesToUpdateSuccessorMapping(game.getPlayer2Variables(), otherChoices); + + for (auto const& otherChoice : otherChoicesUpdateToSuccessorMappings) { + for (uint64_t updateIndex = 0; updateIndex < sortedChoiceUpdateIndicesAndMasses.size(); ++updateIndex) { + storm::storage::BitVector const& choiceSuccessor = choiceUpdateToSuccessorMapping.at(sortedChoiceUpdateIndicesAndMasses[updateIndex].first).first; + storm::storage::BitVector const& otherChoiceSuccessor = otherChoice.at(sortedChoiceUpdateIndicesAndMasses[updateIndex].first).first; + + bool deviates = choiceSuccessor != otherChoiceSuccessor; + if (deviates) { + std::map variableUpdates = abstractor.get().getVariableUpdates(player1Index, sortedChoiceUpdateIndicesAndMasses[updateIndex].first); + + for (uint64_t predicateIndex = 0; predicateIndex < choiceSuccessor.size(); ++predicateIndex) { + if (choiceSuccessor[predicateIndex] != otherChoiceSuccessor[predicateIndex]) { + possibleRefinementPredicates.push_back(abstractionInformation.getPredicateByIndex(predicateIndex).substitute(variableUpdates).simplify()); + if (!rankPredicates) { + break; + } + } + } + + break; + } + } + } + + STORM_LOG_ASSERT(!possibleRefinementPredicates.empty(), "Expected refinement predicates."); + + STORM_LOG_TRACE("Possible refinement predicates:"); + for (auto const& pred : possibleRefinementPredicates) { + STORM_LOG_TRACE(pred); + } + } + + return RefinementPredicates(fromGuard ? RefinementPredicates::Source::Guard : RefinementPredicates::Source::WeakestPrecondition, {possibleRefinementPredicates}); + } + template PivotStateCandidatesResult computePivotStates(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) { @@ -413,31 +500,39 @@ namespace storm { bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero() && !lowerChoice1.isZero() && !lowerChoice2.isZero(); if (lowerChoicesDifferent) { - STORM_LOG_TRACE("Deriving predicate based on lower choice."); - predicates = derivePredicatesFromDifferingChoices((pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + STORM_LOG_TRACE("Deriving predicates based on lower choice."); + if (this->addPredicatesEagerly) { + predicates = derivePredicatesFromChoice(game, pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice && minPlayer2Strategy, lowerChoice1); + } else { + predicates = derivePredicatesFromDifferingChoices((pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + } } - if (predicates && (!player1ChoicesDifferent || predicates.get().getSource() == RefinementPredicates::Source::Guard)) { + if (predicates && !player1ChoicesDifferent) { return predicates.get(); - } else { - boost::optional additionalPredicates; - - storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; - storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); - storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero() && !upperChoice1.isZero() && !upperChoice2.isZero(); - if (upperChoicesDifferent) { - STORM_LOG_TRACE("Deriving predicate based on upper choice."); + } + + boost::optional additionalPredicates; + + storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; + storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); + + bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero() && !upperChoice1.isZero() && !upperChoice2.isZero(); + if (upperChoicesDifferent) { + STORM_LOG_TRACE("Deriving predicates based on upper choice."); + if (this->addPredicatesEagerly) { + additionalPredicates = derivePredicatesFromChoice(game, pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice && maxPlayer2Strategy, upperChoice1); + } else { additionalPredicates = derivePredicatesFromDifferingChoices((pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); } - - if (additionalPredicates) { - if (additionalPredicates.get().getSource() == RefinementPredicates::Source::Guard) { - return additionalPredicates.get(); - } else { - predicates.get().addPredicates(additionalPredicates.get().getPredicates()); - } + } + + if (additionalPredicates) { + if (additionalPredicates.get().getSource() == RefinementPredicates::Source::Guard) { + return additionalPredicates.get(); + } else { + predicates.get().addPredicates(additionalPredicates.get().getPredicates()); } } diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index a3269ac91..403cd92c7 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -145,6 +145,7 @@ namespace storm { private: RefinementPredicates derivePredicatesFromDifferingChoices(storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; + RefinementPredicates derivePredicatesFromChoice(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& choice, storm::dd::Bdd const& choiceSuccessors) const; RefinementPredicates derivePredicatesFromPivotState(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; /*! @@ -186,6 +187,9 @@ namespace storm { /// A flag indicating whether predicates are to be ranked. bool rankPredicates; + /// A flag indicating whether predicates are to be generated eagerly. + bool addPredicatesEagerly; + /// A flag indicating whether all guards have been used to refine the abstraction. bool addedAllGuardsFlag; diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index cfd1bed60..d7003a39f 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -179,7 +179,6 @@ namespace storm { } relevantBlockPartition[representativeBlock].insert(relevantBlockPartition[assignmentVariableBlock].begin(), relevantBlockPartition[assignmentVariableBlock].end()); relevantBlockPartition[assignmentVariableBlock].clear(); - } } } @@ -188,200 +187,235 @@ namespace storm { // Now remove all blocks that are empty and obtain the partition. std::vector> cleanedRelevantBlockPartition; - for (auto& element : relevantBlockPartition) { - if (!element.empty()) { - cleanedRelevantBlockPartition.emplace_back(std::move(element)); + for (auto& outerBlock : relevantBlockPartition) { + if (!outerBlock.empty()) { + cleanedRelevantBlockPartition.emplace_back(); + + for (auto const& innerBlock : outerBlock) { + if (!localExpressionInformation.getExpressionBlock(innerBlock).empty()) { + cleanedRelevantBlockPartition.back().insert(innerBlock); + } + } + + if (cleanedRelevantBlockPartition.back().empty()) { + cleanedRelevantBlockPartition.pop_back(); + } } } 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 variablesContainedInGuard = command.get().getGuardExpression().getVariables(); + STORM_LOG_TRACE("Decomposition into " << relevantBlockPartition.size() << " blocks."); + for (auto const& block : relevantBlockPartition) { + STORM_LOG_TRACE("New block of size " << block.size() << ":"); - // 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 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; - } + std::set blockPredicateIndices; + for (auto const& innerBlock : block) { + blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); + } + + for (auto const& predicateIndex : blockPredicateIndices) { + STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex)); + } + } + + std::set variablesContainedInGuard = command.get().getGuardExpression().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 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; + } + if (allContained) { + enumerateAbstractGuard = false; + } + } + + uint64_t numberOfSolutions = 0; + uint64_t numberOfTotalSolutions = 0; + + // If we need to enumerate the guard, do it only once now. + if (enumerateAbstractGuard) { + std::set relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard); + std::vector guardDecisionVariables; + std::vector> 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 << " solutions 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::unordered_map> result = abstractGuard.toExpression(this->getAbstractionInformation().getExpressionManager()); + + // Then add it to the solver. + for (auto const& expression : result.first) { + smtSolver->add(expression); + } - uint64_t numberOfSolutions = 0; + // 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> blockBdds; + for (auto const& block : relevantBlockPartition) { + std::set relevantPredicates; + for (auto const& innerBlock : block) { + relevantPredicates.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); + } - if (enumerateAbstractGuard) { - // otherwise, enumerate the abstract guard so we do this only once - std::set relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard); - std::vector guardDecisionVariables; - std::vector> 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::unordered_map> 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))); - } + if (relevantPredicates.empty()) { + STORM_LOG_TRACE("Block does not contain relevant predicates, skipping it."); + continue; } - // then enumerate the solutions for each of the blocks of the decomposition - uint64_t usedNondeterminismVariables = 0; - uint64_t blockCounter = 0; - std::vector> blockBdds; - for (auto const& block : relevantBlockPartition) { - std::set relevantPredicates; - for (auto const& innerBlock : block) { - relevantPredicates.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); - } - - std::vector transitionDecisionVariables; - std::vector> 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 transitionDecisionVariables; + std::vector> 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>> destinationVariablesAndPredicates; - for (uint64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - destinationVariablesAndPredicates.emplace_back(); - for (auto const& assignment : command.get().getUpdate(updateIndex).getAssignments()) { - uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()); - std::set const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex); - if (block.find(assignmentVariableBlockIndex) != block.end()) { - for (auto const& element : relevantPredicatesAndVariables.second[updateIndex]) { - if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) { - destinationVariablesAndPredicates.back().push_back(element); - transitionDecisionVariables.push_back(element.first); - } + } + + std::vector>> destinationVariablesAndPredicates; + for (uint64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { + destinationVariablesAndPredicates.emplace_back(); + for (auto const& assignment : command.get().getUpdate(updateIndex).getAssignments()) { + uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()); + std::set const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex); + if (block.find(assignmentVariableBlockIndex) != block.end()) { + for (auto const& element : relevantPredicatesAndVariables.second[updateIndex]) { + if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) { + destinationVariablesAndPredicates.back().push_back(element); + transitionDecisionVariables.push_back(element.first); } } } } - - std::unordered_map, std::vector>> 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(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(std::ceil(std::log2(maximalNumberOfChoices + 1))); - - // Finally, build overall result. - storm::dd::Bdd 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 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(); - } + std::unordered_map, std::vector>> 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 << "."); + numberOfTotalSolutions += numberOfSolutions; - // multiply the results - storm::dd::Bdd resultBdd = getAbstractionInformation().getDdManager().getBddOne(); - for (auto const& blockBdd : blockBdds) { - resultBdd &= blockBdd; + // 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(sourceDistributionsPair.second.size())); } - // if we did not explicitly enumerate the guard, we can construct it from the result BDD. - if (!enumerateAbstractGuard) { - std::set 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 variablesToAbstract; - std::set_intersection(allVariables.begin(), allVariables.end(), resultBdd.getContainedMetaVariables().begin(), resultBdd.getContainedMetaVariables().end(), std::inserter(variablesToAbstract, variablesToAbstract.begin())); + // 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(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)))); + std::cout << "need " << numberOfVariablesNeeded << " variables for " << (maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)) << " choices" << std::endl; + + // Finally, build overall result. + storm::dd::Bdd 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."); - abstractGuard = resultBdd.existsAbstract(variablesToAbstract); - } else { - // Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks. - resultBdd &= abstractGuard; + // We start with the distribution index of 1, because 0 is reserved for a potential bottom choice. + uint_fast64_t distributionIndex = blockCounter == 0 ? 1 : 0; + storm::dd::Bdd 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; - // multiply with missing identities - resultBdd &= computeMissingIdentities(); - - // cache and return result - resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); + blockBdds.push_back(resultBdd); + ++blockCounter; + } + + if (enumerateAbstractGuard) { + smtSolver->pop(); + } + + // multiply the results + storm::dd::Bdd resultBdd = getAbstractionInformation().getDdManager().getBddOne(); + uint64_t blockIndex = 0; + for (auto const& blockBdd : blockBdds) { + blockBdd.template toAdd().exportToDot("block" + std::to_string(command.get().getGlobalIndex()) + "_" + std::to_string(blockIndex) + ".dot"); + resultBdd &= blockBdd; + ++blockIndex; + } + + // If we did not explicitly enumerate the guard, we can construct it from the result BDD. + if (!enumerateAbstractGuard) { + std::set 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()); - // Cache the result. - cachedDd = GameBddResult(resultBdd, usedNondeterminismVariables); + std::set variablesToAbstract; + std::set_intersection(allVariables.begin(), allVariables.end(), resultBdd.getContainedMetaVariables().begin(), resultBdd.getContainedMetaVariables().end(), std::inserter(variablesToAbstract, variablesToAbstract.begin())); - auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); - forceRecomputation = false; + abstractGuard = resultBdd.existsAbstract(variablesToAbstract); + } else { + // Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks. + resultBdd &= abstractGuard; } + + resultBdd.template toAdd().exportToDot("decomp" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + + auto identities = computeMissingIdentities(); + identities.template toAdd().exportToDot("idents" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + + // multiply with missing identities + resultBdd &= computeMissingIdentities(); + + // cache and return result + resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); + + // Cache the result. + cachedDd = GameBddResult(resultBdd, usedNondeterminismVariables); + + auto end = std::chrono::high_resolution_clock::now(); + + STORM_LOG_TRACE("Enumerated " << numberOfTotalSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); + forceRecomputation = false; } template @@ -433,6 +467,8 @@ namespace storm { STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty."); } + resultBdd.template toAdd().exportToDot("nodecomp" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + resultBdd &= computeMissingIdentities(); resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); @@ -460,12 +496,12 @@ namespace storm { auto const& leftHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignedVariable); result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); - // Keep track of all assigned variables, so we can find the related predicates later. - assignedVariables.insert(assignedVariable); +// // Keep track of all assigned variables, so we can find the related predicates later. +// assignedVariables.insert(assignedVariable); } - 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; } @@ -594,6 +630,7 @@ namespace storm { 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) { + std::cout << "adding update identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(sourceRelevantIt->second) << " to update " << updateIndex << std::endl; updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second); } else { ++updateRelevantIt; @@ -614,6 +651,7 @@ namespace storm { for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { + std::cout << "adding global identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(predicateIndex) << std::endl; result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); } else { ++relevantIt; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 0ebb77f7d..c79a423d3 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -530,9 +530,8 @@ namespace storm { // Derive the optimization direction for player 1 (assuming menu-game abstraction). storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask); - + // Create the abstractor. - std::shared_ptr> abstractor; if (preprocessedModel.isPrismProgram()) { abstractor = std::make_shared>(preprocessedModel.asPrismProgram(), smtSolverFactory); } else { @@ -543,7 +542,6 @@ namespace storm { } abstractor->addTerminalStates(targetStateExpression); abstractor->setTargetStates(targetStateExpression); - // Create a refiner that can be used to refine the abstraction when needed. storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); @@ -556,15 +554,15 @@ namespace storm { boost::optional> previousSymbolicQualitativeResult = boost::none; boost::optional> previousSymbolicMinQuantitativeResult = boost::none; boost::optional> previousExplicitResult = boost::none; - for (uint_fast64_t iterations = 0; iterations < maximalNumberOfAbstractions; ++iterations) { + for (iteration = 0; iteration < maximalNumberOfAbstractions; ++iteration) { auto iterationStart = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Starting iteration " << iterations << "."); + STORM_LOG_TRACE("Starting iteration " << iteration << "."); // (1) build the abstraction. auto abstractionStart = std::chrono::high_resolution_clock::now(); storm::abstraction::MenuGame game = abstractor->abstract(); auto abstractionEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); + STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); // (2) Prepare initial, constraint and target state BDDs for later use. storm::dd::Bdd initialStates = game.getInitialStates(); @@ -575,11 +573,13 @@ namespace storm { targetStates |= game.getBottomStates(); } + exit(-1); + // #ifdef LOCAL_DEBUG -// initialStates.template toAdd().exportToDot("init" + std::to_string(iterations) + ".dot"); -// targetStates.template toAdd().exportToDot("target" + std::to_string(iterations) + ".dot"); -// abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); -// game.getReachableStates().template toAdd().exportToDot("reach" + std::to_string(iterations) + ".dot"); +// initialStates.template toAdd().exportToDot("init" + std::to_string(iteration) + ".dot"); +// targetStates.template toAdd().exportToDot("target" + std::to_string(iteration) + ".dot"); +// abstractor->exportToDot("game" + std::to_string(iteration) + ".dot", targetStates, game.getManager().getBddOne()); +// game.getReachableStates().template toAdd().exportToDot("reach" + std::to_string(iteration) + ".dot"); // #endif std::unique_ptr result; @@ -595,7 +595,7 @@ namespace storm { } auto iterationEnd = std::chrono::high_resolution_clock::now(); - STORM_LOG_INFO("Iteration " << iterations << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); + STORM_LOG_INFO("Iteration " << iteration << " took " << std::chrono::duration_cast(iterationEnd - iterationStart).count() << "ms."); } // If this point is reached, we have given up on abstraction. @@ -790,10 +790,6 @@ namespace storm { qualitativeRefinement = refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair); auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_INFO("Qualitative refinement completed in " << std::chrono::duration_cast(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms."); - } else if (initialStates.isSubsetOf(initialMaybeStates) && checkTask.isQualitativeSet()) { - // If all initial states are 'maybe' states and the property we needed to check is a qualitative one, - // we can return the result here. - return std::make_unique>(storm::storage::sparse::state_type(0), ValueType(0.5)); } ExplicitQuantitativeResultMinMax quantitativeResult; @@ -1001,6 +997,12 @@ namespace storm { STORM_LOG_INFO("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << result.prob0Min.player1States.getNonZeroCount() << " 'no', " << result.prob1Min.player1States.getNonZeroCount() << " 'yes'."); STORM_LOG_INFO("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << result.prob0Max.player1States.getNonZeroCount() << " 'no', " << result.prob1Max.player1States.getNonZeroCount() << " 'yes'."); +// this->abstractor->exportToDot("lower_game" + std::to_string(iteration) + ".dot", result.prob1Max.getStates(), (result.prob0Min.getPlayer1Strategy() && result.prob0Min.getPlayer2Strategy()) || (result.prob1Min.getPlayer1Strategy() && result.prob1Min.getPlayer2Strategy())); +// this->abstractor->exportToDot("upper_game" + std::to_string(iteration) + ".dot", targetStates, (result.prob0Max.getPlayer1Strategy() && result.prob0Max.getPlayer2Strategy()) || (result.prob1Max.getPlayer1Strategy() && result.prob1Max.getPlayer2Strategy())); +// this->abstractor->exportToDot("lower_game" + std::to_string(iteration) + ".dot", targetStates, game.getManager().getBddOne()); +// this->abstractor->exportToDot("upper_game" + std::to_string(iteration) + ".dot", targetStates, game.getManager().getBddOne()); +// exit(-1); + STORM_LOG_ASSERT(checkQualitativeStrategies(result, targetStates), "Qualitative strategies appear to be broken."); return result; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 0319e48c5..e93e91c69 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -142,6 +142,12 @@ namespace storm { /// The mode selected for solving the abstraction. storm::settings::modules::AbstractionSettings::SolveMode solveMode; + + /// The currently used abstractor. + std::shared_ptr> abstractor; + + /// The performed number of refinement iterations. + uint64_t iteration; }; } } diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 08f947a48..0bee562f4 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -27,6 +27,7 @@ namespace storm { const std::string AbstractionSettings::maximalAbstractionOptionName = "maxabs"; const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred"; const std::string AbstractionSettings::constraintsOptionName = "constraints"; + const std::string AbstractionSettings::useEagerRefinementOptionName = "eagerref"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -94,6 +95,11 @@ namespace storm { .setDefaultValueString("off").build()) .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, useEagerRefinementOptionName, true, "Sets whether to refine eagerly.") + .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, constraintsOptionName, true, "Specifies additional constraints used by the abstraction.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build()) .build()); @@ -111,7 +117,7 @@ namespace storm { } bool AbstractionSettings::isUseDecompositionSet() const { - return this->getOption(useDecompositionOptionName).getHasOptionBeenSet(); + return this->getOption(useDecompositionOptionName).getArgumentByName("value").getValueAsString() == "on"; } AbstractionSettings::SplitMode AbstractionSettings::getSplitMode() const { @@ -200,6 +206,10 @@ namespace storm { return this->getOption(constraintsOptionName).getArgumentByName("constraints").getValueAsString(); } + bool AbstractionSettings::isUseEagerRefinementSet() const { + return this->getOption(useEagerRefinementOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 0959f2772..2ff536be6 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -142,6 +142,11 @@ namespace storm { */ std::string getConstraintString() const; + /*! + * Retrieves whether to refine eagerly. + */ + bool isUseEagerRefinementSet() const; + const static std::string moduleName; private: @@ -159,6 +164,7 @@ namespace storm { const static std::string maximalAbstractionOptionName; const static std::string rankRefinementPredicatesOptionName; const static std::string constraintsOptionName; + const static std::string useEagerRefinementOptionName; }; } diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 5271a628a..62aa7ccb1 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -410,6 +410,29 @@ namespace storm { return Add(this->getDdManager(), internalBdd.template toAdd(), this->getContainedMetaVariables()); } + template + std::vector> Bdd::split(std::set const& variables) const { + std::set remainingMetaVariables; + std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), variables.begin(), variables.end(), std::inserter(remainingMetaVariables, remainingMetaVariables.begin())); + + std::vector ddGroupVariableIndices; + for (auto const& variable : variables) { + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); + + std::vector> internalBddGroups = this->internalBdd.splitIntoGroups(ddGroupVariableIndices); + std::vector> groups; + for (auto const& internalBdd : internalBddGroups) { + groups.emplace_back(Bdd(this->getDdManager(), internalBdd, remainingMetaVariables)); + } + + return groups; + } + template storm::storage::BitVector Bdd::toVector(storm::dd::Odd const& rowOdd) const { return internalBdd.toVector(rowOdd, this->getSortedVariableIndices()); diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index 9e36ba52b..acb7e9122 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -343,6 +343,11 @@ namespace storm { template Add toAdd() const; + /*! + * Splits the BDD along the given variables (must be at the top). + */ + std::vector> split(std::set const& variables) const; + /*! * Converts the BDD to a bit vector. The given offset-labeled DD is used to determine the correct row of * each entry. diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index b69040372..41aee2517 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -412,6 +412,32 @@ namespace storm { } } + std::vector> InternalBdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { + std::vector> result; + splitIntoGroupsRec(Cudd_Regular(this->getCuddDdNode()), Cudd_IsComplement(this->getCuddDdNode()), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + return result; + } + + void InternalBdd::splitIntoGroupsRec(DdNode* dd, bool negated, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { + // For the empty DD, we do not need to create a group. + if (negated && dd == Cudd_ReadOne(ddManager->getCuddManager().getManager())) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(InternalBdd(ddManager, cudd::BDD(ddManager->getCuddManager(), negated ? Cudd_Complement(dd) : dd))); + } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) { + splitIntoGroupsRec(dd, negated, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd, negated, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } else { + DdNode* elseNode = Cudd_E(dd); + DdNode* thenNode = Cudd_T(dd); + + splitIntoGroupsRec(elseNode, negated ^ Cudd_IsComplement(elseNode), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(thenNode, negated ^ Cudd_IsComplement(thenNode), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const { uint_fast64_t currentIndex = 0; filterExplicitVectorRec(Cudd_Regular(this->getCuddDdNode()), ddManager->getCuddManager(), 0, Cudd_IsComplement(this->getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, odd, targetValues, currentIndex, sourceValues); diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.h b/src/storm/storage/dd/cudd/InternalCuddBdd.h index 93c54c0c8..2a8d8dd52 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.h @@ -385,6 +385,14 @@ namespace storm { */ void filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const; + /*! + * Splits the BDD into several BDDs that differ in the encoding of the given group variables (given via indices). + * + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of BDDs that are the separate groups (wrt. to the encoding of the given variables). + */ + std::vector> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; + friend struct std::hash>; /*! @@ -504,6 +512,8 @@ namespace storm { */ static storm::expressions::Variable toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex); + void splitIntoGroupsRec(DdNode* dd, bool negated, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; + InternalDdManager const* ddManager; cudd::BDD cuddBdd; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 97252476a..2ca68d944 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -443,6 +443,33 @@ namespace storm { } } + std::vector> InternalBdd::splitIntoGroups(std::vector const& ddGroupVariableIndices) const { + std::vector> result; + splitIntoGroupsRec(this->getSylvanBdd().GetBDD(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size()); + return result; + } + + void InternalBdd::splitIntoGroupsRec(BDD dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const { + // For the empty DD, we do not need to create a group. + if (dd == sylvan_false) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(InternalBdd(ddManager, sylvan::Bdd(dd))); + } else if (bdd_isterminal(dd) || ddGroupVariableIndices[currentLevel] < sylvan_var(dd)) { + splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } else { + // Otherwise, we compute the ODDs for both the then- and else successors. + BDD thenDdNode = sylvan_high(dd); + BDD elseDdNode = sylvan_low(dd); + + splitIntoGroupsRec(elseDdNode, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + splitIntoGroupsRec(thenDdNode, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); + } + } + std::pair, std::unordered_map> InternalBdd::toExpression(storm::expressions::ExpressionManager& manager) const { std::pair, std::unordered_map> result; diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h index a1160654c..e5c5a3df2 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.h @@ -374,6 +374,14 @@ namespace storm { */ void filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, storm::storage::BitVector const& sourceValues, storm::storage::BitVector& targetValues) const; + /*! + * Splits the BDD into several BDDs that differ in the encoding of the given group variables (given via indices). + * + * @param ddGroupVariableIndices The indices of the variables that are used to distinguish the groups. + * @return A vector of BDDs that are the separate groups (wrt. to the encoding of the given variables). + */ + std::vector> splitIntoGroups(std::vector const& ddGroupVariableIndices) const; + friend struct std::hash>; /*! @@ -488,6 +496,7 @@ namespace storm { */ static storm::expressions::Variable toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex); + void splitIntoGroupsRec(BDD dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const; // The internal manager responsible for this BDD. InternalDdManager const* ddManager;