diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index b927b6203..80ba611aa 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -494,7 +494,7 @@ namespace storm {
storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
- constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
+ constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue());
}
constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k");
@@ -512,7 +512,7 @@ namespace storm {
storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
for (auto element : transitionMatrix.getRow(choice)) {
- constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
+ constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue());
}
storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index d8b9284d9..26fb6070d 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -110,14 +110,42 @@ namespace storm {
if (optionActive) {
setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
}
+
+ // Include the options from a possibly specified configuration file, but don't overwrite existing settings.
+ if (storm::settings::generalSettings().isConfigSet()) {
+ this->setFromConfigurationFile(storm::settings::generalSettings().getConfigFilename());
+ }
+
+ // Finally, check whether all modules are okay with the current settings.
+ this->checkAllModules();
}
void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
- STORM_LOG_ASSERT(false, "Not yet implemented.");
+ std::map<std::string, std::vector<std::string>> configurationFileSettings = parseConfigFile(configFilename);
+
+ for (auto const& optionArgumentsPair : configurationFileSettings) {
+ auto options = this->longNameToOptions.find(optionArgumentsPair.first);
+
+ // We don't need to check whether this option exists or not, because this is already checked when
+ // parsing the configuration file.
+
+ // Now go through all the matching options and set them according to the values.
+ for (auto option : options->second) {
+ if (option->getHasOptionBeenSet()) {
+ // If the option was already set from the command line, we issue a warning and ignore the
+ // settings from the configuration file.
+ STORM_LOG_WARN("The option '" << option->getLongName() << "' of module '" << option->getModuleName() << "' has been set in the configuration file '" << configFilename << "', but was overwritten on the command line." << std::endl);
+ } else {
+ // If, however, the option has not been set yet, we try to assign values ot its arguments
+ // based on the argument strings.
+ setOptionArguments(optionArgumentsPair.first, option, optionArgumentsPair.second);
+ }
+ }
+ }
}
void SettingsManager::printHelp(std::string const& hint) const {
- std::cout << "usage: storm [options]" << std::endl << std::endl;
+ STORM_PRINT("usage: storm [options]" << std::endl << std::endl);
if (hint == "all") {
// Find longest option name.
@@ -166,7 +194,7 @@ namespace storm {
// Print the matching modules.
uint_fast64_t maxLength = std::max(maxLengthModules, maxLengthOptions);
if (matchingModuleNames.size() > 0) {
- std::cout << "Matching modules for hint '" << hint << "':" << std::endl;
+ STORM_PRINT("Matching modules for hint '" << hint << "':" << std::endl)
for (auto const& matchingModuleName : matchingModuleNames) {
printHelpForModule(matchingModuleName, maxLength);
}
@@ -174,14 +202,14 @@ namespace storm {
// Print the matching options.
if (matchingOptions.size() > 0) {
- std::cout << "Matching options for hint '" << hint << "':" << std::endl;
+ STORM_PRINT("Matching options for hint '" << hint << "':" << std::endl);
for (auto const& option : matchingOptions) {
- std::cout << std::setw(maxLength) << std::left << *option << std::endl;
+ STORM_PRINT(std::setw(maxLength) << std::left << *option << std::endl);
}
}
if (matchingModuleNames.empty() && matchingOptions.empty()) {
- std::cout << "Hint '" << hint << "' did not match any modules or options." << std::endl;
+ STORM_PRINT("Hint '" << hint << "' did not match any modules or options." << std::endl);
}
}
}
@@ -189,20 +217,16 @@ namespace storm {
void SettingsManager::printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength) const {
auto moduleIterator = moduleOptions.find(moduleName);
STORM_LOG_THROW(moduleIterator != moduleOptions.end(), storm::exceptions::IllegalFunctionCallException, "Cannot print help for unknown module '" << moduleName << "'.");
- std::cout << "##### Module '" << moduleName << "' ";
- for (uint_fast64_t i = 0; i < std::min(maxLength, maxLength - moduleName.length() - 16); ++i) {
- std::cout << "#";
- }
- std::cout << std::endl;
+ STORM_PRINT("##### Module '" << moduleName << "' " << std::string(std::min(maxLength, maxLength - moduleName.length() - 16), '#') << std::endl);
// Save the flags for std::cout so we can manipulate them and be sure they will be restored as soon as this
// stream goes out of scope.
boost::io::ios_flags_saver out(std::cout);
for (auto const& option : moduleIterator->second) {
- std::cout << std::setw(maxLength) << std::left << *option << std::endl;
+ STORM_PRINT(std::setw(maxLength) << std::left << *option << std::endl);
}
- std::cout << std::endl;
+ STORM_PRINT(std::endl);
}
uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
@@ -290,27 +314,32 @@ namespace storm {
return true;
}
+ void SettingsManager::setOptionArguments(std::string const& optionName, std::shared_ptr<Option> option, std::vector<std::string> const& argumentCache) {
+ STORM_LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
+
+ // Now set the provided argument values one by one.
+ for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {
+ ArgumentBase& argument = option->getArgument(i);
+ bool conversionOk = argument.setFromStringValue(argumentCache[i]);
+ STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed.");
+ }
+
+ // In case there are optional arguments that were not set, we set them to their default value.
+ for (uint_fast64_t i = argumentCache.size(); i < option->getArgumentCount(); ++i) {
+ ArgumentBase& argument = option->getArgument(i);
+ argument.setFromDefaultValue();
+ }
+
+ option->setHasOptionBeenSet();
+ }
+
void SettingsManager::setOptionsArguments(std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap, std::vector<std::string> const& argumentCache) {
auto optionIterator = optionMap.find(optionName);
STORM_LOG_THROW(optionIterator != optionMap.end(), storm::exceptions::OptionParserException, "Unknown option '" << optionName << "'.");
// Iterate over all options and set the arguments.
for (auto& option : optionIterator->second) {
- option->setHasOptionBeenSet();
- STORM_LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
-
- // Now set the provided argument values one by one.
- for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {
- ArgumentBase& argument = option->getArgument(i);
- bool conversionOk = argument.setFromStringValue(argumentCache[i]);
- STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed.");
- }
-
- // In case there are optional arguments that were not set, we set them to their default value.
- for (uint_fast64_t i = argumentCache.size(); i < option->getArgumentCount(); ++i) {
- ArgumentBase& argument = option->getArgument(i);
- argument.setFromDefaultValue();
- }
+ setOptionArguments(optionName, option, argumentCache);
}
}
@@ -325,6 +354,105 @@ namespace storm {
}
}
+ void SettingsManager::checkAllModules() const {
+ for (auto const& nameModulePair : this->modules) {
+ nameModulePair.second->check();
+ }
+ }
+
+ std::map<std::string, std::vector<std::string>> SettingsManager::parseConfigFile(std::string const& filename) const {
+ std::map<std::string, std::vector<std::string>> result;
+
+ std::ifstream input(filename);
+ STORM_LOG_THROW(input.good(), storm::exceptions::OptionParserException, "Could not read from config file '" << filename << "'.");
+
+ bool globalScope = true;
+ std::string activeModule = "";
+ uint_fast64_t lineNumber = 1;
+ for (std::string line; getline(input, line); ++lineNumber) {
+ // If the first character of the line is a "[", we expect the settings of a new module to start and
+ // the line to be of the shape [<module>].
+ if (line.at(0) == '[') {
+ STORM_LOG_THROW(line.at(0) == '[' && line.find("]") == line.length() - 1 && line.find("[", 1) == line.npos, storm::exceptions::OptionParserException, "Illegal module name header in configuration file '" << filename << " in line " << std::to_string(lineNumber) << ". Expected [<module>] where <module> is a placeholder for a known module.");
+
+ // Extract the module name and check whether it's a legal one.
+ std::string moduleName = line.substr(1, line.length() - 2);
+ STORM_LOG_THROW(moduleName != "" && (moduleName == "global" || (this->modules.find(moduleName) != this->modules.end())), storm::exceptions::OptionParserException, "Module header in configuration file '" << filename << " in line " << std::to_string(lineNumber) << " refers to unknown module '" << moduleName << ".");
+
+ // If the module name is "global", we unset the currently active module and treat all options to follow as unprefixed.
+ if (moduleName == "global") {
+ globalScope = true;
+ } else {
+ activeModule = moduleName;
+ globalScope = false;
+ }
+ } else {
+ // In this case, we expect the line to be of the shape o or o=a b c, where o is an option and a, b
+ // and c are the values that are supposed to be assigned to the arguments of the option.
+ std::size_t assignmentSignIndex = line.find("=");
+ bool containsAssignment = false;
+ if (assignmentSignIndex != line.npos) {
+ containsAssignment = true;
+ }
+
+ std::string optionName;
+ if (containsAssignment) {
+ optionName = line.substr(0, assignmentSignIndex);
+ } else {
+ optionName = line;
+ }
+
+ if (globalScope) {
+ STORM_LOG_THROW(this->longNameToOptions.find(optionName) != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Option assignment in configuration file '" << filename << " in line " << lineNumber << " refers to unknown option '" << optionName << "'.");
+ } else {
+ STORM_LOG_THROW(this->longNameToOptions.find(activeModule + ":" + optionName) != this->longNameToOptions.end(), storm::exceptions::OptionParserException, "Option assignment in configuration file '" << filename << " in line " << lineNumber << " refers to unknown option '" << activeModule << ":" << optionName << "'.");
+ }
+
+ std::string fullOptionName = (!globalScope ? activeModule + ":" : "") + optionName;
+ STORM_LOG_WARN_COND(result.find(fullOptionName) == result.end(), "Option '" << fullOptionName << "' is set in line " << lineNumber << " of configuration file " << filename << ", but has been set before.");
+
+ // If the current line is an assignment, split the right-hand side of the assignment into parts
+ // enclosed by quotation marks.
+ if (containsAssignment) {
+ std::string assignedValues = line.substr(assignmentSignIndex + 1);
+ std::vector<std::string> argumentCache;
+
+ // As horrible as it may look, this regular expression matches either a quoted string (possibly
+ // containing escaped quotes) or a simple word (without whitespaces and quotes).
+ std::regex argumentRegex("\"(([^\\\\\"]|((\\\\\\\\)*\\\\\")|\\\\[^\"])*)\"|(([^ \\\\\"]|((\\\\\\\\)*\\\\\")|\\\\[^\"])+)");
+ boost::algorithm::trim_left(assignedValues);
+
+ while (!assignedValues.empty()) {
+ std::smatch match;
+ bool hasMatch = std::regex_search(assignedValues, match, argumentRegex);
+
+ // If the input could not be matched, we have a parsing error.
+ STORM_LOG_THROW(hasMatch, storm::exceptions::OptionParserException, "Parsing error in configuration file '" << filename << "' in line " << lineNumber << ". Unexpected input '" << assignedValues << "'.");
+
+ // Extract the matched argument and cut off the quotation marks if necessary.
+ std::string matchedArgument = std::string(match[0].first, match[0].second);
+ if (matchedArgument.at(0) == '"') {
+ matchedArgument = matchedArgument.substr(1, matchedArgument.length() - 2);
+ }
+ argumentCache.push_back(matchedArgument);
+
+ assignedValues = assignedValues.substr(match.length());
+ boost::algorithm::trim_left(assignedValues);
+ }
+
+
+ // After successfully parsing the argument values, we store them in the result map.
+ result.emplace(fullOptionName, argumentCache);
+ } else {
+ // In this case, we can just insert the option to indicate it should be set (without arguments).
+ result.emplace(fullOptionName, std::vector<std::string>());
+ }
+ }
+ }
+
+ return result;
+ }
+
SettingsManager const& manager() {
return SettingsManager::manager();
}
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 94d309813..41383f336 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -8,6 +8,7 @@
#include <utility>
#include <functional>
#include <unordered_map>
+#include <map>
#include <vector>
#include <memory>
@@ -156,6 +157,15 @@ namespace storm {
*/
void addOption(std::shared_ptr<Option> const& option);
+ /*!
+ * Sets the arguments of the given option from the provided strings.
+ *
+ * @param optionName The name of the option. This is only used for error output.
+ * @param option The option for which to set the arguments.
+ * @param argumentCache The arguments of the option as string values.
+ */
+ static void setOptionArguments(std::string const& optionName, std::shared_ptr<Option> option, std::vector<std::string> const& argumentCache);
+
/*!
* Sets the arguments of the options matching the given name from the provided strings.
*
@@ -179,6 +189,11 @@ namespace storm {
*/
static void addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap);
+ /*!
+ * Checks all modules for consistency by calling their respective check method.
+ */
+ void checkAllModules() const;
+
/*!
* Retrieves the (print) length of the longest option of all modules.
*
@@ -193,6 +208,14 @@ namespace storm {
* @return The length of the longest option name.
*/
uint_fast64_t getPrintLengthOfLongestOption(std::string const& moduleName) const;
+
+ /*!
+ * Parses the given file and stores the settings in the returned map.
+ *
+ * @param filename The name of the file that is to be scanned for settings.
+ * @return A mapping of option names to the argument values (represented as strings).
+ */
+ std::map<std::string, std::vector<std::string>> parseConfigFile(std::string const& filename) const;
};
/*!
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp
index e2e29834d..6191b1643 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -1,6 +1,7 @@
#include "src/settings/modules/CounterexampleGeneratorSettings.h"
#include "src/settings/SettingsManager.h"
+#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace settings {
@@ -19,7 +20,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
}
- bool CounterexampleGeneratorSettings::isMinimalCommandGenerationSet() const {
+ bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const {
return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
}
@@ -40,6 +41,18 @@ namespace storm {
return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
}
+ bool CounterexampleGeneratorSettings::check() const {
+ // Ensure that the model was given either symbolically or explicitly.
+ STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically.");
+
+ if (isMinimalCommandSetGenerationSet()) {
+ STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
+ STORM_LOG_WARN_COND(isUseMilpBasedMinimalCommandSetGenerationSet() || !isUseSchedulerCutsSet(), "Using scheduler cuts is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
+ }
+
+ return true;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h
index 680224b5a..049747183 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.h
+++ b/src/settings/modules/CounterexampleGeneratorSettings.h
@@ -24,7 +24,7 @@ namespace storm {
*
* @return True iff a minimal command set counterexample is to be generated.
*/
- bool isMinimalCommandGenerationSet() const;
+ bool isMinimalCommandSetGenerationSet() const;
/*!
* Retrieves whether the MILP-based technique is to be used to generate a minimal command set
@@ -58,6 +58,8 @@ namespace storm {
*/
bool isUseSchedulerCutsSet() const;
+ bool check() const override;
+
// The name of the module.
static const std::string moduleName;
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 45d3b58a6..585bcfdfb 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -2,6 +2,7 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
+#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace settings {
@@ -266,6 +267,17 @@ namespace storm {
return this->getOption(statisticsOptionName).getHasOptionBeenSet();
}
+ bool GeneralSettings::check() const {
+ // 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 + (isPctlPropertySet() ? 1 : 0) + (isPctlFileSet() ? 1 : 0) + (isCslPropertySet() ? + 1 : 0) + (isCslFileSet() ? 1 : 0) + (isLtlPropertySet() ? 1 : 0) + (isLtlFileSet() ? 1 : 0);
+ STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify exactly one source of properties.");
+
+ return true;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 10e4aa77d..75f48d8f1 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -313,6 +313,8 @@ namespace storm {
* @return True iff statistics are to be shown for counterexample generation.
*/
bool isShowStatisticsSet() const;
+
+ bool check() const override;
// The name of the module.
static const std::string moduleName;
diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp
index c45eb93a5..030a69006 100644
--- a/src/settings/modules/GlpkSettings.cpp
+++ b/src/settings/modules/GlpkSettings.cpp
@@ -19,10 +19,22 @@ namespace storm {
return this->getOption(outputOptionName).getHasOptionBeenSet();
}
+ bool GlpkSettings::isIntegerToleranceSet() const {
+ return this->getOption(integerToleranceOption).getHasOptionBeenSet();
+ }
+
double GlpkSettings::getIntegerTolerance() const {
return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
+ bool GlpkSettings::check() const {
+ if (isOutputSet() || isIntegerToleranceSet()) {
+ STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::glpk, "glpk is not selected as the used LP solver, so setting options for glpk has no effect.");
+ }
+
+ return true;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h
index c23b2add0..b58e91746 100644
--- a/src/settings/modules/GlpkSettings.h
+++ b/src/settings/modules/GlpkSettings.h
@@ -26,6 +26,13 @@ namespace storm {
*/
bool isOutputSet() const;
+ /*!
+ * Retrieves whether the integer tolerance has been set.
+ *
+ * @return True iff the integer tolerance has been set.
+ */
+ bool isIntegerToleranceSet() const;
+
/*!
* Retrieves the integer tolerance to be used.
*
@@ -33,6 +40,8 @@ namespace storm {
*/
double getIntegerTolerance() const;
+ bool check() const override;
+
// The name of the module.
static const std::string moduleName;
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index c9c8b1840..4b9f27f9e 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -32,6 +32,10 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
+ bool GmmxxEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
+ return this->getOption(techniqueOptionName).getHasOptionBeenSet();
+ }
+
GmmxxEquationSolverSettings::LinearEquationTechnique GmmxxEquationSolverSettings::getLinearEquationSystemTechnique() const {
std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (linearEquationSystemTechniqueAsString == "bicgstab") {
@@ -46,6 +50,10 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
+ bool GmmxxEquationSolverSettings::isPreconditioningTechniqueSet() const {
+ return this->getOption(preconditionOptionName).getHasOptionBeenSet();
+ }
+
GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
std::string preconditioningTechniqueAsString = this->getOption(preconditionOptionName).getArgumentByName("name").getValueAsString();
if (preconditioningTechniqueAsString == "ilu") {
@@ -58,22 +66,46 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
}
+ bool GmmxxEquationSolverSettings::isRestartIterationCountSet() const {
+ return this->getOption(restartOptionName).getHasOptionBeenSet();
+ }
+
uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
return this->getOption(restartOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
+ bool GmmxxEquationSolverSettings::isMaximalIterationCountSet() const {
+ return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+ }
+
uint_fast64_t GmmxxEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
+ bool GmmxxEquationSolverSettings::isPrecisionSet() const {
+ return this->getOption(precisionOptionName).getHasOptionBeenSet();
+ }
+
double GmmxxEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
+ bool GmmxxEquationSolverSettings::isConvergenceCriterionSet() const {
+ return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+ }
+
GmmxxEquationSolverSettings::ConvergenceCriterion GmmxxEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GmmxxEquationSolverSettings::ConvergenceCriterion::Absolute : GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
}
+ bool GmmxxEquationSolverSettings::check() const {
+ bool optionsSet = isLinearEquationSystemTechniqueSet() || isPreconditioningTechniqueSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
+
+ STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
+
+ return true;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.h b/src/settings/modules/GmmxxEquationSolverSettings.h
index 7504f7456..07bc90174 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.h
+++ b/src/settings/modules/GmmxxEquationSolverSettings.h
@@ -28,6 +28,13 @@ namespace storm {
*/
GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
+ /*!
+ * Retrieves whether the linear equation system technique has been set.
+ *
+ * @return True iff the linear equation system technique has been set.
+ */
+ bool isLinearEquationSystemTechniqueSet() const;
+
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
*
@@ -35,6 +42,13 @@ namespace storm {
*/
LinearEquationTechnique getLinearEquationSystemTechnique() const;
+ /*!
+ * Retrieves whether the preconditioning technique has been set.
+ *
+ * @return True iff the preconditioning technique has been set.
+ */
+ bool isPreconditioningTechniqueSet() const;
+
/*!
* Retrieves the technique that is to be used for preconditioning solving systems of linear equations.
*
@@ -42,6 +56,13 @@ namespace storm {
*/
PreconditioningTechnique getPreconditioningTechnique() const;
+ /*!
+ * Retrieves whether the restart iteration count has been set.
+ *
+ * @return True iff the restart iteration count has been set.
+ */
+ bool isRestartIterationCountSet() const;
+
/*!
* Retrieves the number of iterations after which restarted techniques are to be restarted.
*
@@ -49,6 +70,13 @@ namespace storm {
*/
uint_fast64_t getRestartIterationCount() const;
+ /*!
+ * Retrieves whether the maximal iteration count has been set.
+ *
+ * @return True iff the maximal iteration count has been set.
+ */
+ bool isMaximalIterationCountSet() const;
+
/*!
* Retrieves the maximal number of iterations to perform until giving up on converging.
*
@@ -56,6 +84,13 @@ namespace storm {
*/
uint_fast64_t getMaximalIterationCount() const;
+ /*!
+ * Retrieves whether the precision has been set.
+ *
+ * @return True iff the precision has been set.
+ */
+ bool isPrecisionSet() const;
+
/*!
* Retrieves the precision that is used for detecting convergence.
*
@@ -63,6 +98,13 @@ namespace storm {
*/
double getPrecision() const;
+ /*!
+ * Retrieves whether the convergence criterion has been set.
+ *
+ * @return True iff the convergence criterion has been set.
+ */
+ bool isConvergenceCriterionSet() const;
+
/*!
* Retrieves the selected convergence criterion.
*
@@ -70,6 +112,8 @@ namespace storm {
*/
ConvergenceCriterion getConvergenceCriterion() const;
+ bool check() const override;
+
// The name of the module.
static const std::string moduleName;
diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp
index 1038fce26..86751cc1d 100644
--- a/src/settings/modules/GurobiSettings.cpp
+++ b/src/settings/modules/GurobiSettings.cpp
@@ -19,10 +19,18 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
}
+ bool GurobiSettings::isIntegerToleranceSet() const {
+ return this->getOption(integerToleranceOption).getHasOptionBeenSet();
+ }
+
double GurobiSettings::getIntegerTolerance() const {
return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
+ bool GurobiSettings::isNumberOfThreadsSet() const {
+ return this->getOption(threadsOption).getHasOptionBeenSet();
+ }
+
uint_fast64_t GurobiSettings::getNumberOfThreads() const {
return this->getOption(threadsOption).getArgumentByName("count").getValueAsUnsignedInteger();
}
@@ -31,6 +39,14 @@ namespace storm {
return this->getOption(outputOption).getHasOptionBeenSet();
}
+ bool GurobiSettings::check() const {
+ if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) {
+ STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::Gurobi, "Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect.");
+ }
+
+ return true;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GurobiSettings.h b/src/settings/modules/GurobiSettings.h
index d0e92127b..ce7fcd78f 100644
--- a/src/settings/modules/GurobiSettings.h
+++ b/src/settings/modules/GurobiSettings.h
@@ -19,6 +19,13 @@ namespace storm {
*/
GurobiSettings(storm::settings::SettingsManager& settingsManager);
+ /*!
+ * Retrieves whether the integer tolerance has been set.
+ *
+ * @return True iff the integer tolerance has been set.
+ */
+ bool isIntegerToleranceSet() const;
+
/*!
* Retrieves the integer tolerance to be used.
*
@@ -26,6 +33,13 @@ namespace storm {
*/
double getIntegerTolerance() const;
+ /*!
+ * Retrieves whether the number of threads has been set.
+ *
+ * @return True iff the number of threads has been set.
+ */
+ bool isNumberOfThreadsSet() const;
+
/*!
* Retrieves the maximal number of threads Gurobi is allowed to use.
*
@@ -40,6 +54,8 @@ namespace storm {
*/
bool isOutputSet() const;
+ bool check() const override;
+
// The name of the module.
static const std::string moduleName;
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index b03feece6..76af99b3e 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -24,6 +24,10 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
+ bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
+ return this->getOption(techniqueOptionName).getHasOptionBeenSet();
+ }
+
NativeEquationSolverSettings::LinearEquationTechnique NativeEquationSolverSettings::getLinearEquationSystemTechnique() const {
std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (linearEquationSystemTechniqueAsString == "jacobi") {
@@ -32,18 +36,38 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
+ bool NativeEquationSolverSettings::isMaximalIterationCountSet() const {
+ return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+ }
+
uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
+ bool NativeEquationSolverSettings::isPrecisionSet() const {
+ return this->getOption(precisionOptionName).getHasOptionBeenSet();
+ }
+
double NativeEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
+ bool NativeEquationSolverSettings::isConvergenceCriterionSet() const {
+ return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+ }
+
NativeEquationSolverSettings::ConvergenceCriterion NativeEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative;
}
+ bool NativeEquationSolverSettings::check() const {
+ bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
+
+ STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Native || !optionSet, "Native is not selected as the equation solver, so setting options for native has no effect.");
+
+ return true;
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h
index 826d40941..9d6e43ecd 100644
--- a/src/settings/modules/NativeEquationSolverSettings.h
+++ b/src/settings/modules/NativeEquationSolverSettings.h
@@ -25,6 +25,13 @@ namespace storm {
*/
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
+ /*!
+ * Retrieves whether the linear equation system technique has been set.
+ *
+ * @return True iff the linear equation system technique has been set.
+ */
+ bool isLinearEquationSystemTechniqueSet() const;
+
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
*
@@ -32,6 +39,13 @@ namespace storm {
*/
LinearEquationTechnique getLinearEquationSystemTechnique() const;
+ /*!
+ * Retrieves whether the maximal iteration count has been set.
+ *
+ * @return True iff the maximal iteration count has been set.
+ */
+ bool isMaximalIterationCountSet() const;
+
/*!
* Retrieves the maximal number of iterations to perform until giving up on converging.
*
@@ -39,6 +53,13 @@ namespace storm {
*/
uint_fast64_t getMaximalIterationCount() const;
+ /*!
+ * Retrieves whether the precision has been set.
+ *
+ * @return True iff the precision has been set.
+ */
+ bool isPrecisionSet() const;
+
/*!
* Retrieves the precision that is used for detecting convergence.
*
@@ -46,6 +67,13 @@ namespace storm {
*/
double getPrecision() const;
+ /*!
+ * Retrieves whether the convergence criterion has been set.
+ *
+ * @return True iff the convergence criterion has been set.
+ */
+ bool isConvergenceCriterionSet() const;
+
/*!
* Retrieves the selected convergence criterion.
*
@@ -53,6 +81,8 @@ namespace storm {
*/
ConvergenceCriterion getConvergenceCriterion() const;
+ bool check() const override;
+
// The name of the module.
static const std::string moduleName;
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 162d2a393..2be0bd112 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -200,9 +200,8 @@ namespace storm {
try {
manager.setFromCommandLine(argc, argv);
} catch (storm::exceptions::OptionParserException& e) {
- std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
- std::cout << std::endl;
manager.printHelp();
+ throw e;
return false;
}
@@ -260,7 +259,7 @@ namespace storm {
}
void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
- if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) {
+ if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
diff --git a/src/utility/macros.h b/src/utility/macros.h
index 511fdcc12..a8d75d3c8 100644
--- a/src/utility/macros.h
+++ b/src/utility/macros.h
@@ -44,14 +44,49 @@ extern log4cplus::Logger logger;
LOG4CPLUS_WARN(logger, message); \
} while (false)
+#define STORM_LOG_WARN_COND(cond, message) \
+{ \
+ if (!(cond)) { \
+ LOG4CPLUS_WARN(logger, message); \
+ } \
+} while (false)
+
#define STORM_LOG_INFO(message) \
{ \
LOG4CPLUS_INFO(logger, message); \
} while (false)
+#define STORM_LOG_INFO_COND(cond, message) \
+{ \
+ if (!(cond)) { \
+ LOG4CPLUS_INFO(logger, message); \
+ } \
+} while (false)
+
#define STORM_LOG_ERROR(message) \
{ \
LOG4CPLUS_ERROR(logger, message); \
} while (false)
+#define STORM_LOG_ERROR_COND(cond, message) \
+{ \
+ if (!(cond)) { \
+ LOG4CPLUS_ERROR(logger, message); \
+ } \
+} while (false)
+
+/*!
+ * Define the macros that print information and optionally also log it.
+ */
+#define STORM_PRINT(message) \
+{ \
+ std::cout << message; \
+}
+
+#define STORM_PRINT_AND_LOG(message) \
+{ \
+ STORM_LOG_INFO(message); \
+ STORM_PRINT(message); \
+}
+
#endif /* STORM_UTILITY_MACROS_H_ */
\ No newline at end of file