properties can now be given as string or file. both ways accept multiple formulas

Former-commit-id: 60acecb951

src/parser/FormulaParser.cpp

@@ -202,6 +202,8 @@ namespace storm {
                 STORM_LOG_DEBUG("Parsed formula successfully.");
             } catch (qi::expectation_failure<PositionIteratorType> const& e) {
                 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
+//            } catch (std::exception const& e) {
+//                STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse formula: " << e.what());
             }
             
             return result;

src/settings/SettingsManager.cpp

@@ -89,7 +89,7 @@ namespace storm {
                 std::string const& currentArgument = commandLineArguments[i];
                 
                 // Check if the given argument is a new option or belongs to a previously given option.
-                if (currentArgument.at(0) == '-') {
+                if (!currentArgument.empty() && currentArgument.at(0) == '-') {
                     if (optionActive) {
                         // At this point we know that a new option is about to come. Hence, we need to assign the current
                         // cache content to the option that was active until now.

src/settings/modules/GeneralSettings.cpp

@@ -21,7 +21,7 @@ namespace storm {
             const std::string GeneralSettings::verboseOptionName = "verbose";
             const std::string GeneralSettings::verboseOptionShortName = "v";
             const std::string GeneralSettings::precisionOptionName = "precision";
-            const std::string GeneralSettings::precisionOptionShortName = "p";
+            const std::string GeneralSettings::precisionOptionShortName = "eps";
             const std::string GeneralSettings::exportDotOptionName = "exportdot";
             const std::string GeneralSettings::configOptionName = "config";
             const std::string GeneralSettings::configOptionShortName = "c";
@@ -30,7 +30,7 @@ namespace storm {
             const std::string GeneralSettings::symbolicOptionName = "symbolic";
             const std::string GeneralSettings::symbolicOptionShortName = "s";
             const std::string GeneralSettings::propertyOptionName = "prop";
-            const std::string GeneralSettings::propertyFileOptionName = "propfile";
+            const std::string GeneralSettings::propertyOptionShortName = "prop";
             const std::string GeneralSettings::transitionRewardsOptionName = "transrew";
             const std::string GeneralSettings::stateRewardsOptionName = "staterew";
             const std::string GeneralSettings::counterexampleOptionName = "counterexample";
@@ -75,10 +75,8 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies a PCTL formula that is to be checked on the model.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, propertyFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the PCTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the formulas to be checked on the model.").setShortName(propertyOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula or filename", "The formula or the file containing the formulas.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
@@ -176,15 +174,7 @@ namespace storm {
             }
             
             std::string GeneralSettings::getProperty() const {
-                return this->getOption(propertyOptionName).getArgumentByName("formula").getValueAsString();
-            }
-            
-            bool GeneralSettings::isPropertyFileSet() const {
-                return this->getOption(propertyFileOptionName).getHasOptionBeenSet();
-            }
-            
-            std::string GeneralSettings::getPropertiesFilename() const {
-                return this->getOption(propertyFileOptionName).getArgumentByName("filename").getValueAsString();
+                return this->getOption(propertyOptionName).getArgumentByName("formula or filename").getValueAsString();
             }
             
             bool GeneralSettings::isTransitionRewardsSet() const {
@@ -311,10 +301,6 @@ namespace storm {
                 // Ensure that the model was given either symbolically or explicitly.
                 STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
                 
-                // Make sure that one "source" for properties is given.
-                uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0);
-                STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both.");
-                
                 STORM_LOG_THROW(this->getEngine() == Engine::Sparse || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine.");
                 
                 return true;

src/settings/modules/GeneralSettings.h

@@ -146,20 +146,6 @@ namespace storm {
                  */
                 std::string getProperty() const;
 
-                /*!
-                 * Retrieves whether a property file was set.
-                 *
-                 * @return True iff a property was set.
-                 */
-                bool isPropertyFileSet() const;
-                
-                /*!
-                 * Retrieves the name of the file that contains the properties to be checked on the model.
-                 *
-                 * @return The name of the file that contains the properties to be checked on the model.
-                 */
-                std::string getPropertiesFilename() const;
-
                 /*!
                  * Retrieves whether the transition reward option was set.
                  *
@@ -359,7 +345,7 @@ namespace storm {
                 static const std::string symbolicOptionName;
                 static const std::string symbolicOptionShortName;
                 static const std::string propertyOptionName;
-                static const std::string propertyFileOptionName;
+                static const std::string propertyOptionShortName;
                 static const std::string transitionRewardsOptionName;
                 static const std::string stateRewardsOptionName;
                 static const std::string counterexampleOptionName;

src/utility/cli.cpp

@@ -220,17 +220,19 @@ namespace storm {
                 // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
                 std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
                 if (settings.isPropertySet()) {
-					std::shared_ptr<storm::logic::Formula> formula;
+                    storm::parser::FormulaParser formulaParser;
                     if (program) {
                         storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
-                        formula = formulaParser.parseSingleFormulaFromString(settings.getProperty());
+                    }
+                    
+                    // If the given property looks like a file (containing a dot and there exists a file with that name),
+                    // we try to parse it as a file, otherwise we assume it's a property.
+                    std::string property = settings.getProperty();
+                    if (property.find(".") != std::string::npos && std::ifstream(property).good()) {
+                        formulas = formulaParser.parseFromFile(settings.getProperty());
                     } else {
-                        storm::parser::FormulaParser formulaParser;
-                        formula = formulaParser.parseSingleFormulaFromString(settings.getProperty());
+                        formulas = formulaParser.parseFromString(settings.getProperty());
                     }
-					formulas.push_back(formula);
-                } else if (settings.isPropertyFileSet()) {
-                        // FIXME: asap.
                 }
 
                 if (settings.isSymbolicSet()) {