From b45497a8c4cee07c697982badd6fdc2851646db3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 30 Sep 2020 22:00:10 +0200 Subject: [PATCH] Added --propsasmulti switch to interpret input formulas as multi-objective formula --- src/storm-cli-utilities/model-handling.h | 6 ++++++ src/storm/api/properties.cpp | 13 +++++++++++++ src/storm/api/properties.h | 1 + src/storm/settings/modules/IOSettings.cpp | 8 ++++++++ src/storm/settings/modules/IOSettings.h | 6 ++++++ 5 files changed, 34 insertions(+) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index f630e67df..9fc3cc772 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -347,6 +347,12 @@ namespace storm { SymbolicInput output = input; + // Preprocess properties (if requested) + if (ioSettings.isPropertiesAsMultiSet()) { + STORM_LOG_THROW(!input.properties.empty(), storm::exceptions::InvalidArgumentException, "Can not translate properties to multi-objective formula because no properties were specified."); + output.properties = {storm::api::createMultiObjectiveProperty(output.properties)}; + } + // Substitute constant definitions in symbolic input. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); std::map constantDefinitions; diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index b1e36af86..bd07cb013 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -58,5 +58,18 @@ namespace storm { return formulas; } + storm::jani::Property createMultiObjectiveProperty(std::vector const& properties) { + std::set undefConstants; + std::string name = ""; + std::string comment = ""; + for (auto const& prop : properties) { + undefConstants.insert(prop.getUndefinedConstants().begin(), prop.getUndefinedConstants().end()); + name += prop.getName(); + comment += prop.getComment(); + STORM_LOG_WARN_COND(prop.getFilter().isDefault(), "Non-default property filter of property " + prop.getName() + " will be dropped during conversion to multi-objective property."); + } + auto multiFormula = std::make_shared(extractFormulasFromProperties(properties)); + return storm::jani::Property(name, multiFormula, undefConstants, comment); + } } } diff --git a/src/storm/api/properties.h b/src/storm/api/properties.h index c0c878f48..2df4a1fe1 100644 --- a/src/storm/api/properties.h +++ b/src/storm/api/properties.h @@ -33,6 +33,7 @@ namespace storm { std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution); std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); std::vector> extractFormulasFromProperties(std::vector const& properties); + storm::jani::Property createMultiObjectiveProperty(std::vector const& properties); } } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index dc438f231..7069c453a 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -50,6 +50,7 @@ namespace storm { const std::string IOSettings::qvbsInputOptionName = "qvbs"; const std::string IOSettings::qvbsInputOptionShortName = "qvbs"; const std::string IOSettings::qvbsRootOptionName = "qvbsroot"; + const std::string IOSettings::propertiesAsMultiOptionName = "propsasmulti"; std::string preventDRNPlaceholderOptionName = "no-drn-placeholders"; @@ -103,6 +104,9 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("instance-index", "The selected instance of this model.").setDefaultValueUnsignedInteger(0).makeOptional().build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The comma separated list of property names to check. Omit to check all, \"\" to check none.").setDefaultValueString("").makeOptional().build()) .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, propertiesAsMultiOptionName, false, "If set, the selected properties are interpreted as a multi-objective formula.").setIsAdvanced().build()); + #ifdef STORM_HAVE_QVBS std::string qvbsRootDefault = STORM_QVBS_ROOT; #else @@ -321,6 +325,10 @@ namespace storm { return path.getValueAsString(); } + bool IOSettings::isPropertiesAsMultiSet() const { + return this->getOption(propertiesAsMultiOptionName).getHasOptionBeenSet(); + } + void IOSettings::finalize() { // Intentionally left empty. } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 3f41bdce7..447913665 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -339,6 +339,11 @@ namespace storm { */ std::string getQvbsRoot() const; + /*! + * Retrieves whether the input properties are to be interpreted as a single multi-objective formula + */ + bool isPropertiesAsMultiSet() const; + bool check() const override; void finalize() override; @@ -377,6 +382,7 @@ namespace storm { static const std::string qvbsInputOptionName; static const std::string qvbsInputOptionShortName; static const std::string qvbsRootOptionName; + static const std::string propertiesAsMultiOptionName; };