From 4a0134797cbda1add3154ac9c91ae77d71ca8d28 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 31 May 2018 17:08:40 +0200 Subject: [PATCH] option to add initial predicates --- src/storm/abstraction/MenuGameAbstractor.h | 2 +- src/storm/abstraction/MenuGameRefiner.cpp | 4 ++++ src/storm/abstraction/MenuGameRefiner.h | 2 +- .../abstraction/prism/PrismMenuGameAbstractor.cpp | 2 +- src/storm/settings/modules/AbstractionSettings.cpp | 12 +++++++++++- src/storm/settings/modules/AbstractionSettings.h | 8 ++++++++ 6 files changed, 26 insertions(+), 4 deletions(-) diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index f55a7f236..1887d60ec 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -76,7 +76,7 @@ namespace storm { * computation. */ virtual void notifyGuardsArePredicates() = 0; - + protected: bool isRestrictToRelevantStatesSet() const; diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 25c4242ba..4ebfc24ce 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -93,6 +93,10 @@ namespace storm { this->abstractor.get().notifyGuardsArePredicates(); addedAllGuardsFlag = true; } + if (abstractionSettings.isAddAllInitialExpressionsSet()) { + storm::expressions::Expression initialExpression = this->abstractor.get().getInitialExpression(); + performRefinement(createGlobalRefinement(preprocessPredicates({initialExpression}, RefinementPredicates::Source::InitialExpression))); + } if (abstractionSettings.isInjectRefinementPredicatesSet()) { std::string predicatesString = abstractionSettings.getInjectedRefinementPredicates(); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 60d632694..c906fa9cd 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -40,7 +40,7 @@ namespace storm { class RefinementPredicates { public: enum class Source { - WeakestPrecondition, InitialGuard, Guard, Interpolation, Manual + WeakestPrecondition, InitialGuard, InitialExpression, Guard, Interpolation, Manual }; RefinementPredicates() = default; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 7370645ac..88d75b50f 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -276,7 +276,7 @@ namespace storm { module.notifyGuardsArePredicates(); } } - + // Explicitly instantiate the class. template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 8153b8e2c..ace89c635 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -17,6 +17,7 @@ namespace storm { const std::string AbstractionSettings::useDecompositionOptionName = "decomposition"; const std::string AbstractionSettings::splitModeOptionName = "split"; const std::string AbstractionSettings::addAllGuardsOptionName = "all-guards"; + const std::string AbstractionSettings::addInitialExpressionsOptionName = "all-inits"; const std::string AbstractionSettings::useInterpolationOptionName = "interpolation"; const std::string AbstractionSettings::precisionOptionName = "precision"; const std::string AbstractionSettings::relativeOptionName = "relative"; @@ -65,7 +66,12 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) .setDefaultValueString("on").build()) .build()); - + + this->addOption(storm::settings::OptionBuilder(moduleName, addInitialExpressionsOptionName, true, "Sets whether all initial expressions are added as initial predicates.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("on").build()) + .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, useInterpolationOptionName, true, "Sets whether interpolation is to be used to eliminate spurious pivot blocks.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) .setDefaultValueString("on").build()) @@ -166,6 +172,10 @@ namespace storm { return this->getOption(addAllGuardsOptionName).getArgumentByName("value").getValueAsString() == "on"; } + bool AbstractionSettings::isAddAllInitialExpressionsSet() const { + return this->getOption(addInitialExpressionsOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + void AbstractionSettings::setAddAllGuards(bool value) { this->getOption(addAllGuardsOptionName).getArgumentByName("value").setFromStringValue(value ? "on" : "off"); } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 95f1e3e36..5e2e8fdbc 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -62,6 +62,13 @@ namespace storm { */ bool isAddAllGuardsSet() const; + /*! + * Retrieves whether the option to add all initial expressions was set. + * + * @return True iff the option was set. + */ + bool isAddAllInitialExpressionsSet() const; + /*! * Sets the option to add all guards to the specified value. * @@ -179,6 +186,7 @@ namespace storm { const static std::string useDecompositionOptionName; const static std::string splitModeOptionName; const static std::string addAllGuardsOptionName; + const static std::string addInitialExpressionsOptionName; const static std::string useInterpolationOptionName; const static std::string precisionOptionName; const static std::string relativeOptionName;