diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index a9db0f620..e511c3e29 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -14,6 +14,8 @@ #include "storm/utility/solver.h" #include "storm/utility/shortestPaths.h" +#include "storm/parser/ExpressionParser.h" + #include "storm/solver/MathsatSmtSolver.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -76,7 +78,7 @@ namespace storm { addPredicatesEagerly = abstractionSettings.isUseEagerRefinementSet(); equivalenceChecker.addConstraints(abstractor.getAbstractionInformation().getConstraints()); - if (storm::settings::getModule().isAddAllGuardsSet()) { + if (abstractionSettings.isAddAllGuardsSet()) { std::vector guards; std::pair player1Choices = this->abstractor.get().getPlayer1ChoiceRange(); @@ -91,11 +93,34 @@ namespace storm { this->abstractor.get().notifyGuardsArePredicates(); addedAllGuardsFlag = true; } + + if (abstractionSettings.isInjectRefinementPredicatesSet()) { + std::string predicatesString = abstractionSettings.getInjectedRefinementPredicates(); + std::vector predicatesAsStrings; + boost::split(predicatesAsStrings, predicatesString, boost::is_any_of(";")); + + auto const& expressionManager = abstractor.getAbstractionInformation().getExpressionManager(); + storm::parser::ExpressionParser expressionParser(expressionManager); + std::unordered_map variableMapping; + for (auto const& variableTypePair : expressionManager) { + variableMapping[variableTypePair.first.getName()] = variableTypePair.first; + } + expressionParser.setIdentifierMapping(variableMapping); + + for (auto const& predicateString : predicatesAsStrings) { + storm::expressions::Expression predicate = expressionParser.parseFromString(predicateString); + STORM_LOG_TRACE("Adding special (user-provided) refinement predicate " << predicateString << "."); + refinementPredicatesToInject.emplace_back(predicate); + } + + // Finally reverse the list, because we take the predicates from the back. + std::reverse(refinementPredicatesToInject.begin(), refinementPredicatesToInject.end()); + } } template - void MenuGameRefiner::refine(std::vector const& predicates) const { - performRefinement(createGlobalRefinement(preprocessPredicates(predicates, RefinementPredicates::Source::Manual))); + void MenuGameRefiner::refine(std::vector const& predicates, bool allowInjection) const { + performRefinement(createGlobalRefinement(preprocessPredicates(predicates, RefinementPredicates::Source::Manual)), allowInjection); } template @@ -279,10 +304,6 @@ namespace storm { // Decode both choices to explicit mappings. std::map> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(lowerChoice); std::map> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(upperChoice); - - lowerChoice.template toAdd().exportToDot("lower.dot"); - upperChoice.template toAdd().exportToDot("upper.dot"); - STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); // First, sort updates according to probability mass. @@ -536,7 +557,11 @@ namespace storm { if (additionalPredicates.get().getSource() == RefinementPredicates::Source::Guard) { return additionalPredicates.get(); } else { - predicates.get().addPredicates(additionalPredicates.get().getPredicates()); + if (!predicates) { + predicates = additionalPredicates; + } else { + predicates.get().addPredicates(additionalPredicates.get().getPredicates()); + } } } @@ -1569,14 +1594,20 @@ namespace storm { } template - void MenuGameRefiner::performRefinement(std::vector const& refinementCommands) const { - for (auto const& command : refinementCommands) { - STORM_LOG_INFO("Refining with " << command.getPredicates().size() << " predicates."); - for (auto const& predicate : command.getPredicates()) { - STORM_LOG_INFO(predicate); - } - if (!command.getPredicates().empty()) { - abstractor.get().refine(command); + void MenuGameRefiner::performRefinement(std::vector const& refinementCommands, bool allowInjection) const { + if (!refinementPredicatesToInject.empty() && allowInjection) { + STORM_LOG_INFO("Refining with (injected) predicate " << refinementPredicatesToInject.back() << "."); + abstractor.get().refine(RefinementCommand({refinementPredicatesToInject.back()})); + refinementPredicatesToInject.pop_back(); + } else { + for (auto const& command : refinementCommands) { + STORM_LOG_INFO("Refining with " << command.getPredicates().size() << " predicates."); + for (auto const& predicate : command.getPredicates()) { + STORM_LOG_INFO(predicate); + } + if (!command.getPredicates().empty()) { + abstractor.get().refine(command); + } } } diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 403cd92c7..276d178fb 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -107,8 +107,10 @@ namespace storm { * Refines the abstractor with the given predicates. * * @param predicates The predicates to use for refinement. + * @param allowInjection If true, the refiner is free to inject manually-specified refinement predicates + * instead of the provided ones. */ - void refine(std::vector const& predicates) const; + void refine(std::vector const& predicates, bool allowInjection = true) const; /*! * Refines the abstractor based on the qualitative result by trying to derive suitable predicates. @@ -170,7 +172,7 @@ namespace storm { boost::optional derivePredicatesFromInterpolationKShortestPaths(storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ValueType minProbability, ValueType maxProbability, ExplicitGameStrategyPair const& maxStrategyPair) const; boost::optional derivePredicatesFromInterpolationReversedPath(storm::dd::Odd const& odd, storm::expressions::ExpressionManager& interpolationManager, std::vector const& reversedPath, std::vector const& stateToOffset, std::vector const& player1Labels) const; - void performRefinement(std::vector const& refinementCommands) const; + void performRefinement(std::vector const& refinementCommands, bool allowInjection = true) const; /// The underlying abstractor to refine. std::reference_wrapper> abstractor; @@ -193,6 +195,10 @@ namespace storm { /// A flag indicating whether all guards have been used to refine the abstraction. bool addedAllGuardsFlag; + /// A vector of refinement predicates that are injected (starting with the *last* one in this list). If + // empty, the predicates are derived as usual. + mutable std::vector refinementPredicatesToInject; + /// The heuristic to use for pivot block selection. storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic; diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 84fe80137..ff9884720 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 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) { + CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : 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), debug(debug) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -205,16 +205,22 @@ namespace storm { relevantBlockPartition = std::move(cleanedRelevantBlockPartition); STORM_LOG_TRACE("Decomposition into " << relevantBlockPartition.size() << " blocks."); -// for (auto const& block : relevantBlockPartition) { -// std::set blockPredicateIndices; -// for (auto const& innerBlock : block) { -// blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); -// } -// -// for (auto const& predicateIndex : blockPredicateIndices) { -// STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex)); -// } -// } + if (this->debug) { + uint64_t blockIndex = 0; + for (auto const& block : relevantBlockPartition) { + STORM_LOG_TRACE("Predicates of block " << blockIndex << ":"); + std::set blockPredicateIndices; + for (auto const& innerBlock : block) { + blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); + } + + for (auto const& predicateIndex : blockPredicateIndices) { + STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex)); + } + + ++blockIndex; + } + } std::set variablesContainedInGuard = command.get().getGuardExpression().getVariables(); diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index 9b911c8f5..e6d7c7238 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -56,7 +56,7 @@ namespace storm { * @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. */ - CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition); + CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); /*! * Refines the abstract command with the given predicates. @@ -268,6 +268,9 @@ namespace storm { // A state-set abstractor used to determine the bottom states if not all guards were added. StateSetAbstractor bottomStateAbstractor; + + // A flag that indicates whether or not debug mode is enabled. + bool debug; }; } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index 09e1932cb..d1574e23b 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -23,12 +23,12 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. uint64_t counter = 0; for (auto const& command : module.getCommands()) { - commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition); + commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, debug); ++counter; } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index d5d2e9dc7..9771347c6 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -38,7 +38,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @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, bool useDecomposition); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); 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 661aeca57..7370645ac 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -65,9 +65,11 @@ namespace storm { abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 64, 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(); + auto const& settings = storm::settings::getModule(); + bool useDecomposition = settings.isUseDecompositionSet(); + bool debug = settings.isDebugSet(); for (auto const& module : program.getModules()) { - this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition); + this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, debug); } // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. @@ -154,10 +156,12 @@ namespace storm { // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); + std::set successorAndAuxVariables(abstractionInformation.getSuccessorVariables()); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); + successorAndAuxVariables.insert(auxVariables.begin(), auxVariables.end()); storm::utility::Stopwatch relevantStatesWatch(true); storm::dd::Bdd nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne(); @@ -173,16 +177,17 @@ namespace storm { relevantStatesWatch.stop(); storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); + + // Compute the choices with only valid successors so we can restrict the game to these. + + auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables); // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); - storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); - if (program.get().hasInitialConstruct()) { - initialStates &= validBlocks; - } + storm::dd::Bdd extendedTransitionRelation = validBlocks && nonTerminalStates && game.bdd && choicesWithOnlyValidSuccessors; + storm::dd::Bdd transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract); + storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates() && validBlocks; initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); - reachableStates &= validBlocks; relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { @@ -222,7 +227,7 @@ namespace storm { // Construct the transition matrix by cutting away the transitions of unreachable states. // Note that we also restrict the successor states of transitions, because there might be successors // that are not in the relevant we restrict to. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd(); + storm::dd::Add transitionMatrix = (extendedTransitionRelation && reachableStates && reachableStates.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs())).template toAdd(); transitionMatrix *= commandUpdateProbabilitiesAdd; transitionMatrix += deadlockTransitions; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 588040ce9..35613d9fd 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -372,7 +372,7 @@ namespace storm { // Extend the values of the maybe states by the qualitative values. result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd() : qualitativeResult.prob1Max.getPlayer1States().template toAdd(); } else { - STORM_LOG_TRACE("No maybe states."); + STORM_LOG_TRACE("No " << (player2Direction == storm::OptimizationDirection::Minimize ? "min" : "max") << " maybe states."); // Extend the values of the maybe states by the qualitative values. result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd() : qualitativeResult.prob1Max.getPlayer1States().template toAdd(); @@ -545,7 +545,7 @@ namespace storm { // Create a refiner that can be used to refine the abstraction when needed. storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); - refiner.refine(initialPredicates); + refiner.refine(initialPredicates, false); storm::dd::Bdd globalConstraintStates = abstractor->getStates(constraintExpression); storm::dd::Bdd globalTargetStates = abstractor->getStates(targetStateExpression); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 0bee562f4..0f73e2c4f 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -28,6 +28,8 @@ namespace storm { const std::string AbstractionSettings::rankRefinementPredicatesOptionName = "rankpred"; const std::string AbstractionSettings::constraintsOptionName = "constraints"; const std::string AbstractionSettings::useEagerRefinementOptionName = "eagerref"; + const std::string AbstractionSettings::debugOptionName = "debug"; + const std::string AbstractionSettings::injectRefinementPredicatesOption = "injectref"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -104,6 +106,14 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build()) .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOption, true, "Specifies predicates used by the refinement instead of the derived predicates.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").build()) + .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, true, "Sets whether to enable debug mode.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("off").build()) + .build()); } AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const { @@ -210,6 +220,18 @@ namespace storm { return this->getOption(useEagerRefinementOptionName).getArgumentByName("value").getValueAsString() == "on"; } + bool AbstractionSettings::isDebugSet() const { + return this->getOption(debugOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + + bool AbstractionSettings::isInjectRefinementPredicatesSet() const { + return this->getOption(injectRefinementPredicatesOption).getHasOptionBeenSet(); + } + + std::string AbstractionSettings::getInjectedRefinementPredicates() const { + return this->getOption(injectRefinementPredicatesOption).getArgumentByName("predicates").getValueAsString(); + } + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 2ff536be6..f6627129f 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -147,6 +147,21 @@ namespace storm { */ bool isUseEagerRefinementSet() const; + /*! + * Retrieves whether the debug option was set. + */ + bool isDebugSet() const; + + /*! + * Retrieves whether the option to inject the refinement predicates is set. + */ + bool isInjectRefinementPredicatesSet() const; + + /*! + * Retrieves a string containing refinement predicates to inject (if there are any). + */ + std::string getInjectedRefinementPredicates() const; + const static std::string moduleName; private: @@ -165,6 +180,8 @@ namespace storm { const static std::string rankRefinementPredicatesOptionName; const static std::string constraintsOptionName; const static std::string useEagerRefinementOptionName; + const static std::string debugOptionName; + const static std::string injectRefinementPredicatesOption; }; }