From 9f71721c218b5dbf7dcec48b7427b28c3027a102 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 4 Dec 2016 13:29:03 +0100 Subject: [PATCH] added option to choose pivot based on most probable path and weighted deviation --- src/storm/abstraction/GameBddResult.cpp | 2 +- src/storm/abstraction/MenuGameRefiner.cpp | 186 +++++++++++------- src/storm/abstraction/MenuGameRefiner.h | 20 +- .../settings/modules/AbstractionSettings.cpp | 16 ++ .../settings/modules/AbstractionSettings.h | 12 ++ 5 files changed, 166 insertions(+), 70 deletions(-) diff --git a/src/storm/abstraction/GameBddResult.cpp b/src/storm/abstraction/GameBddResult.cpp index d2dd31a57..9c6111acc 100644 --- a/src/storm/abstraction/GameBddResult.cpp +++ b/src/storm/abstraction/GameBddResult.cpp @@ -1,4 +1,4 @@ -#include "storm/abstraction/prism/GameBddResult.h" +#include "storm/abstraction/GameBddResult.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 178558087..102bb56fa 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -12,11 +12,12 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/AbstractionSettings.h" namespace storm { namespace abstraction { + using storm::settings::modules::AbstractionSettings; + RefinementPredicates::RefinementPredicates(Source const& source, std::vector const& predicates) : source(source), predicates(predicates) { // Intentionally left empty. } @@ -33,6 +34,11 @@ namespace storm { this->predicates.insert(this->predicates.end(), newPredicates.begin(), newPredicates.end()); } + template + MostProbablePathsResult::MostProbablePathsResult(storm::dd::Add const& maxProbabilities, storm::dd::Bdd const& spanningTree) : maxProbabilities(maxProbabilities), spanningTree(spanningTree) { + // Intentionally left empty. + } + template struct PivotStateCandidatesResult { storm::dd::Bdd reachableTransitionsMin; @@ -40,13 +46,13 @@ namespace storm { storm::dd::Bdd pivotStates; }; - template - PivotStateResult::PivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection) : pivotState(pivotState), fromDirection(fromDirection) { + template + PivotStateResult::PivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection, boost::optional> const& mostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), mostProbablePathsResult(mostProbablePathsResult) { // Intentionally left empty. } 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()), 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()), pivotSelectionHeuristic(storm::settings::getModule().getPivotSelectionHeuristic()), splitter(), equivalenceChecker(std::move(smtSolver)) { if (storm::settings::getModule().isAddAllGuardsSet()) { std::vector guards; @@ -67,7 +73,7 @@ namespace storm { // static int cnt = 0; template - storm::dd::Bdd getMostProbablePathSpanningTree(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& targetState, storm::dd::Bdd const& transitionFilter) { + MostProbablePathsResult getMostProbablePathSpanningTree(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionFilter) { storm::dd::Add maxProbabilities = game.getInitialStates().template toAdd(); storm::dd::Bdd border = game.getInitialStates(); @@ -98,72 +104,121 @@ namespace storm { border = updateStates; } - return spanningTree; + return MostProbablePathsResult(maxProbabilities, spanningTree); } - + template - PivotStateResult pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionsMin, storm::dd::Bdd const& transitionsMax, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { - - // Set up used variables. - storm::dd::Bdd frontierMin = initialStates; - storm::dd::Bdd frontierMax = initialStates; - storm::dd::Bdd frontierPivotStates = frontierMin && pivotStates; - - // Check whether we have pivot states on the very first level. - uint64_t level = 0; - bool foundPivotState = !frontierPivotStates.isZero(); - if (foundPivotState) { - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - return PivotStateResult(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize); + PivotStateResult pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame const& game, PivotStateCandidatesResult const& pivotStateCandidateResult, boost::optional> const& qualitativeResult, boost::optional> const& quantitativeResult) { + + // Get easy access to strategies. + storm::dd::Bdd minPlayer1Strategy; + storm::dd::Bdd minPlayer2Strategy; + storm::dd::Bdd maxPlayer1Strategy; + storm::dd::Bdd maxPlayer2Strategy; + if (qualitativeResult) { + minPlayer1Strategy = qualitativeResult.get().prob0Min.getPlayer1Strategy(); + minPlayer2Strategy = qualitativeResult.get().prob0Min.getPlayer2Strategy(); + maxPlayer1Strategy = qualitativeResult.get().prob1Max.getPlayer1Strategy(); + maxPlayer2Strategy = qualitativeResult.get().prob1Max.getPlayer2Strategy(); + } else if (quantitativeResult) { + minPlayer1Strategy = quantitativeResult.get().min.player1Strategy; + minPlayer2Strategy = quantitativeResult.get().min.player2Strategy; + maxPlayer1Strategy = quantitativeResult.get().max.player1Strategy; + maxPlayer2Strategy = quantitativeResult.get().max.player2Strategy; } else { - // Otherwise, we perform a simulatenous BFS in the sense that we make one step in both the min and max - // transitions and check for pivot states we encounter. - while (!foundPivotState) { - frontierMin = frontierMin.relationalProduct(transitionsMin, rowVariables, columnVariables); - frontierMax = frontierMax.relationalProduct(transitionsMax, rowVariables, columnVariables); - ++level; - - storm::dd::Bdd frontierMinPivotStates = frontierMin && pivotStates; - storm::dd::Bdd frontierMaxPivotStates = frontierMax && pivotStates; - uint64_t numberOfPivotStateCandidatesOnLevel = frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount(); - - if (!frontierMinPivotStates.isZero() || !frontierMaxPivotStates.isZero()) { - if (quantitativeResult) { - storm::dd::Add frontierMinPivotStatesAdd = frontierMinPivotStates.template toAdd(); - storm::dd::Add frontierMaxPivotStatesAdd = frontierMaxPivotStates.template toAdd(); - storm::dd::Add diffMin = frontierMinPivotStatesAdd * quantitativeResult.get().max.values - frontierMinPivotStatesAdd * quantitativeResult.get().min.values; - storm::dd::Add diffMax = frontierMaxPivotStatesAdd * quantitativeResult.get().max.values - frontierMaxPivotStatesAdd * quantitativeResult.get().min.values; - - ValueType diffValue; - storm::OptimizationDirection direction; - if (diffMin.getMax() >= diffMax.getMax()) { - direction = storm::OptimizationDirection::Minimize; - diffValue = diffMin.getMax(); - } else { - direction = storm::OptimizationDirection::Maximize; - diffValue = diffMax.getMax(); - } - - STORM_LOG_TRACE("Picked pivot state with difference " << diffValue << " from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - return PivotStateResult(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction); - } else { - STORM_LOG_TRACE("Picked pivot state from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - - storm::OptimizationDirection direction; - if (!frontierMinPivotStates.isZero()) { - direction = storm::OptimizationDirection::Minimize; + STORM_LOG_ASSERT(false, "Either qualitative or quantitative result is required."); + } + + storm::dd::Bdd pivotStates = pivotStateCandidateResult.pivotStates; + + if (heuristic == AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation) { + // Set up used variables. + storm::dd::Bdd initialStates = game.getInitialStates(); + std::set const& rowVariables = game.getRowVariables(); + std::set const& columnVariables = game.getColumnVariables(); + storm::dd::Bdd transitionsMin = pivotStateCandidateResult.reachableTransitionsMin; + storm::dd::Bdd transitionsMax = pivotStateCandidateResult.reachableTransitionsMax; + storm::dd::Bdd frontierMin = initialStates; + storm::dd::Bdd frontierMax = initialStates; + storm::dd::Bdd frontierPivotStates = frontierMin && pivotStates; + + // Check whether we have pivot states on the very first level. + uint64_t level = 0; + bool foundPivotState = !frontierPivotStates.isZero(); + if (foundPivotState) { + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + return PivotStateResult(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize); + } else { + // Otherwise, we perform a simulatenous BFS in the sense that we make one step in both the min and max + // transitions and check for pivot states we encounter. + while (!foundPivotState) { + frontierMin = frontierMin.relationalProduct(transitionsMin, rowVariables, columnVariables); + frontierMax = frontierMax.relationalProduct(transitionsMax, rowVariables, columnVariables); + ++level; + + storm::dd::Bdd frontierMinPivotStates = frontierMin && pivotStates; + storm::dd::Bdd frontierMaxPivotStates = frontierMax && pivotStates; + uint64_t numberOfPivotStateCandidatesOnLevel = frontierMinPivotStates.getNonZeroCount() + frontierMaxPivotStates.getNonZeroCount(); + + if (!frontierMinPivotStates.isZero() || !frontierMaxPivotStates.isZero()) { + if (quantitativeResult) { + storm::dd::Add frontierMinPivotStatesAdd = frontierMinPivotStates.template toAdd(); + storm::dd::Add frontierMaxPivotStatesAdd = frontierMaxPivotStates.template toAdd(); + storm::dd::Add diffMin = frontierMinPivotStatesAdd * quantitativeResult.get().max.values - frontierMinPivotStatesAdd * quantitativeResult.get().min.values; + storm::dd::Add diffMax = frontierMaxPivotStatesAdd * quantitativeResult.get().max.values - frontierMaxPivotStatesAdd * quantitativeResult.get().min.values; + + ValueType diffValue; + storm::OptimizationDirection direction; + if (diffMin.getMax() >= diffMax.getMax()) { + direction = storm::OptimizationDirection::Minimize; + diffValue = diffMin.getMax(); + } else { + direction = storm::OptimizationDirection::Maximize; + diffValue = diffMax.getMax(); + } + + STORM_LOG_TRACE("Picked pivot state with difference " << diffValue << " from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + return PivotStateResult(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction); } else { - direction = storm::OptimizationDirection::Maximize; + STORM_LOG_TRACE("Picked pivot state from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + + storm::OptimizationDirection direction; + if (!frontierMinPivotStates.isZero()) { + direction = storm::OptimizationDirection::Minimize; + } else { + direction = storm::OptimizationDirection::Maximize; + } + + return PivotStateResult(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction); } - - return PivotStateResult(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction); } } } + } else { + // Compute the most probable paths to the reachable states and the corresponding spanning trees. + MostProbablePathsResult minMostProbablePathsResult = getMostProbablePathSpanningTree(game, minPlayer1Strategy && minPlayer2Strategy); + MostProbablePathsResult maxMostProbablePathsResult = getMostProbablePathSpanningTree(game, maxPlayer1Strategy && maxPlayer2Strategy); + storm::dd::Bdd selectedPivotState; + + storm::dd::Add score = pivotStates.template toAdd() * minMostProbablePathsResult.maxProbabilities.maximum(maxMostProbablePathsResult.maxProbabilities); + + if (heuristic == AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation && quantitativeResult) { + score = score * (quantitativeResult.get().max.values - quantitativeResult.get().min.values); + } + selectedPivotState = score.maxAbstractRepresentative(game.getRowVariables()); + STORM_LOG_TRACE("Selected pivot state with score " << score.getMax() << "."); + + storm::OptimizationDirection fromDirection = storm::OptimizationDirection::Minimize; + storm::dd::Add selectedPivotStateAsAdd = selectedPivotState.template toAdd(); + if ((selectedPivotStateAsAdd * maxMostProbablePathsResult.maxProbabilities).getMax() > (selectedPivotStateAsAdd * minMostProbablePathsResult.maxProbabilities).getMax()) { + fromDirection = storm::OptimizationDirection::Maximize; + } + + return PivotStateResult(selectedPivotState, fromDirection, fromDirection == storm::OptimizationDirection::Minimize ? minMostProbablePathsResult : maxMostProbablePathsResult); } STORM_LOG_ASSERT(false, "This point must not be reached, because then no pivot state could be found."); - return PivotStateResult(storm::dd::Bdd(), storm::OptimizationDirection::Minimize); + return PivotStateResult(storm::dd::Bdd(), storm::OptimizationDirection::Minimize); } template @@ -398,7 +453,6 @@ namespace storm { // Perform a backward search for an initial state. storm::dd::Bdd currentState = pivotState; - uint64_t cnt = 0; while ((currentState && game.getInitialStates()).isZero()) { storm::dd::Bdd predecessorTransition = currentState.swapVariables(game.getRowColumnMetaVariablePairs()) && spanningTree; std::tuple decodedPredecessor = abstractionInformation.decodeStatePlayer1ChoiceAndUpdate(predecessorTransition); @@ -441,18 +495,18 @@ namespace storm { } template - boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, PivotStateResult const& pivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const { + boost::optional MenuGameRefiner::derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, PivotStateResult const& pivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const { AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); // Compute the most probable path from any initial state to the pivot state. - storm::dd::Bdd spanningTree = getMostProbablePathSpanningTree(game, pivotStateResult.pivotState, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); + MostProbablePathsResult mostProbablePathsResult = getMostProbablePathSpanningTree(game, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); // Create a new expression manager that we can use for the interpolation. std::shared_ptr interpolationManager = abstractionInformation.getExpressionManager().clone(); // Build the trace of the most probable path in terms of which predicates hold in each step. - std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, spanningTree, pivotStateResult.pivotState); + std::pair>, std::map> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, mostProbablePathsResult.spanningTree, pivotStateResult.pivotState); auto const& trace = traceAndVariableSubstitution.first; auto const& variableSubstitution = traceAndVariableSubstitution.second; @@ -528,7 +582,7 @@ namespace storm { STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - PivotStateResult pivotStateResult = pickPivotState(game.getInitialStates(), pivotStateCandidatesResult.reachableTransitionsMin, pivotStateCandidatesResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateCandidatesResult.pivotStates); + 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"); @@ -571,7 +625,7 @@ namespace storm { STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to refine without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - PivotStateResult pivotStateResult = pickPivotState(game.getInitialStates(), pivotStateCandidatesResult.reachableTransitionsMin, pivotStateCandidatesResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateCandidatesResult.pivotStates); + PivotStateResult pivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult); boost::optional predicates; if (useInterpolation) { diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index bebb6bba2..e23b03303 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -16,6 +16,8 @@ #include "storm/storage/dd/DdType.h" +#include "storm/settings/modules/AbstractionSettings.h" + #include "storm/utility/solver.h" namespace storm { @@ -44,13 +46,22 @@ namespace storm { Source source; std::vector predicates; }; + + template + struct MostProbablePathsResult { + MostProbablePathsResult(storm::dd::Add const& maxProbabilities, storm::dd::Bdd const& spanningTree); + + storm::dd::Add maxProbabilities; + storm::dd::Bdd spanningTree; + }; - template + template struct PivotStateResult { - PivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection); + PivotStateResult(storm::dd::Bdd const& pivotState, storm::OptimizationDirection fromDirection, boost::optional> const& mostProbablePathsResult = boost::none); storm::dd::Bdd pivotState; storm::OptimizationDirection fromDirection; + boost::optional> mostProbablePathsResult; }; template @@ -96,7 +107,7 @@ namespace storm { */ std::vector createGlobalRefinement(std::vector const& predicates) const; - boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, PivotStateResult const& pivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; + boost::optional derivePredicatesFromInterpolation(storm::abstraction::MenuGame const& game, PivotStateResult const& pivotStateResult, storm::dd::Bdd const& minPlayer1Strategy, storm::dd::Bdd const& minPlayer2Strategy, storm::dd::Bdd const& maxPlayer1Strategy, storm::dd::Bdd const& maxPlayer2Strategy) const; std::pair>, std::map> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& spanningTree, storm::dd::Bdd const& pivotState) const; void performRefinement(std::vector const& refinementCommands) const; @@ -119,6 +130,9 @@ namespace storm { /// A flag indicating whether the initially added guards shall be split before using them for refinement. bool splitInitialGuards; + /// The heuristic to use for pivot block selection. + storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic; + /// An object that can be used for splitting predicates. mutable storm::expressions::PredicateSplitter splitter; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 9b58fb49c..4ac30ff46 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string AbstractionSettings::splitInterpolantsOptionName = "split-interpolants"; const std::string AbstractionSettings::splitAllOptionName = "split-all"; const std::string AbstractionSettings::precisionOptionName = "precision"; + const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); @@ -27,6 +28,9 @@ 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("max-weighted-dev").build()).build()); } bool AbstractionSettings::isAddAllGuardsSet() const { @@ -56,6 +60,18 @@ namespace storm { double AbstractionSettings::getPrecision() const { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } + + AbstractionSettings::PivotSelectionHeuristic AbstractionSettings::getPivotSelectionHeuristic() const { + std::string heuristicName = this->getOption(pivotHeuristicOptionName).getArgumentByName("name").getValueAsString(); + if (heuristicName == "nearest-max-dev") { + return AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation; + } else if (heuristicName == "most-prob-path") { + return AbstractionSettings::PivotSelectionHeuristic::MostProbablePath; + } else if (heuristicName == "max-weighted-dev") { + return AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown pivot selection heuristic '" << heuristicName << "'."); + } } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 9f95a5640..16fc2d9be 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -11,6 +11,10 @@ namespace storm { */ class AbstractionSettings : public ModuleSettings { public: + enum class PivotSelectionHeuristic { + NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation + }; + /*! * Creates a new set of abstraction settings. */ @@ -64,6 +68,13 @@ namespace storm { * @return The precision to use for detecting convergence. */ double getPrecision() const; + + /*! + * Retrieves the selected heuristic to select pivot blocks. + * + * @return The selected heuristic. + */ + PivotSelectionHeuristic getPivotSelectionHeuristic() const; const static std::string moduleName; @@ -76,6 +87,7 @@ namespace storm { const static std::string splitInterpolantsOptionName; const static std::string splitAllOptionName; const static std::string precisionOptionName; + const static std::string pivotHeuristicOptionName; }; }