From f4146c821aecfc6bfcd86a9d6de52ab58eab41aa Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 8 Dec 2016 16:20:19 +0100 Subject: [PATCH] more value-reuse --- .../abstraction/prism/CommandAbstractor.cpp | 4 +--- .../abstraction/GameBasedMdpModelChecker.cpp | 10 +++++++--- .../abstraction/GameBasedMdpModelChecker.h | 3 +++ .../settings/modules/AbstractionSettings.cpp | 13 +++++++++++++ .../settings/modules/AbstractionSettings.h | 18 +++++++++++++++++- src/storm/solver/SymbolicGameSolver.cpp | 2 +- 6 files changed, 42 insertions(+), 8 deletions(-) diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index ee537b88e..bbfe1baf9 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -44,9 +44,7 @@ namespace storm { for (auto predicateIndex : predicates) { localExpressionInformation.addExpression(predicateIndex); } - - STORM_LOG_TRACE("Current variable partition is: " << localExpressionInformation); - + // Next, we check whether there is work to be done by recomputing the relevant predicates and checking // whether they changed. std::pair, std::vector>> newRelevantPredicates = this->computeRelevantPredicates(); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index c32bd0f18..ef3767c89 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()), reuseQualitativeResults(false) { + GameBasedMdpModelChecker::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(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."); @@ -54,7 +54,9 @@ namespace storm { preprocessedModel = originalProgram; } - reuseQualitativeResults = storm::settings::getModule().isReuseQualitativeResultsSet(); + bool reuseAll = storm::settings::getModule().isReuseAllResultsSet(); + reuseQualitativeResults = reuseAll || storm::settings::getModule().isReuseQualitativeResultsSet(); + reuseQuantitativeResults = reuseAll || storm::settings::getModule().isReuseQuantitativeResultsSet(); } template @@ -292,6 +294,7 @@ namespace storm { // Enter the main-loop of abstraction refinement. boost::optional> previousQualitativeResult = boost::none; + boost::optional> previousMinQuantitativeResult = 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 << "."); @@ -367,7 +370,8 @@ namespace storm { QuantitativeResultMinMax quantitativeResult; // (7) Solve the min values and check whether we can give the answer already. - quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin); + quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none); + previousMinQuantitativeResult = quantitativeResult.min; result = checkForResultAfterQuantitativeCheck(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue); if (result) { printStatistics(abstractor, game); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h index ef0c3c0e0..1329ef399 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -92,6 +92,9 @@ namespace storm { /// A flag indicating whether to reuse the qualitative results. bool reuseQualitativeResults; + + /// A flag indicating whether to reuse the quantitative results. + bool reuseQuantitativeResults; }; } } diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 2c24d2af7..6cac964a2 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -21,6 +21,8 @@ namespace storm { const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic"; const std::string AbstractionSettings::invalidBlockStrategyOptionName = "invalid-blocks"; const std::string AbstractionSettings::reuseQualitativeResultsOptionName = "reuse-qualitative"; + const std::string AbstractionSettings::reuseQuantitativeResultsOptionName = "reuse-quantitative"; + const std::string AbstractionSettings::reuseAllResultsOptionName = "reuse-all"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); @@ -40,6 +42,8 @@ namespace storm { .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()); + this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, reuseAllResultsOptionName, true, "Sets whether to reuse all results.").build()); } bool AbstractionSettings::isAddAllGuardsSet() const { @@ -97,6 +101,15 @@ namespace storm { bool AbstractionSettings::isReuseQualitativeResultsSet() const { return this->getOption(reuseQualitativeResultsOptionName).getHasOptionBeenSet(); } + + bool AbstractionSettings::isReuseQuantitativeResultsSet() const { + return this->getOption(reuseQuantitativeResultsOptionName).getHasOptionBeenSet(); + } + + bool AbstractionSettings::isReuseAllResultsSet() const { + return this->getOption(reuseAllResultsOptionName).getHasOptionBeenSet(); + } + } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index ea9e90ada..3852e744c 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -88,12 +88,26 @@ namespace storm { InvalidBlockDetectionStrategy getInvalidBlockDetectionStrategy() const; /*! - * Retrieves whether the option to reuse the qualitative results. + * Retrieves whether the option to reuse the qualitative results was set. * * @param True iff the option was set. */ bool isReuseQualitativeResultsSet() const; + + /*! + * Retrieves whether the option to reuse the quantitative results was set. + * + * @param True iff the option was set. + */ + bool isReuseQuantitativeResultsSet() const; + /*! + * Retrieves whether the option to reuse all results was set. + * + * @param True iff the option was set. + */ + bool isReuseAllResultsSet() const; + const static std::string moduleName; private: @@ -108,6 +122,8 @@ namespace storm { const static std::string pivotHeuristicOptionName; const static std::string invalidBlockStrategyOptionName; const static std::string reuseQualitativeResultsOptionName; + const static std::string reuseQuantitativeResultsOptionName; + const static std::string reuseAllResultsOptionName; }; } diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp index 8924f1415..996c7fc72 100644 --- a/src/storm/solver/SymbolicGameSolver.cpp +++ b/src/storm/solver/SymbolicGameSolver.cpp @@ -41,7 +41,7 @@ namespace storm { } boost::optional> previousPlayer2Values; if (generatePlayer2Strategy) { - if (basePlayer2Strategy) { + if (basePlayer2Strategy && player2Goal == storm::OptimizationDirection::Maximize) { player2Strategy = basePlayer2Strategy.get(); // If we are required to generate a player 2 strategy based on another one that is not the zero strategy,