From 16f3b06f53dfc1c2e448ca3db1c518be474539cc Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 15 Dec 2016 14:23:05 +0100 Subject: [PATCH] added decomposition to JANI abstractor, fixed wrong assertion --- .../abstraction/jani/AutomatonAbstractor.cpp | 9 +- .../abstraction/jani/AutomatonAbstractor.h | 3 +- src/storm/abstraction/jani/EdgeAbstractor.cpp | 398 +++++++++++++++--- src/storm/abstraction/jani/EdgeAbstractor.h | 26 +- .../jani/JaniMenuGameAbstractor.cpp | 14 +- .../abstraction/jani/JaniMenuGameAbstractor.h | 3 - .../abstraction/prism/CommandAbstractor.cpp | 142 +++---- .../abstraction/prism/CommandAbstractor.h | 17 +- .../abstraction/prism/ModuleAbstractor.cpp | 9 +- .../abstraction/prism/ModuleAbstractor.h | 3 +- .../prism/PrismMenuGameAbstractor.cpp | 15 +- .../prism/PrismMenuGameAbstractor.h | 3 - .../abstraction/GameBasedMdpModelChecker.cpp | 2 +- .../settings/modules/AbstractionSettings.cpp | 17 - .../settings/modules/AbstractionSettings.h | 14 +- 15 files changed, 437 insertions(+), 238 deletions(-) diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 77684b842..32e53cf7f 100644 --- 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 - AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr 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::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr 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; } } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index bc7cce6e4..b75a61b0d 100644 --- 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& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy); + AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); AutomatonAbstractor(AutomatonAbstractor const&) = default; AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default; diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index ec1eae2ab..6fab837ab 100644 --- 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 - EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr 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::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr 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::vector>> newRelevantPredicates = this->computeRelevantPredicates(); @@ -72,6 +72,303 @@ namespace storm { template void EdgeAbstractor::recomputeCachedBdd() { + if (useDecomposition) { + recomputeCachedBddWithDecomposition(); + } else { + recomputeCachedBddWithoutDecomposition(); + } + } + + template + void EdgeAbstractor::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 allRelevantBlocks; + std::map 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> relevantBlockPartition; + std::map variableToLocalBlockIndex; + uint64_t index = 0; + for (auto const& blockIndex : allRelevantBlocks) { + relevantBlockPartition.emplace_back(std::set({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 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 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> 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 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 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 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))); + } + } + + // 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>> 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 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, 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(); + } + + // multiply the results + storm::dd::Bdd 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 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())); + + 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(resultBdd, usedNondeterminismVariables); + + 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; + } + } + + template + void EdgeAbstractor::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, std::vector>> 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 std::pair, std::vector>> EdgeAbstractor::computeRelevantPredicates() const { std::pair, std::vector>> 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::Bdd EdgeAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd EdgeAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector> const& variablePredicates) const { storm::dd::Bdd 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::Bdd EdgeAbstractor::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd EdgeAbstractor::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector>> const& variablePredicates) const { storm::dd::Bdd 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 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 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::Bdd EdgeAbstractor::computeMissingGlobalIdentities() const { storm::dd::Bdd 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 GameBddResult EdgeAbstractor::abstract() { if (forceRecomputation) { @@ -351,7 +623,7 @@ namespace storm { BottomStateResult EdgeAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard()); BottomStateResult 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; template class EdgeAbstractor; #ifdef STORM_HAVE_CARL - template class EdgeAbstractor; + template class EdgeAbstractor; #endif } } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index 01be8bab7..02240b34c 100644 --- 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& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors); + EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr 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 getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const; + storm::dd::Bdd getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector> 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 getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const; + storm::dd::Bdd getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector>> 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 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; diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 845465a7e..e2bcd456b 100644 --- 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 - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr 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().getInvalidBlockDetectionStrategy()) { + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr 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(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // For each module of the concrete program, we create an abstract counterpart. + bool useDecomposition = storm::settings::getModule().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 game = automata.front().abstract(); - if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { - auto validBlockStart = std::chrono::high_resolution_clock::now(); - storm::dd::Bdd 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(validBlockEnd - validBlockStart).count() << "ms."); - } - // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index d14ad0d06..781579d56 100644 --- 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; }; } } diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index b2a79622e..12e883e9b 100644 --- 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 - CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr 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::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr 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::vector>> newRelevantPredicates = this->computeRelevantPredicates(); @@ -69,12 +69,21 @@ namespace storm { std::map CommandAbstractor::getVariableUpdates(uint64_t auxiliaryChoice) const { return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap(); } - + template - void CommandAbstractor::recomputeCachedBddUsingDecomposition() { + void CommandAbstractor::recomputeCachedBdd() { + if (useDecomposition) { + recomputeCachedBddWithDecomposition(); + } else { + recomputeCachedBddWithoutDecomposition(); + } + } + + template + void CommandAbstractor::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> relevantBlockPartition; std::map variableToLocalBlockIndex; @@ -110,7 +119,7 @@ namespace storm { for (auto const& update : command.get().getUpdates()) { for (auto const& assignment : update.getAssignments()) { std::set 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 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 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 transitionDecisionVariables; std::vector> sourceVariablesAndPredicates; for (auto const& element : relevantPredicatesAndVariables.first) { @@ -269,7 +278,7 @@ namespace storm { } } } - + std::unordered_map, std::vector>> 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(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."); @@ -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 resultBdd = getAbstractionInformation().getDdManager().getBddOne(); @@ -357,7 +368,7 @@ namespace storm { } template - void CommandAbstractor::recomputeCachedBdd() { + void CommandAbstractor::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 std::pair, std::vector>> CommandAbstractor::computeRelevantPredicates() const { std::pair, std::vector>> 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 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 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::Bdd CommandAbstractor::computeMissingGlobalIdentities() const { storm::dd::Bdd 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 GameBddResult CommandAbstractor::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 CommandAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { STORM_LOG_TRACE("Computing bottom state transitions of command " << command.get()); BottomStateResult 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; template class CommandAbstractor; #ifdef STORM_HAVE_CARL - template class CommandAbstractor; + template class CommandAbstractor; #endif } } diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index 21494e2b2..e673de271 100644 --- 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& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors, bool useDecomposition); + CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr 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 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; diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index d9cf92093..27b23c7a1 100644 --- 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 - ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr 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::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr 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); } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 5982ec361..3cfb21ca7 100644 --- 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& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy, bool useDecomposition); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); ModuleAbstractor(ModuleAbstractor const&) = default; ModuleAbstractor& operator=(ModuleAbstractor const&) = default; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index f49c104c0..89e3b6026 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -33,7 +33,7 @@ namespace storm { template PrismMenuGameAbstractor::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr 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().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().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> PrismMenuGameAbstractor::buildGame() { // As long as there is only one module, we only build its game representation. GameBddResult game = modules.front().abstract(); - - if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { - auto validBlockStart = std::chrono::high_resolution_clock::now(); - storm::dd::Bdd 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(validBlockEnd - validBlockStart).count() << "ms."); - } - + // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index f0928a3be..e8f19eccc 100644 --- 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; }; } } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index a707cd972..139438392 100644 --- 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 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); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 473062a16..e26cb3112 100644 --- 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 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(); } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 8d7a35b2c..c6d2effb8 100644 --- 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;