From d7490a74cbc4bbf0ecd88e9beec974c54cdeddbc Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 25 Aug 2015 11:37:21 +0200 Subject: [PATCH] properties can now be given as string or file. both ways accept multiple formulas Former-commit-id: 60acecb951097aadd7cfa4ed732eda27b145bd72 --- src/parser/FormulaParser.cpp | 2 ++ src/settings/SettingsManager.cpp | 2 +- src/settings/modules/GeneralSettings.cpp | 24 +++++------------------- src/settings/modules/GeneralSettings.h | 16 +--------------- src/utility/cli.cpp | 16 +++++++++------- 5 files changed, 18 insertions(+), 42 deletions(-) diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 5acbba56c..882bc5ea6 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -202,6 +202,8 @@ namespace storm { STORM_LOG_DEBUG("Parsed formula successfully."); } catch (qi::expectation_failure 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; diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 96466d3c9..18225f712 100644 --- a/src/settings/SettingsManager.cpp +++ b/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. diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 10c717149..f3331d516 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/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; diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 1236e5429..648b455ef 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -145,20 +145,6 @@ namespace storm { * @return The property specified with the property option. */ 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; diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index 93ed85ab4..219e566ae 100644 --- a/src/utility/cli.cpp +++ b/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> formulas; if (settings.isPropertySet()) { - std::shared_ptr 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()) {