diff --git a/src/storm/abstraction/LocalExpressionInformation.cpp b/src/storm/abstraction/LocalExpressionInformation.cpp index 98acb1558..4b6735407 100644 --- a/src/storm/abstraction/LocalExpressionInformation.cpp +++ b/src/storm/abstraction/LocalExpressionInformation.cpp @@ -23,7 +23,7 @@ namespace storm { } template - bool LocalExpressionInformation::addExpression(uint_fast64_t globalExpressionIndex) { + std::map LocalExpressionInformation::addExpression(uint_fast64_t globalExpressionIndex) { storm::expressions::Expression const& expression = abstractionInformation.get().getPredicateByIndex(globalExpressionIndex); // Register the expression for all variables that appear in it. @@ -47,12 +47,12 @@ namespace storm { } template - bool LocalExpressionInformation::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) { + std::map LocalExpressionInformation::relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable) { return this->relate({firstVariable, secondVariable}); } template - bool LocalExpressionInformation::relate(std::set const& variables) { + std::map LocalExpressionInformation::relate(std::set const& variables) { // Determine all blocks that need to be merged. std::set blocksToMerge; for (auto const& variable : variables) { @@ -63,15 +63,20 @@ namespace storm { // If we found a single block only, there is nothing to do. if (blocksToMerge.size() == 1) { - return false; + std::map identity; + for (uint64_t i = 0; i < getNumberOfBlocks(); ++i) { + identity.emplace_hint(identity.end(), i, i); + } + return identity; } - this->mergeBlocks(blocksToMerge); - return true; + return this->mergeBlocks(blocksToMerge); } template - void LocalExpressionInformation::mergeBlocks(std::set const& blocksToMerge) { + std::map LocalExpressionInformation::mergeBlocks(std::set const& blocksToMerge) { + std::map oldToNewIndices; + // Merge all blocks into the block to keep. std::vector> newVariableBlocks; std::vector> newExpressionBlocks; @@ -90,12 +95,14 @@ namespace storm { for (auto const& variable : variableBlocks[blockIndex]) { variableToBlockMapping[variable] = blockToKeep; } + oldToNewIndices[blockIndex] = blockToKeep; newVariableBlocks[blockToKeep].insert(variableBlocks[blockIndex].begin(), variableBlocks[blockIndex].end()); newExpressionBlocks[blockToKeep].insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end()); ++blocksToMergeIt; } else { // Otherwise just move the current block to the new partition. + oldToNewIndices[blockIndex] = newVariableBlocks.size(); // Adjust the mapping for all variables of the old block. for (auto const& variable : variableBlocks[blockIndex]) { @@ -109,6 +116,8 @@ namespace storm { variableBlocks = std::move(newVariableBlocks); expressionBlocks = std::move(newExpressionBlocks); + + return oldToNewIndices; } template @@ -172,6 +181,11 @@ namespace storm { return result; } + template + std::set const& LocalExpressionInformation::getExpressionBlock(uint64_t index) const { + return expressionBlocks[index]; + } + template std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition) { std::vector blocks; diff --git a/src/storm/abstraction/LocalExpressionInformation.h b/src/storm/abstraction/LocalExpressionInformation.h index 37c0a3b68..cdae4a343 100644 --- a/src/storm/abstraction/LocalExpressionInformation.h +++ b/src/storm/abstraction/LocalExpressionInformation.h @@ -30,9 +30,9 @@ namespace storm { * Adds the expression and therefore indirectly may cause blocks of variables to be merged. * * @param globalExpressionIndex The global index of the expression. - * @return True iff the partition changed. + * @return A mapping from old block indices to the new ones (after possible merges). */ - bool addExpression(uint_fast64_t globalExpressionIndex); + std::map addExpression(uint_fast64_t globalExpressionIndex); /*! * Retrieves whether the two given variables are in the same block of the partition. @@ -48,17 +48,17 @@ namespace storm { * * @param firstVariable The first variable. * @param secondVariable The second variable. - * @return True iff the partition changed. + * @return A mapping from old block indices to the new ones (after possible merges). */ - bool relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable); + std::map relate(storm::expressions::Variable const& firstVariable, storm::expressions::Variable const& secondVariable); /*! * Places the given variables in the same block of the partition and performs the implied merges. * * @param variables The variables to relate. - * @return True iff the partition changed. + * @return A mapping from old block indices to the new ones (after possible merges). */ - bool relate(std::set const& variables); + std::map relate(std::set const& variables); /*! * Retrieves the block of related variables of the given variable. @@ -123,6 +123,13 @@ namespace storm { */ std::set getExpressionsUsingVariables(std::set const& variables) const; + /*! + * Retrieves the expression block with the given index. + * + * @return The requested expression block. + */ + std::set const& getExpressionBlock(uint64_t index) const; + template friend std::ostream& operator<<(std::ostream& out, LocalExpressionInformation const& partition); @@ -131,8 +138,9 @@ namespace storm { * Merges the blocks with the given indices. * * @param blocksToMerge The indices of the blocks to merge. + * @return A mapping from old block indices to the new ones (after possible merges). */ - void mergeBlocks(std::set const& blocksToMerge); + std::map mergeBlocks(std::set const& blocksToMerge); // The set of variables relevant for this partition. std::set relevantVariables; diff --git a/src/storm/abstraction/ValidBlockAbstractor.cpp b/src/storm/abstraction/ValidBlockAbstractor.cpp new file mode 100644 index 000000000..dcfdcf20c --- /dev/null +++ b/src/storm/abstraction/ValidBlockAbstractor.cpp @@ -0,0 +1,136 @@ +#include "storm/abstraction/ValidBlockAbstractor.h" + +#include "storm/abstraction/AbstractionInformation.h" + +#include "storm/storage/dd/DdManager.h" + +#include "storm/utility/solver.h" + +namespace storm { + namespace abstraction { + + template + ValidBlockAbstractor::ValidBlockAbstractor(AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory) : abstractionInformation(abstractionInformation), localExpressionInformation(abstractionInformation), validBlocks(abstractionInformation.getDdManager().getBddOne()), checkForRecomputation(false) { + + uint64_t numberOfBlocks = localExpressionInformation.getNumberOfBlocks(); + validBlocksForPredicateBlocks.resize(numberOfBlocks, abstractionInformation.getDdManager().getBddOne()); + relevantVariablesAndPredicates.resize(numberOfBlocks); + decisionVariables.resize(numberOfBlocks); + + for (uint64_t i = 0; i < numberOfBlocks; ++i) { + smtSolvers.emplace_back(smtSolverFactory->create(abstractionInformation.getExpressionManager())); + for (auto const& constraint : abstractionInformation.getConstraints()) { + smtSolvers.back()->add(constraint); + } + } + } + + template + storm::dd::Bdd const& ValidBlockAbstractor::getValidBlocks() { + if (checkForRecomputation) { + recomputeValidBlocks(); + } + + return validBlocks; + } + + template + void ValidBlockAbstractor::refine(std::vector const& predicates) { + for (auto const& predicate : predicates) { + std::map mergeInformation = localExpressionInformation.addExpression(predicate); + + // Perform the remapping caused by merges. + for (auto const& blockRemapping : mergeInformation) { + if (blockRemapping.first == blockRemapping.second) { + continue; + } + + validBlocksForPredicateBlocks[blockRemapping.second] = validBlocksForPredicateBlocks[blockRemapping.first]; + smtSolvers[blockRemapping.second] = std::move(smtSolvers[blockRemapping.first]); + relevantVariablesAndPredicates[blockRemapping.second] = std::move(relevantVariablesAndPredicates[blockRemapping.first]); + decisionVariables[blockRemapping.second] = std::move(decisionVariables[blockRemapping.first]); + } + validBlocksForPredicateBlocks.resize(localExpressionInformation.getNumberOfBlocks()); + smtSolvers.resize(localExpressionInformation.getNumberOfBlocks()); + relevantVariablesAndPredicates.resize(localExpressionInformation.getNumberOfBlocks()); + decisionVariables.resize(localExpressionInformation.getNumberOfBlocks()); + } + checkForRecomputation = true; + } + + template + void ValidBlockAbstractor::recomputeValidBlocks() { + storm::dd::Bdd newValidBlocks = abstractionInformation.get().getDdManager().getBddOne(); + + for (uint64_t blockIndex = 0; blockIndex < localExpressionInformation.getNumberOfBlocks(); ++blockIndex) { + std::set const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex); + + // If the size of the block changed, we need to add the appropriate variables and recompute the solution. + if (relevantVariablesAndPredicates[blockIndex].size() < predicateBlock.size()) { + recomputeValidBlockForPredicateBlock(blockIndex); + } + + newValidBlocks &= validBlocksForPredicateBlocks[blockIndex]; + } + + validBlocks = newValidBlocks; + } + + template + void ValidBlockAbstractor::recomputeValidBlockForPredicateBlock(uint64_t blockIndex) { + std::set const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex); + + std::vector> newVariables = this->getAbstractionInformation().declareNewVariables(relevantVariablesAndPredicates[blockIndex], predicateBlock); + for (auto const& element : newVariables) { + smtSolvers[blockIndex]->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second))); + decisionVariables[blockIndex].push_back(element.first); + } + + relevantVariablesAndPredicates[blockIndex].insert(relevantVariablesAndPredicates[blockIndex].end(), newVariables.begin(), newVariables.end()); + std::sort(relevantVariablesAndPredicates[blockIndex].begin(), relevantVariablesAndPredicates[blockIndex].end(), + [] (std::pair const& first, std::pair const& second) { + return first.second < second.second; + }); + + // Use all-sat to enumerate all valid blocks for this predicate block. + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + uint64_t numberOfSolutions = 0; + smtSolvers[blockIndex]->allSat(decisionVariables[blockIndex], [&result,this,&numberOfSolutions,blockIndex] (storm::solver::SmtSolver::ModelReference const& model) { + result |= getSourceStateBdd(model, blockIndex); + ++numberOfSolutions; + return true; + }); + + STORM_LOG_TRACE("Computed valid blocks for predicate block " << blockIndex << " (" << numberOfSolutions << " solutions enumerated)."); + + validBlocksForPredicateBlocks[blockIndex] = result; + } + + template + AbstractionInformation const& ValidBlockAbstractor::getAbstractionInformation() const { + return abstractionInformation.get(); + } + + template + storm::dd::Bdd ValidBlockAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); +// std::cout << "new model ----------------" << std::endl; + for (auto const& variableIndexPair : relevantVariablesAndPredicates[blockIndex]) { + if (model.getBooleanValue(variableIndexPair.first)) { +// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is true" << std::endl; + result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); + } else { +// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is false" << std::endl; + result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); + } + } + + STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty."); + return result; + } + + template class ValidBlockAbstractor; + template class ValidBlockAbstractor; + + } +} diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 729704a36..ee537b88e 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace prism { template - CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), 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 allowInvalidSuccessors) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), 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()); @@ -154,9 +154,10 @@ namespace storm { assignedVariables.insert(assignedVariable); } - auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables); - - result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); + if (!allowInvalidSuccessors) { + auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables); + result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); + } return result; } @@ -198,6 +199,7 @@ namespace storm { // Determine and add new relevant source predicates. std::vector> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); for (auto const& element : newSourceVariables) { + allRelevantPredicates.insert(element.second); smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second))); decisionVariables.push_back(element.first); } @@ -210,6 +212,7 @@ namespace storm { for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { std::vector> newSuccessorVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); for (auto const& element : newSuccessorVariables) { + allRelevantPredicates.insert(element.second); smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second).substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); decisionVariables.push_back(element.first); } @@ -271,22 +274,34 @@ namespace storm { template storm::dd::Bdd CommandAbstractor::computeMissingUpdateIdentities() const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { // Compute the identities that are missing for this update. - auto firstIt = relevantPredicatesAndVariables.first.begin(); - auto firstIte = relevantPredicatesAndVariables.first.end(); - auto secondIt = relevantPredicatesAndVariables.second[updateIndex].begin(); - auto secondIte = relevantPredicatesAndVariables.second[updateIndex].end(); + auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin(); + auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end(); - // Go through all relevant source predicates. This is guaranteed to be a superset of the set of - // relevant successor predicates for any update. storm::dd::Bdd updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne(); - for (; firstIt != firstIte; ++firstIt) { - // If the predicates do not match, there is a predicate missing, so we need to add its identity. - if (secondIt == secondIte || firstIt->second != secondIt->second) { - updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(firstIt->second); - } else if (secondIt != secondIte) { - ++secondIt; + 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; + } } } @@ -297,17 +312,32 @@ namespace storm { template storm::dd::Bdd CommandAbstractor::computeMissingGlobalIdentities() const { - auto relevantIt = relevantPredicatesAndVariables.first.begin(); - auto relevantIte = relevantPredicatesAndVariables.first.end(); - storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); - for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) { - if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { - result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex); - } else { - ++relevantIt; + + 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; + } } } + return result; } diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index 0bacfbba8..ecf985bae 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -57,9 +57,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 guardIsPredicate A flag indicating whether the guard of the command was added as a predicate. + * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors. */ - CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate = false); + CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allowInvalidSuccessors); /*! * Refines the abstract command with the given predicates. @@ -220,6 +220,9 @@ namespace storm { // The currently relevant source/successor predicates and the corresponding variables. std::pair>, std::vector>>> relevantPredicatesAndVariables; + // The set of all relevant predicates. + std::set allRelevantPredicates; + // The most recent result of a call to computeDd. If nothing has changed regarding the relevant // predicates, this result may be reused. GameBddResult cachedDd; @@ -227,6 +230,11 @@ 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 the guard of the command was added as a predicate. If this is true, there // is no need to compute bottom states. bool skipBottomStates; diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index ab9b6c592..e825eee48 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -9,6 +9,8 @@ #include "storm/storage/prism/Module.h" +#include "storm/settings/SettingsManager.h" + #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" @@ -18,12 +20,19 @@ namespace storm { namespace abstraction { namespace prism { + using storm::settings::modules::AbstractionSettings; + template - ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allGuardsAdded) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + + bool allowInvalidSuccessorsInCommands = false; + if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { + allowInvalidSuccessorsInCommands = true; + } // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { - commands.emplace_back(command, abstractionInformation, smtSolverFactory, allGuardsAdded); + commands.emplace_back(command, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands); } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 5bb3e0f07..4ba63a56d 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -4,6 +4,8 @@ #include "storm/abstraction/prism/CommandAbstractor.h" +#include "storm/settings/modules/AbstractionSettings.h" + #include "storm/storage/expressions/Expression.h" #include "storm/utility/solver.h" @@ -34,9 +36,8 @@ 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 allGuardsAdded A flag indicating whether all guards of the program were added. */ - ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool allGuardsAdded = false); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory = std::make_shared(), storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy = storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy::Command); 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 ccb8d35fc..0ed031fe3 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -12,6 +12,8 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" + #include "storm/utility/dd.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" @@ -28,10 +30,12 @@ namespace storm { #undef LOCAL_DEBUG + using storm::settings::modules::AbstractionSettings; + 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), currentGame(nullptr), refinementPerformed(false) { + : 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()) { // 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. @@ -62,7 +66,7 @@ namespace storm { // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { - this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory); + this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy); } // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. @@ -85,6 +89,9 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(predicateIndices); + + // Refine the valid blocks. + validBlockAbstractor.refine(predicateIndices); refinementPerformed |= !command.getPredicates().empty(); } @@ -134,6 +141,20 @@ namespace storm { // As long as there is only one module, we only build its game representation. GameBddResult game = modules.front().abstract(); + if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) { + storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); + + // Cut away all invalid blocks for both source and targets. + storm::dd::Bdd newGameBdd = game.bdd; + newGameBdd &= validBlocks; + newGameBdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); + + if (newGameBdd != game.bdd) { + STORM_LOG_TRACE("Global invalid block detection reduced the number of transitions from " << game.bdd.getNonZeroCount() << " to " << newGameBdd.getNonZeroCount() << "."); + game.bdd = newGameBdd; + } + } + // 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 48be5968b..a85c326f6 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -6,12 +6,15 @@ #include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/MenuGame.h" #include "storm/abstraction/RefinementCommand.h" +#include "storm/abstraction/ValidBlockAbstractor.h" #include "storm/abstraction/prism/ModuleAbstractor.h" #include "storm/storage/dd/Add.h" #include "storm/storage/expressions/Expression.h" +#include "storm/settings/modules/AbstractionSettings.h" + namespace storm { namespace utility { namespace solver { @@ -144,6 +147,9 @@ namespace storm { // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; + + // An object that is used to compute the valid blocks. + ValidBlockAbstractor validBlockAbstractor; // An ADD characterizing the probabilities of commands and their updates. storm::dd::Add commandUpdateProbabilitiesAdd; @@ -153,6 +159,9 @@ 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/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 4ac30ff46..431d67d7c 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -19,6 +19,7 @@ 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"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); @@ -31,6 +32,10 @@ namespace storm { std::vector pivotHeuristic = {"nearest-max-dev", "most-prob-path", "max-weighted-dev"}; 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("max-weighted-dev").build()).build()); + + std::vector invalidBlockStrategies = {"none", "command", "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', 'command' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("command").build()).build()); } bool AbstractionSettings::isAddAllGuardsSet() const { @@ -72,6 +77,18 @@ 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 == "command") { + return AbstractionSettings::InvalidBlockDetectionStrategy::Command; + } else if (strategyName == "global") { + return AbstractionSettings::InvalidBlockDetectionStrategy::Global; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown invalid block detection strategy '" << strategyName << "'."); + } } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 16fc2d9be..1fadfe2a0 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -15,6 +15,10 @@ namespace storm { NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation }; + enum class InvalidBlockDetectionStrategy { + None, Command, Global + }; + /*! * Creates a new set of abstraction settings. */ @@ -75,6 +79,13 @@ 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; const static std::string moduleName; @@ -88,6 +99,7 @@ namespace storm { const static std::string splitAllOptionName; const static std::string precisionOptionName; const static std::string pivotHeuristicOptionName; + const static std::string invalidBlockStrategyOptionName; }; }