Added --propsasmulti switch to interpret input formulas as multi-objective formula

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<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;

src/storm/api/properties.cpp

@@ -58,5 +58,18 @@ namespace storm {
             return formulas;
         }
         
+        storm::jani::Property createMultiObjectiveProperty(std::vector<storm::jani::Property> const& properties) {
+            std::set<storm::expressions::Variable> 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<storm::logic::MultiObjectiveFormula>(extractFormulasFromProperties(properties));
+            return storm::jani::Property(name, multiFormula, undefConstants, comment);
+        }
     }
 }

src/storm/api/properties.h

@@ -33,6 +33,7 @@ namespace storm {
         std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
         std::vector<storm::jani::Property> filterProperties(std::vector<storm::jani::Property> const& properties, boost::optional<std::set<std::string>> const& propertyFilter);
         std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties);
+        storm::jani::Property createMultiObjectiveProperty(std::vector<storm::jani::Property> const& properties);
 
     }
 }

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.
             }

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;
 
             };