diff --git a/src/settings/Argument.h b/src/settings/Argument.h index 6626ba35d..c697fdb45 100644 --- a/src/settings/Argument.h +++ b/src/settings/Argument.h @@ -106,7 +106,7 @@ namespace storm { * @return The value of the argument. */ T const& getArgumentValue() const { - STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was neither set nor specifies a default value."); + STORM_LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument '" << this->getName() << "', because it was neither set nor specifies a default value."); if (this->getHasBeenSet()) { return this->argumentValue; } else { diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index fb3f89352..45d3b58a6 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -30,6 +30,7 @@ namespace storm { const std::string GeneralSettings::transitionRewardsOptionName = "transrew"; const std::string GeneralSettings::stateRewardsOptionName = "staterew"; const std::string GeneralSettings::counterexampleOptionName = "counterexample"; + const std::string GeneralSettings::counterexampleOptionShortName = "cex"; const std::string GeneralSettings::dontFixDeadlockOptionName = "nofixdl"; const std::string GeneralSettings::dontFixDeadlockOptionShortName = "ndl"; const std::string GeneralSettings::timeoutOptionName = "timeout"; @@ -69,7 +70,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, ltlFileOptionName, false, "Specifies the LTL formulas that are to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).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.").build()).build()); + .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, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index e37030385..10e4aa77d 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -341,6 +341,7 @@ namespace storm { static const std::string transitionRewardsOptionName; static const std::string stateRewardsOptionName; static const std::string counterexampleOptionName; + static const std::string counterexampleOptionShortName; static const std::string dontFixDeadlockOptionName; static const std::string dontFixDeadlockOptionShortName; static const std::string timeoutOptionName;