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<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;
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<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()) {