From 26320049a65675909162594a264a0e8b108e95fc Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 27 Nov 2016 21:28:56 +0100 Subject: [PATCH] more options and bugfix --- src/storm/abstraction/MenuGameAbstractor.h | 2 +- src/storm/abstraction/MenuGameRefiner.cpp | 38 ++++++++------- src/storm/abstraction/MenuGameRefiner.h | 11 +++-- .../prism/PrismMenuGameAbstractor.cpp | 11 +---- .../prism/PrismMenuGameAbstractor.h | 9 +--- .../abstraction/GameBasedMdpModelChecker.cpp | 46 +++++++++++-------- .../settings/modules/AbstractionSettings.cpp | 11 +++++ .../settings/modules/AbstractionSettings.h | 18 +++++++- 8 files changed, 83 insertions(+), 63 deletions(-) diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 281264a48..c4657e4fb 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -29,7 +29,7 @@ namespace storm { virtual std::map getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0; /// Methods to refine the abstraction. - virtual void refine(std::vector const& commands) = 0; + virtual void refine(RefinementCommand const& command) = 0; /// Exports a representation of the current abstraction state in the dot format. virtual void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const = 0; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index ce8fc573d..a370b0b29 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -12,7 +12,7 @@ namespace storm { namespace abstraction { template - MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), splitPredicates(storm::settings::getModule().isSplitPredicatesSet()), splitter(), equivalenceChecker(std::move(smtSolver)) { + MenuGameRefiner::MenuGameRefiner(MenuGameAbstractor& abstractor, std::unique_ptr&& smtSolver) : abstractor(abstractor), splitPredicates(storm::settings::getModule().isSplitPredicatesSet()), splitGuards(storm::settings::getModule().isSplitGuardsSet()), splitter(), equivalenceChecker(std::move(smtSolver)) { if (storm::settings::getModule().isAddAllGuardsSet()) { std::vector guards; @@ -21,7 +21,7 @@ namespace storm { for (uint64_t index = player1Choices.first; index < player1Choices.second; ++index) { guards.push_back(this->abstractor.get().getGuard(index)); } - performRefinement(createGlobalRefinement(guards)); + performRefinement(createGlobalRefinement(preprocessPredicates(guards, storm::settings::getModule().isSplitInitialGuardsSet()))); } } @@ -74,9 +74,10 @@ namespace storm { } template - storm::expressions::Expression MenuGameRefiner::derivePredicateFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { + std::pair MenuGameRefiner::derivePredicateFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const { // Prepare result. storm::expressions::Expression newPredicate; + bool fromGuard = false; // Get abstraction informatin for easier access. AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); @@ -95,6 +96,7 @@ namespace storm { if (buttomStateSuccessor) { STORM_LOG_TRACE("One of the successors is a bottom state, taking a guard as a new predicate."); newPredicate = abstractor.get().getGuard(player1Index); + fromGuard = true; STORM_LOG_DEBUG("Derived new predicate (based on guard): " << newPredicate); } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); @@ -130,7 +132,7 @@ namespace storm { for (auto const& predicate : abstractionInformation.getPredicates()) { STORM_LOG_TRACE(predicate); } - return newPredicate; + return std::make_pair(newPredicate, fromGuard); } template @@ -169,7 +171,7 @@ namespace storm { } template - storm::expressions::Expression MenuGameRefiner::derivePredicateFromPivotState(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 { + std::pair MenuGameRefiner::derivePredicateFromPivotState(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 { // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); @@ -182,7 +184,7 @@ namespace storm { STORM_LOG_TRACE("Refining based on lower choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - storm::expressions::Expression newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + std::pair newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); return newPredicate; @@ -195,7 +197,7 @@ namespace storm { if (upperChoicesDifferent) { STORM_LOG_TRACE("Refining based on upper choice."); auto refinementStart = std::chrono::high_resolution_clock::now(); - storm::expressions::Expression newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + std::pair newPredicate = derivePredicateFromDifferingChoices(pivotState, (pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); auto refinementEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); return newPredicate; @@ -234,8 +236,8 @@ namespace storm { storm::dd::Bdd pivotState = pickPivotStateWithMinimalDistance(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates); // Derive predicate based on the selected pivot state. - storm::expressions::Expression newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); - std::vector preparedPredicates = preprocessPredicates({newPredicate}); + std::pair newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + std::vector preparedPredicates = preprocessPredicates({newPredicate.first}, (newPredicate.second && splitGuards) || (!newPredicate.second && splitPredicates)); performRefinement(createGlobalRefinement(preparedPredicates)); return true; } @@ -262,15 +264,15 @@ namespace storm { storm::dd::Bdd pivotState = pickPivotStateWithMinimalDistance(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates); // Derive predicate based on the selected pivot state. - storm::expressions::Expression newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); - std::vector preparedPredicates = preprocessPredicates({newPredicate}); + std::pair newPredicate = derivePredicateFromPivotState(game, pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); + std::vector preparedPredicates = preprocessPredicates({newPredicate.first}, (newPredicate.second && splitGuards) || (!newPredicate.second && splitPredicates)); performRefinement(createGlobalRefinement(preparedPredicates)); return true; } template - std::vector MenuGameRefiner::preprocessPredicates(std::vector const& predicates) const { - if (splitPredicates) { + std::vector MenuGameRefiner::preprocessPredicates(std::vector const& predicates, bool split) const { + if (split) { std::vector cleanedAtoms; for (auto const& predicate : predicates) { @@ -314,19 +316,15 @@ namespace storm { template std::vector MenuGameRefiner::createGlobalRefinement(std::vector const& predicates) const { std::vector commands; - - // std::pair player1Choices = abstractor.get().getPlayer1ChoiceRange(); - // for (uint64_t index = player1Choices.first; index < player1Choices.second; ++index) { - // commands.emplace_back(index, predicates); - // } commands.emplace_back(predicates); - return commands; } template void MenuGameRefiner::performRefinement(std::vector const& refinementCommands) const { - abstractor.get().refine(refinementCommands); + for (auto const& command : refinementCommands) { + abstractor.get().refine(command); + } } template class MenuGameRefiner; diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index a284966b9..e5be859c4 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -53,13 +53,13 @@ namespace storm { bool refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QuantitativeResultMinMax const& quantitativeResult) const; private: - storm::expressions::Expression derivePredicateFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; - storm::expressions::Expression derivePredicateFromPivotState(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; + std::pair derivePredicateFromDifferingChoices(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) const; + std::pair derivePredicateFromPivotState(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; /*! * Preprocesses the predicates. */ - std::vector preprocessPredicates(std::vector const& predicates) const; + std::vector preprocessPredicates(std::vector const& predicates, bool allowSplits) const; /*! * Creates a set of refinement commands that amounts to splitting all player 1 choices with the given set of predicates. @@ -73,7 +73,10 @@ namespace storm { /// A flag indicating whether predicates shall be split before using them for refinement. bool splitPredicates; - + + /// A flag indicating whether predicates shall be split before using them for refinement. + bool splitGuards; + /// An object that can be used for splitting predicates. mutable storm::expressions::PredicateSplitter splitter; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index f9b8479a0..9727cb7c0 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -72,15 +72,6 @@ namespace storm { commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); } - template - void PrismMenuGameAbstractor::refine(std::vector const& commands) { - for (auto const& command : commands) { - STORM_LOG_THROW(!command.refersToPlayer1Choice(), storm::exceptions::NotSupportedException, "Currently only global refinement is supported."); - refine(command); - refinementPerformed |= !command.getPredicates().empty(); - } - } - template void PrismMenuGameAbstractor::refine(RefinementCommand const& command) { // Add the predicates to the global list of predicates and gather their indices. @@ -97,6 +88,8 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(predicateIndices); + + refinementPerformed |= !command.getPredicates().empty(); } template diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h index bef998346..6c8835b9c 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h @@ -93,19 +93,12 @@ namespace storm { */ storm::dd::Bdd getStates(storm::expressions::Expression const& predicate); - /*! - * Performs the given refinement commands. - * - * @param commands The commands to perform. - */ - virtual void refine(std::vector const& commands) override; - /*! * Performs the given refinement command. * * @param command The command to perform. */ - void refine(RefinementCommand const& command); + virtual void refine(RefinementCommand const& command) override; /*! * Exports the current state of the abstraction in the dot format to the given file. diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 5a7c31d97..dedd850a9 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -211,14 +211,32 @@ namespace storm { QuantitativeResult computeQuantitativeResult(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame const& game, QualitativeResultMinMax const& qualitativeResult, storm::dd::Add const& initialStatesAdd, storm::dd::Bdd const& maybeStates, boost::optional> const& startInfo = boost::none) { bool min = player2Direction == storm::OptimizationDirection::Minimize; + QuantitativeResult result; // The minimal value after qualitative checking can only be zero. If it was 1, we could have given // the result right away. Similarly, the maximal value can only be one at this point. - ValueType initialStateValue = min ? storm::utility::zero() : storm::utility::one(); + result.initialStateValue = min ? storm::utility::zero() : storm::utility::one(); - QuantitativeResult result; + // We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative + // preprocessing if possible. + storm::dd::Bdd combinedPlayer1QualitativeStrategies; + storm::dd::Bdd combinedPlayer2QualitativeStrategies; + if (min) { + combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer1Strategy() || qualitativeResult.prob1Min.getPlayer1Strategy()); + combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer2Strategy() || qualitativeResult.prob1Min.getPlayer2Strategy()); + } else { + combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer1Strategy() || qualitativeResult.prob1Max.getPlayer1Strategy()); + combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy()); + } + + result.player1Strategy = combinedPlayer1QualitativeStrategies; + result.player2Strategy = combinedPlayer2QualitativeStrategies; + result.values = game.getManager().template getAddZero(); + auto start = std::chrono::high_resolution_clock::now(); if (!maybeStates.isZero()) { + STORM_LOG_TRACE("Solving " << maybeStates.getNonZeroCount() << " maybe states."); + // Solve the quantitative values of maybe states. result = solveMaybeStates(player1Direction, player2Direction, game, maybeStates, min ? qualitativeResult.prob1Min.getPlayer1States() : qualitativeResult.prob1Max.getPlayer1States(), startInfo); @@ -233,24 +251,12 @@ namespace storm { storm::dd::Add initialStateValueAdd = initialStatesAdd * result.values; // For min, we can only require a non-zero count of *at most* one, because the result may actually be 0. STORM_LOG_ASSERT((!min || initialStateValueAdd.getNonZeroCount() == 1) && (min || initialStateValueAdd.getNonZeroCount() <= 1), "Wrong number of results for initial states. Expected " << (min ? "<= 1" : "1") << ", but got " << initialStateValueAdd.getNonZeroCount() << "."); - result.initialStateValue = initialStateValue = initialStateValueAdd.getMax(); - - // Finally, we fix the strategies. That is, we take the decisions of the strategies obtained in the - // qualitiative preprocessing if possible. - storm::dd::Bdd combinedPlayer1QualitativeStrategies; - storm::dd::Bdd combinedPlayer2QualitativeStrategies; - if (min) { - combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer1Strategy() || qualitativeResult.prob1Min.getPlayer1Strategy()); - combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Min.getPlayer2Strategy() || qualitativeResult.prob1Min.getPlayer2Strategy()); - } else { - combinedPlayer1QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer1Strategy() || qualitativeResult.prob1Max.getPlayer1Strategy()); - combinedPlayer2QualitativeStrategies = (qualitativeResult.prob0Max.getPlayer2Strategy() || qualitativeResult.prob1Max.getPlayer2Strategy()); - } + result.initialStateValue = result.initialStateValue = initialStateValueAdd.getMax(); result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy); result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy); } else { - result = QuantitativeResult(initialStateValue, game.getManager().template getAddZero(), game.getManager().getBddZero(), game.getManager().getBddZero()); + STORM_LOG_TRACE("No maybe states."); } auto end = std::chrono::high_resolution_clock::now(); @@ -369,10 +375,10 @@ namespace storm { } // Make sure that all strategies are still valid strategies. - STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); - STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); - STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.isZero() || quantitativeResult.min.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.isZero() || quantitativeResult.max.player1Strategy.template toAdd().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal."); + STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.isZero() || quantitativeResult.min.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); + STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.isZero() || quantitativeResult.max.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); // (10) If we arrived at this point, it means that we have all qualitative and quantitative // information about the game, but we could not yet answer the query. In this case, we need to refine. diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 0ba299dbf..84299e260 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -10,10 +10,14 @@ namespace storm { const std::string AbstractionSettings::moduleName = "abstraction"; const std::string AbstractionSettings::addAllGuardsOptionName = "allguards"; const std::string AbstractionSettings::splitPredicatesOptionName = "split-preds"; + const std::string AbstractionSettings::splitInitialGuardsOptionName = "split-init-guards"; + const std::string AbstractionSettings::splitGuardsOptionName = "split-guards"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, splitPredicatesOptionName, true, "Sets whether the predicates are split into atoms before they are added.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, splitInitialGuardsOptionName, true, "Sets whether the initial guards are split into atoms before they are added.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, splitGuardsOptionName, true, "Sets whether the guards are split into atoms before they are added.").build()); } bool AbstractionSettings::isAddAllGuardsSet() const { @@ -23,7 +27,14 @@ namespace storm { bool AbstractionSettings::isSplitPredicatesSet() const { return this->getOption(splitPredicatesOptionName).getHasOptionBeenSet(); } + + bool AbstractionSettings::isSplitInitialGuardsSet() const { + return this->getOption(splitInitialGuardsOptionName).getHasOptionBeenSet(); + } + bool AbstractionSettings::isSplitGuardsSet() const { + return this->getOption(splitGuardsOptionName).getHasOptionBeenSet(); + } } } } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 144ca289a..30c699ac1 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -29,12 +29,28 @@ namespace storm { * @return True iff the option was set. */ bool isSplitPredicatesSet() const; - + + /*! + * Retrieves whether the option to split the initially added guards to atoms was set. + * + * @return True iff the option was set. + */ + bool isSplitInitialGuardsSet() const; + + /*! + * Retrieves whether the option to split guards derived later to atoms was set. + * + * @return True iff the option was set. + */ + bool isSplitGuardsSet() const; + const static std::string moduleName; private: const static std::string addAllGuardsOptionName; const static std::string splitPredicatesOptionName; + const static std::string splitInitialGuardsOptionName; + const static std::string splitGuardsOptionName; }; }