diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 0abca47e0..f161812cf 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -54,7 +54,7 @@ namespace storm { } template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(storm::settings::getModule().isSplitAllSet()), splitPredicates(storm::settings::getModule().isSplitPredicatesSet()), splitGuards(storm::settings::getModule().isSplitGuardsSet()), splitInitialGuards(storm::settings::getModule().isSplitInitialGuardsSet()), pivotSelectionHeuristic(storm::settings::getModule().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), useInterpolation(storm::settings::getModule().isUseInterpolationSet()), splitAll(storm::settings::getModule().isSplitAllSet()), splitPredicates(storm::settings::getModule().isSplitPredicatesSet()), splitGuards(storm::settings::getModule().isSplitGuardsSet()), splitInitialGuards(storm::settings::getModule().isSplitInitialGuardsSet()), addedAllGuardsFlag(false), pivotSelectionHeuristic(storm::settings::getModule().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) { if (storm::settings::getModule().isAddAllGuardsSet()) { std::vector guards; @@ -64,6 +64,8 @@ namespace storm { guards.push_back(this->abstractor.get().getGuard(index)); } performRefinement(createGlobalRefinement(preprocessPredicates(guards, RefinementPredicates::Source::InitialGuard))); + + addedAllGuardsFlag = true; } } @@ -72,8 +74,6 @@ namespace storm { performRefinement(createGlobalRefinement(predicates)); } -// static int cnt = 0; - template MostProbablePathsResult getMostProbablePathSpanningTree(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionFilter) { storm::dd::Add maxProbabilities = game.getInitialStates().template toAdd(); @@ -589,15 +589,6 @@ namespace storm { // Now that we have the pivot state candidates, we need to pick one. PivotStateResult pivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none); -// pivotStateResult.pivotState.template toAdd().exportToDot("pivot__" + std::to_string(cnt) + ".dot"); -// (pivotStateResult.pivotState && minPlayer1Strategy).template toAdd().exportToDot("pivotmin_pl1__" + std::to_string(cnt) + ".dot"); -// (pivotStateResult.pivotState && minPlayer1Strategy && minPlayer2Strategy).template toAdd().exportToDot("pivotmin_pl1pl2__" + std::to_string(cnt) + ".dot"); -// ((pivotStateResult.pivotState && minPlayer1Strategy && minPlayer2Strategy).template toAdd() * game.getExtendedTransitionMatrix()).exportToDot("pivotmin_succ__" + std::to_string(cnt) + ".dot"); -// (pivotStateResult.pivotState && maxPlayer1Strategy).template toAdd().exportToDot("pivotmax_pl1__" + std::to_string(cnt) + ".dot"); -// (pivotStateResult.pivotState && maxPlayer1Strategy && maxPlayer2Strategy).template toAdd().exportToDot("pivotmax_pl1pl2__" + std::to_string(cnt) + ".dot"); -// ((pivotStateResult.pivotState && maxPlayer1Strategy && maxPlayer2Strategy).template toAdd() * game.getExtendedTransitionMatrix()).exportToDot("pivotmax_succ__" + std::to_string(cnt) + ".dot"); -// ++cnt; - boost::optional predicates; if (useInterpolation) { predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); @@ -716,6 +707,11 @@ namespace storm { } } + template + bool MenuGameRefiner::addedAllGuards() const { + return addedAllGuardsFlag; + } + template class MenuGameRefiner; template class MenuGameRefiner; diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index e79248509..9334690ec 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -94,6 +94,11 @@ namespace storm { */ bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) const; + /*! + * Retrieves whether all guards were added. + */ + bool addedAllGuards() const; + private: RefinementPredicates derivePredicatesFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; RefinementPredicates derivePredicatesFromPivotState(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& pivotState, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; @@ -130,6 +135,9 @@ namespace storm { /// A flag indicating whether the initially added guards shall be split before using them for refinement. bool splitInitialGuards; + + /// A flag indicating whether all guards have been used to refine the abstraction. + bool addedAllGuardsFlag; /// The heuristic to use for pivot block selection. storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 9d12a0798..d750138ce 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -41,7 +41,7 @@ namespace storm { using storm::abstraction::QuantitativeResultMinMax; template - GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false) { STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Currently only PRISM models are supported by the game-based model checker."); storm::prism::Program const& originalProgram = model.asPrismProgram(); STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker."); @@ -53,6 +53,8 @@ namespace storm { } else { preprocessedModel = originalProgram; } + + reuseQualitativeResults = storm::settings::getModule().isReuseQualitativeResultsSet(); } template @@ -289,6 +291,7 @@ namespace storm { refiner.refine(initialPredicates); // Enter the main-loop of abstraction refinement. + boost::optional> previousQualitativeResult = boost::none; for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { auto iterationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Starting iteration " << iterations << "."); @@ -316,11 +319,12 @@ namespace storm { // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). auto qualitativeStart = std::chrono::high_resolution_clock::now(); QualitativeResultMinMax qualitativeResult; - std::unique_ptr result = computeProb01States(checkTask, qualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates); + std::unique_ptr result = computeProb01States(checkTask, qualitativeResult, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates, refiner.addedAllGuards()); if (result) { printStatistics(abstractor, game); return result; } + previousQualitativeResult = qualitativeResult; auto qualitativeEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast(qualitativeEnd - qualitativeStart).count() << "ms."); @@ -432,44 +436,98 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not derive player 1 optimization direction."); return storm::OptimizationDirection::Maximize; } - - template - std::unique_ptr GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { - // TODO: use MDP functions when the directions of the players agree? - - qualitativeResult.prob0Min = computeProb01States(true, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates); - qualitativeResult.prob1Min = computeProb01States(false, player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, constraintStates, targetStates); - std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); - if (!result) { - qualitativeResult.prob0Max = computeProb01States(true, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, targetStates); - - // As all states that have a probability 1 when player 2 minimizes will also have probability 1 when - // player 2 maximizes, we can take this set as the target states for thiw operation. - qualitativeResult.prob1Max = computeProb01States(false, player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, constraintStates, qualitativeResult.prob1Min.player1States); - result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); + + template + bool checkQualitativeStrategies(bool prob0, QualitativeResult const& result, storm::dd::Bdd const& targetStates) { + if (prob0) { + STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); + } else { + STORM_LOG_ASSERT(result.hasPlayer1Strategy() && ((result.getPlayer1States() && !targetStates).isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); } + STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); + + return true; + } + + template + bool checkQualitativeStrategies(QualitativeResultMinMax const& qualitativeResult, storm::dd::Bdd const& targetStates) { + bool result = true; + result &= checkQualitativeStrategies(true, qualitativeResult.prob0Min, targetStates); + result &= checkQualitativeStrategies(false, qualitativeResult.prob1Min, targetStates); + result &= checkQualitativeStrategies(true, qualitativeResult.prob0Max, targetStates); + result &= checkQualitativeStrategies(false, qualitativeResult.prob1Max, targetStates); return result; } template - storm::utility::graph::GameProb01Result GameBasedMdpModelChecker::computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates) { - auto start = std::chrono::high_resolution_clock::now(); - storm::utility::graph::GameProb01Result result; - if (prob0) { - result = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); + std::unique_ptr GameBasedMdpModelChecker::computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, bool addedAllGuards) { + + if (reuseQualitativeResults) { + // Depending on the player 1 direction, we choose a different order of operations. + if (player1Direction == storm::OptimizationDirection::Minimize) { + // (1) min/min: compute prob0 using the game functions + qualitativeResult.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + + // (2) min/min: compute prob1 using the MDP functions + storm::dd::Bdd candidates = storm::utility::graph::performProbGreater0A(game, transitionMatrixBdd, constraintStates, targetStates); + storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(game, transitionMatrixBdd, constraintStates, previousQualitativeResult ? previousQualitativeResult.get().prob1Min.player1States : targetStates, candidates); + + // (3) min/min: compute prob1 using the game functions + qualitativeResult.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MinMinMdp)); + + // (4) min/max: compute prob 0 using the game functions + qualitativeResult.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + + // (5) min/max: compute prob 1 using the game functions + // If the guards were previously added, we know that only previous prob1 states can now be prob 1 states again. + boost::optional> prob1Candidates; + if (addedAllGuards && previousQualitativeResult) { + prob1Candidates = previousQualitativeResult.get().prob1Max.player1States; + } + qualitativeResult.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, prob1Candidates); + } else { + // (1) max/max: compute prob0 using the game functions + qualitativeResult.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + + // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states. + storm::dd::Bdd candidates = storm::utility::graph::performProbGreater0E(game, transitionMatrixBdd, constraintStates, targetStates); + if (previousQualitativeResult) { + candidates &= previousQualitativeResult.get().prob1Max.player1States; + } + storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(game, transitionMatrixBdd, constraintStates, targetStates, candidates); + + // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation + qualitativeResult.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true, boost::make_optional(prob1MaxMaxMdp)); + + // (4) max/min: compute prob0 using the game functions + qualitativeResult.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + + // (5) max/min: compute prob1 using the game functions, use prob1 from max/max as the candidate set + qualitativeResult.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp)); + } } else { - result = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true); + qualitativeResult.prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + qualitativeResult.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + qualitativeResult.prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + qualitativeResult.prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); } - if (prob0) { - STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); + STORM_LOG_TRACE("Qualitative precomputation completed."); + STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Minimize << "]: " << qualitativeResult.prob0Min.player1States.getNonZeroCount() << " 'no', " << qualitativeResult.prob1Min.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_TRACE("[" << player1Direction << ", " << storm::OptimizationDirection::Maximize << "]: " << qualitativeResult.prob0Max.player1States.getNonZeroCount() << " 'no', " << qualitativeResult.prob1Max.player1States.getNonZeroCount() << " 'yes'."); + + STORM_LOG_ASSERT(checkQualitativeStrategies(qualitativeResult, targetStates), "Qualitative strategies appear to be broken."); + + // Check for result after qualitative computations. + std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States()); + if (result) { + return result; } else { - STORM_LOG_ASSERT(result.hasPlayer1Strategy() && ((result.getPlayer1States() && !targetStates).isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy."); + result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States()); + if (result) { + return result; + } } - STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy."); - - auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Computed states with probability " << (prob0 ? "0" : "1") << " (player 1: " << player1Direction << ", player 2: " << player2Direction << "): " << result.getPlayer1States().getNonZeroCount() << " '" << (prob0 ? "no" : "yes") << "' states (completed in " << std::chrono::duration_cast(end - start).count() << "ms)."); return result; } diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index 07a3dbce8..ef0c3c0e0 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -71,8 +71,7 @@ namespace storm { * Performs a qualitative check on the the given game to compute the (player 1) states that have probability * 0 or 1, respectively, to reach a target state and only visiting constraint states before. */ - std::unique_ptr computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); - QualitativeResult computeProb01States(bool prob0, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); + std::unique_ptr computeProb01States(CheckTask const& checkTask, QualitativeResultMinMax& qualitativeResult, boost::optional> const& previousQualitativeResult, storm::abstraction::MenuGame const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, bool addedAllGuards); void printStatistics(storm::abstraction::MenuGameAbstractor const& abstractor, storm::abstraction::MenuGame const& game) const; @@ -90,6 +89,9 @@ namespace storm { /// A comparator that can be used for detecting convergence. storm::utility::ConstantsComparator comparator; + + /// A flag indicating whether to reuse the qualitative results. + bool reuseQualitativeResults; }; } } diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp index b48a263ca..fdff99c36 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp @@ -35,7 +35,7 @@ namespace storm { illegalPlayer1Mask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables()); // Correct the mask for player 2. This is necessary, because it is not yet restricted to the legal choices of player 1. - this->illegalMask &= illegalPlayer1Mask; + illegalPlayer2Mask = this->getIllegalMask() && illegalPlayer1Mask; // Then set the illegal mask for player 1 correctly. illegalPlayer1Mask = !illegalPlayer1Mask && reachableStates; @@ -48,8 +48,7 @@ namespace storm { template storm::dd::Bdd StochasticTwoPlayerGame::getIllegalPlayer2Mask() const { - // For player 2, we can simply return the mask of the superclass. - return this->getIllegalMask(); + return illegalPlayer2Mask; } template diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.h b/src/storm/models/symbolic/StochasticTwoPlayerGame.h index 37db5e358..15383b056 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.h +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.h @@ -90,10 +90,12 @@ namespace storm { storm::dd::Bdd getIllegalPlayer2Mask() const; private: - // A mask that characterizes all illegal player 1 choices. The mask for player 2 is given by the mask - // of the superclass (nondeterminstic model). + // A mask that characterizes all illegal player 1 choices. storm::dd::Bdd illegalPlayer1Mask; + // A mask that characterizes all illegal player 2 choices. + storm::dd::Bdd illegalPlayer2Mask; + // The meta variables used to encode the nondeterministic choices of player 1. std::set player1Variables; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 1132a17b0..2c24d2af7 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -20,6 +20,7 @@ namespace storm { 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"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); @@ -29,6 +30,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, splitAllOptionName, true, "Sets whether all predicates are split into atoms before they are added.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-03).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + 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("nearest-max-dev").build()).build()); @@ -36,6 +38,8 @@ namespace storm { 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("global").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build()); } bool AbstractionSettings::isAddAllGuardsSet() const { @@ -89,6 +93,10 @@ namespace storm { } 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 1fadfe2a0..ea9e90ada 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -86,6 +86,13 @@ namespace storm { * @return The strategy to use */ InvalidBlockDetectionStrategy getInvalidBlockDetectionStrategy() const; + + /*! + * Retrieves whether the option to reuse the qualitative results. + * + * @param True iff the option was set. + */ + bool isReuseQualitativeResultsSet() const; const static std::string moduleName; @@ -100,6 +107,7 @@ namespace storm { const static std::string precisionOptionName; const static std::string pivotHeuristicOptionName; const static std::string invalidBlockStrategyOptionName; + const static std::string reuseQualitativeResultsOptionName; }; } diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index db490b8c5..362c731f3 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -33,7 +33,7 @@ namespace storm { } while (changed); auto end = std::chrono::high_resolution_clock::now(); - STORM_LOG_TRACE("Reachability computation completed in " << iteration << " iterations (" << std::chrono::duration_cast(end - start).count() << "ms."); + STORM_LOG_TRACE("Reachability computation completed in " << iteration << " iterations (" << std::chrono::duration_cast(end - start).count() << "ms)."); return reachableStates; } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index ceecdfb18..e2354da57 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -991,12 +991,16 @@ namespace storm { } template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { + GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates) { - // Create two sets of states. Those states for which we definitely know that their probability is 1 and - // those states that potentially have a probability of 1. + // Create the potential prob1 states of player 1. storm::dd::Bdd maybePlayer1States = model.getReachableStates(); - storm::dd::Bdd maybePlayer2States = model.getReachableStates(); + if (player1Candidates) { + maybePlayer1States &= player1Candidates.get(); + } + + // Initialize potential prob1 states of player 2. + storm::dd::Bdd maybePlayer2States = model.getManager().getBddZero(); // A flag that governs whether strategies are produced in the current iteration. bool produceStrategiesInIteration = false; @@ -1523,7 +1527,7 @@ namespace storm { template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); // Instantiations for Sylvan. @@ -1555,7 +1559,7 @@ namespace storm { template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); + template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); } // namespace graph } // namespace utility diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index a10fe8269..1b3b02cbf 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -589,9 +589,10 @@ namespace storm { * @param psiStates The BDD containing all psi states of the model. * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. + * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered. */ template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); + GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional> const& player1Candidates = boost::none); /*! * Performs a topological sort of the states of the system according to the given transitions.