Browse Source

Added functions responsible for printing the help. Started adapting the tests to the new option system.

Former-commit-id: 0407d8223e
tempestpy_adaptions
dehnert 10 years ago
parent
commit
266d660d89
  1. 2
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  2. 4
      src/settings/Argument.h
  3. 76
      src/settings/ArgumentBase.cpp
  4. 48
      src/settings/ArgumentBase.h
  5. 17
      src/settings/ArgumentType.cpp
  6. 12
      src/settings/ArgumentType.h
  7. 37
      src/settings/ArgumentTypeInferationHelper.cpp
  8. 87
      src/settings/Option.cpp
  9. 21
      src/settings/Option.h
  10. 6
      src/settings/OptionBuilder.h
  11. 152
      src/settings/SettingsManager.cpp
  12. 94
      src/settings/SettingsManager.h
  13. 8
      src/settings/modules/CuddSettings.cpp
  14. 2
      src/settings/modules/DebugSettings.cpp
  15. 7
      src/settings/modules/GeneralSettings.cpp
  16. 10
      src/settings/modules/GeneralSettings.h
  17. 12
      src/settings/modules/GlpkSettings.cpp
  18. 56
      src/settings/modules/GmmxxEquationSolverSettings.cpp
  19. 18
      src/settings/modules/GurobiSettings.cpp
  20. 55
      src/settings/modules/ModuleSettings.cpp
  21. 16
      src/settings/modules/ModuleSettings.h
  22. 28
      src/settings/modules/NativeEquationSolverSettings.cpp
  23. 5
      src/settings/modules/NativeEquationSolverSettings.h
  24. 2
      src/storm.cpp
  25. 4
      src/utility/CLI.h
  26. 18
      test/functional/modelchecker/ActionTest.cpp
  27. 4
      test/functional/modelchecker/FilterTest.cpp
  28. 40
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  29. 38
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  30. 6
      test/functional/parser/DeterministicSparseTransitionParserTest.cpp
  31. 6
      test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp
  32. 6
      test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
  33. 24
      test/functional/solver/GlpkLpSolverTest.cpp
  34. 68
      test/functional/solver/GmmxxLinearEquationSolverTest.cpp
  35. 14
      test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
  36. 8
      test/functional/solver/NativeLinearEquationSolverTest.cpp
  37. 14
      test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
  38. 26
      test/functional/storm-functional-tests.cpp

2
src/counterexamples/MILPMinimalLabelSetGenerator.h

@ -1025,7 +1025,7 @@ namespace storm {
// Delegate the actual computation work to the function of equal name.
auto startTime = std::chrono::high_resolution_clock::now();
boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().useSchedulerCuts());
boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet());
auto endTime = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;

4
src/settings/Argument.h

@ -95,8 +95,8 @@ namespace storm {
template <typename S>
bool isCompatibleWith(Argument<S> const& other) const {
LOG_THROW(this->getType() == other.getType(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because they have different types.");
LOG_THROW(this->getIsOptional() != other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them is optional and the other one is not.");
LOG_THROW(this->getHasDefaultValue() != other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not.");
LOG_THROW(this->getIsOptional() == other.getIsOptional(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments '" << this->getName() << "' and '" << other.getName() << "', because one of them is optional and the other one is not.");
LOG_THROW(this->getHasDefaultValue() == other.getHasDefaultValue(), storm::exceptions::ArgumentUnificationException, "Unable to unify the arguments " << this->getName() << " and " << other.getName() << ", because one of them has a default value and the other one does not.");
return true;
}

76
src/settings/ArgumentBase.cpp

@ -0,0 +1,76 @@
#include "src/settings/ArgumentBase.h"
#include <iomanip>
namespace storm {
namespace settings {
uint_fast64_t ArgumentBase::getPrintLength() const {
return this->getName().length() + 2;
}
std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument) {
std::streamsize width = out.width();
uint_fast64_t charactersPrinted = 0;
out << std::setw(0) << std::left << "<" << argument.getName() << "> ";
charactersPrinted += 2 + argument.getName().length();
for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
out << out.fill();
}
out << "\t" << argument.getDescription();
return out;
}
template <typename TargetType>
TargetType ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful) {
std::istringstream stream(valueAsString);
TargetType t;
conversionSuccessful = (stream >> t) && (stream >> std::ws).eof();
return t;
}
template <>
bool ArgumentBase::convertFromString<bool>(std::string const& s, bool& ok) {
static const std::string lowerTrueString = "true";
static const std::string lowerFalseString = "false";
static const std::string lowerYesString = "yes";
static const std::string lowerNoString = "no";
std::string lowerInput = boost::algorithm::to_lower_copy(s);
if (s.compare(lowerTrueString) == 0 || s.compare(lowerYesString) == 0) {
ok = true;
return true;
} else if (s.compare(lowerFalseString) == 0 || s.compare(lowerNoString) == 0) {
ok = true;
return false;
}
std::istringstream stream(s);
bool t;
ok = (stream >> t) && (stream >> std::ws).eof();
return t;
}
template <typename ValueType>
std::string ArgumentBase::convertToString(ValueType const& value) {
std::ostringstream stream;
stream << value;
return stream.str();
}
// Explicitly instantiate the templates.
template std::string ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template int_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template uint_fast64_t ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template double ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template bool ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful);
template std::string ArgumentBase::convertToString(std::string const& value);
template std::string ArgumentBase::convertToString(int_fast64_t const& value);
template std::string ArgumentBase::convertToString(uint_fast64_t const& value);
template std::string ArgumentBase::convertToString(double const& value);
template std::string ArgumentBase::convertToString(bool const& value);
}
}

48
src/settings/ArgumentBase.h

@ -127,6 +127,15 @@ namespace storm {
*/
virtual bool getValueAsBoolean() const = 0;
/*!
* Retrieves the (print) length of the argument.
*
* @return The length of the argument.
*/
uint_fast64_t getPrintLength() const;
friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument);
protected:
// A flag indicating whether the argument has been set.
bool hasBeenSet;
@ -157,45 +166,6 @@ namespace storm {
template <typename ValueType>
static std::string convertToString(ValueType const& value);
};
template <typename TargetType>
TargetType ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful) {
std::istringstream stream(valueAsString);
TargetType t;
conversionSuccessful = (stream >> t) && (stream >> std::ws).eof();
return t;
}
template <>
bool ArgumentBase::convertFromString<bool>(std::string const& s, bool& ok) {
static const std::string lowerTrueString = "true";
static const std::string lowerFalseString = "false";
static const std::string lowerYesString = "yes";
static const std::string lowerNoString = "no";
std::string lowerInput = boost::algorithm::to_lower_copy(s);
if (s.compare(lowerTrueString) == 0 || s.compare(lowerYesString) == 0) {
ok = true;
return true;
} else if (s.compare(lowerFalseString) == 0 || s.compare(lowerNoString) == 0) {
ok = true;
return false;
}
std::istringstream stream(s);
bool t;
ok = (stream >> t) && (stream >> std::ws).eof();
return t;
}
template <typename ValueType>
std::string ArgumentBase::convertToString(ValueType const& value) {
std::ostringstream stream;
stream << value;
return stream.str();
}
}
}

17
src/settings/ArgumentType.cpp

@ -0,0 +1,17 @@
#include "src/settings/ArgumentType.h"
namespace storm {
namespace settings {
std::ostream& operator<<(std::ostream& out, ArgumentType& argumentType) {
switch (argumentType) {
case ArgumentType::String: out << "string"; break;
case ArgumentType::Integer: out << "integer"; break;
case ArgumentType::UnsignedInteger: out << "unsigned integer"; break;
case ArgumentType::Double: out << "double"; break;
case ArgumentType::Boolean: out << "boolean"; break;
}
return out;
}
}
}

12
src/settings/ArgumentType.h

@ -15,17 +15,7 @@ namespace storm {
String, Integer, UnsignedInteger, Double, Boolean
};
std::ostream& operator<<(std::ostream& out, ArgumentType& argumentType) {
switch (argumentType) {
case ArgumentType::String: out << "string"; break;
case ArgumentType::Integer: out << "integer"; break;
case ArgumentType::UnsignedInteger: out << "unsigned integer"; break;
case ArgumentType::Double: out << "double"; break;
case ArgumentType::Boolean: out << "boolean"; break;
}
return out;
}
std::ostream& operator<<(std::ostream& out, ArgumentType& argumentType);
} // namespace settings
} // namespace storm

37
src/settings/ArgumentTypeInferationHelper.cpp

@ -86,5 +86,42 @@ namespace storm {
LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument.");
return value;
}
// Explicitly instantiate the templates.
template ArgumentType ArgumentTypeInferation::inferToEnumType<std::string>();
template ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>();
template ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>();
template ArgumentType ArgumentTypeInferation::inferToEnumType<double>();
template ArgumentType ArgumentTypeInferation::inferToEnumType<bool>();
template std::string const& ArgumentTypeInferation::inferToString<std::string>(ArgumentType const& argumentType, std::string const& value);
template std::string const& ArgumentTypeInferation::inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template std::string const& ArgumentTypeInferation::inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template std::string const& ArgumentTypeInferation::inferToString<double>(ArgumentType const& argumentType, double const& value);
template std::string const& ArgumentTypeInferation::inferToString<bool>(ArgumentType const& argumentType, bool const& value);
template int_fast64_t ArgumentTypeInferation::inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
template int_fast64_t ArgumentTypeInferation::inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template int_fast64_t ArgumentTypeInferation::inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template int_fast64_t ArgumentTypeInferation::inferToInteger<double>(ArgumentType const& argumentType, double const& value);
template int_fast64_t ArgumentTypeInferation::inferToInteger<bool>(ArgumentType const& argumentType, bool const& value);
template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value);
template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value);
template double ArgumentTypeInferation::inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value);
template double ArgumentTypeInferation::inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template double ArgumentTypeInferation::inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template double ArgumentTypeInferation::inferToDouble<double>(ArgumentType const& argumentType, double const& value);
template double ArgumentTypeInferation::inferToDouble<bool>(ArgumentType const& argumentType, bool const& value);
template bool ArgumentTypeInferation::inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value);
template bool ArgumentTypeInferation::inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template bool ArgumentTypeInferation::inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template bool ArgumentTypeInferation::inferToBoolean<double>(ArgumentType const& argumentType, double const& value);
template bool ArgumentTypeInferation::inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value);
}
}

87
src/settings/Option.cpp

@ -0,0 +1,87 @@
#include "src/settings/Option.h"
#include <iomanip>
namespace storm {
namespace settings {
uint_fast64_t Option::getPrintLength() const {
uint_fast64_t length = 2;
if (!this->getRequiresModulePrefix()) {
length += 2;
}
length += this->getModuleName().length() + 1;
length += this->getLongName().length();
if (this->getHasShortName()) {
length += 4;
if (!this->getRequiresModulePrefix()) {
length += 2;
}
length += this->getModuleName().length() + 1;
length += this->getShortName().length();
}
return length;
}
std::vector<std::shared_ptr<ArgumentBase>> const& Option::getArguments() const {
return this->arguments;
}
std::ostream& operator<<(std::ostream& out, Option const& option) {
std::streamsize width = out.width();
uint_fast64_t charactersPrinted = 0;
out << std::setw(0) << "--";
charactersPrinted += 2;
if (!option.getRequiresModulePrefix()) {
out << "[";
++charactersPrinted;
}
out << option.getModuleName() << ":";
charactersPrinted += option.getModuleName().length() + 1;
if (!option.getRequiresModulePrefix()) {
out << "]";
++charactersPrinted;
}
out << option.getLongName();
charactersPrinted += option.getLongName().length();
if (option.getHasShortName()) {
out << " | -";
charactersPrinted += 4;
if (!option.getRequiresModulePrefix()) {
out << "[";
++charactersPrinted;
}
out << option.getModuleName() << ":";
charactersPrinted += option.getModuleName().length() + 1;
if (!option.getRequiresModulePrefix()) {
out << "]";
++charactersPrinted;
}
out << option.getShortName();
charactersPrinted += option.getShortName().length();
}
// Now fill the width.
for (uint_fast64_t i = charactersPrinted; i < width; ++i) {
out << out.fill();
}
out << "\t" << option.getDescription();
if (option.getArgumentCount() > 0) {
// Start by determining the longest print length of the arguments.
uint_fast64_t maxLength = 0;
for (auto const& argument : option.getArguments()) {
maxLength = std::max(maxLength, argument->getPrintLength());
}
for (auto const& argument : option.getArguments()) {
out << std::endl;
out << "\t* " << std::setw(maxLength) << std::left << *argument;
}
}
return out;
}
}
}

21
src/settings/Option.h

@ -74,6 +74,7 @@ namespace storm {
* @return True iff the given argument is compatible with the current one.
*/
bool isCompatibleWith(Option const& other) {
std::cout << "unifying " << *this << " and " << other << std::endl;
LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs.");
for(size_t i = 0; i != this->arguments.size(); i++) {
@ -206,7 +207,7 @@ namespace storm {
* @return True iff the option requires the module name as a prefix.
*/
bool getRequiresModulePrefix() const {
return this->requiresModulePrefix;
return this->requireModulePrefix;
}
/*!
@ -218,6 +219,22 @@ namespace storm {
return this->hasBeenSet;
}
/*!
* Retrieves the arguments of the option.
*
* @return The arguments of the option.
*/
std::vector<std::shared_ptr<ArgumentBase>> const& getArguments() const;
/*!
* Retrieves the (print) length of the option.
*
* @return The length of the option.
*/
uint_fast64_t getPrintLength() const;
friend std::ostream& operator<<(std::ostream& out, Option const& option);
private:
// The long name of the option.
std::string longName;
@ -262,7 +279,7 @@ namespace storm {
* module name.
* @param optionArguments The arguments of the option.
*/
Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(), argumentNameMap() {
Option(std::string const& moduleName, std::string const& longOptionName, std::string const& shortOptionName, bool hasShortOptionName, std::string const& optionDescription, bool isOptionRequired, bool requireModulePrefix, std::vector<std::shared_ptr<ArgumentBase>> const& optionArguments = std::vector<std::shared_ptr<ArgumentBase>>()) : longName(longOptionName), hasShortName(hasShortOptionName), shortName(shortOptionName), description(optionDescription), moduleName(moduleName), isRequired(isOptionRequired), requireModulePrefix(requireModulePrefix), hasBeenSet(false), arguments(optionArguments), argumentNameMap() {
// First, do some sanity checks.
LOG_THROW(!longName.empty(), storm::exceptions::IllegalArgumentException, "Unable to construct option with empty name.");

6
src/settings/OptionBuilder.h

@ -88,7 +88,11 @@ namespace storm {
LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot rebuild an option with one builder.")
this->isBuild = true;
return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->shortName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
if (this->hasShortName) {
return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->shortName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
} else {
return std::shared_ptr<Option>(new Option(this->moduleName, this->longName, this->description, this->isRequired, this->requireModulePrefix, this->arguments));
}
}
private:

152
src/settings/SettingsManager.cpp

@ -3,7 +3,9 @@
#include <cstring>
#include <cctype>
#include <mutex>
#include <iomanip>
#include <boost/algorithm/string.hpp>
#include <boost/io/ios_state.hpp>
#include "src/exceptions/IllegalFunctionCallException.h"
#include "src/exceptions/OptionParserException.h"
@ -44,6 +46,9 @@ namespace storm {
}
void SettingsManager::setFromString(std::string const& commandLineString) {
if (commandLineString.empty()) {
return;
}
std::vector<std::string> argumentVector;
boost::split(argumentVector, commandLineString, boost::is_any_of("\t "));
this->setFromExplodedString(argumentVector);
@ -57,15 +62,21 @@ namespace storm {
std::vector<std::string> argumentCache;
// Walk through all arguments.
std::cout << "before... "<< std::endl;
for (uint_fast64_t i = 0; i < commandLineArguments.size(); ++i) {
std::cout << "in ... " << i << std::endl;
bool existsNextArgument = i < commandLineArguments.size() - 1;
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) == '-') {
// 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.
setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->longNameToOptions : this->shortNameToOptions, argumentCache);
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.
setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
} else {
optionActive = true;
}
if (currentArgument.at(1) == '-') {
// In this case, the argument has to be the long name of an option. Try to get all options that
@ -91,6 +102,11 @@ namespace storm {
LOG_THROW(false, storm::exceptions::OptionParserException, "Found stray argument '" << currentArgument << "' that is not preceeded by a matching option.");
}
}
// If an option is still active at this point, we need to set it.
if (optionActive) {
setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
}
}
void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
@ -98,15 +114,67 @@ namespace storm {
}
void SettingsManager::printHelp(std::string const& moduleName) const {
LOG_ASSERT(false, "Not yet implemented");
std::cout << "usage: storm [options]" << std::endl << std::endl;
if (moduleName == "all") {
// Find longest option name.
uint_fast64_t maxLength = getPrintLengthOfLongestOption();
for (auto const& moduleName : this->moduleNames) {
printHelpForModule(moduleName, maxLength);
}
} else {
uint_fast64_t maxLength = getPrintLengthOfLongestOption(moduleName);
printHelpForModule(moduleName, maxLength);
}
}
void SettingsManager::printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength) const {
auto moduleIterator = moduleOptions.find(moduleName);
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;
// 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;
}
std::cout << std::endl;
}
uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
uint_fast64_t length = 0;
for (auto const& moduleName : this->moduleNames) {
length = std::max(getPrintLengthOfLongestOption(moduleName), length);
}
return length;
}
uint_fast64_t SettingsManager::getPrintLengthOfLongestOption(std::string const& moduleName) const {
auto moduleIterator = modules.find(moduleName);
LOG_THROW(moduleIterator != modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve option length of unknown module '" << moduleName << "'.");
return moduleIterator->second->getPrintLengthOfLongestOption();
}
void SettingsManager::addModule(std::unique_ptr<modules::ModuleSettings>&& moduleSettings) {
auto moduleIterator = this->modules.find(moduleSettings->getModuleName());
LOG_THROW(moduleIterator == this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register module '" << moduleSettings->getModuleName() << "' because a module with the same name already exists.");
// Take over the module settings object.
std::string const& moduleName = moduleSettings->getModuleName();
this->moduleNames.push_back(moduleName);
this->modules.emplace(moduleSettings->getModuleName(), std::move(moduleSettings));
auto iterator = this->modules.find(moduleName);
std::unique_ptr<modules::ModuleSettings> const& settings = iterator->second;
for (auto const& option : moduleSettings->getOptions()) {
// Now register the options of the module.
this->moduleOptions.emplace(moduleName, std::vector<std::shared_ptr<Option>>());
for (auto const& option : settings->getOptions()) {
this->addOption(option);
}
}
@ -123,20 +191,32 @@ namespace storm {
if (!option->getRequiresModulePrefix()) {
bool isCompatible = this->isCompatible(option, option->getLongName(), this->longNameToOptions);
LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
this->longNameToOptions.emplace(option->getLongName(), option);
addOptionToMap(option->getLongName(), option, this->longNameToOptions);
}
// For the prefixed name, we don't need a compatibility check, because a module is not allowed to register the same option twice.
this->longNameToOptions.emplace(option->getModuleName() + ":" + option->getLongName(), option);
addOptionToMap(option->getModuleName() + ":" + option->getLongName(), option, this->longNameToOptions);
if (option->getHasShortName()) {
if (!option->getRequiresModulePrefix()) {
this->shortNameToOptions.emplace(option->getShortName(), option);
bool isCompatible = this->isCompatible(option, option->getShortName(), this->shortNameToOptions);
LOG_THROW(isCompatible, storm::exceptions::IllegalFunctionCallException, "Unable to add option '" << option->getLongName() << "', because an option with the same name is incompatible with it.");
addOptionToMap(option->getShortName(), option, this->shortNameToOptions);
}
this->shortNameToOptions.emplace(option->getModuleName() + ":" + option->getShortName(), option);
addOptionToMap(option->getModuleName() + ":" + option->getShortName(), option, this->shortNameToOptions);
}
}
modules::ModuleSettings const& SettingsManager::getModule(std::string const& moduleName) const {
auto moduleIterator = this->modules.find(moduleName);
LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
return *moduleIterator->second;
}
modules::ModuleSettings& SettingsManager::getModule(std::string const& moduleName) {
auto moduleIterator = this->modules.find(moduleName);
LOG_THROW(moduleIterator != this->modules.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown module '" << moduleName << "'.");
return *moduleIterator->second;
}
bool SettingsManager::isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap) {
auto optionIterator = optionMap.find(optionName);
@ -174,5 +254,59 @@ namespace storm {
}
}
void SettingsManager::addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap) {
auto optionIterator = optionMap.find(name);
if (optionIterator == optionMap.end()) {
std::vector<std::shared_ptr<Option>> optionVector;
optionVector.push_back(option);
optionMap.emplace(name, optionVector);
} else {
optionIterator->second.push_back(option);
}
}
SettingsManager const& manager() {
return SettingsManager::manager();
}
SettingsManager& mutableManager() {
return SettingsManager::manager();
}
storm::settings::modules::GeneralSettings const& generalSettings() {
return dynamic_cast<storm::settings::modules::GeneralSettings const&>(manager().getModule(storm::settings::modules::GeneralSettings::moduleName));
}
storm::settings::modules::GeneralSettings& mutableGeneralSettings() {
return dynamic_cast<storm::settings::modules::GeneralSettings&>(storm::settings::SettingsManager::manager().getModule(storm::settings::modules::GeneralSettings::moduleName));
}
storm::settings::modules::DebugSettings const& debugSettings() {
return dynamic_cast<storm::settings::modules::DebugSettings const&>(manager().getModule(storm::settings::modules::DebugSettings::moduleName));
}
storm::settings::modules::CounterexampleGeneratorSettings const& counterexampleGeneratorSettings() {
return dynamic_cast<storm::settings::modules::CounterexampleGeneratorSettings const&>(manager().getModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName));
}
storm::settings::modules::CuddSettings const& cuddSettings() {
return dynamic_cast<storm::settings::modules::CuddSettings const&>(manager().getModule(storm::settings::modules::CuddSettings::moduleName));
}
storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings() {
return dynamic_cast<storm::settings::modules::GmmxxEquationSolverSettings const&>(manager().getModule(storm::settings::modules::GmmxxEquationSolverSettings::moduleName));
}
storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings() {
return dynamic_cast<storm::settings::modules::NativeEquationSolverSettings const&>(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName));
}
storm::settings::modules::GlpkSettings const& glpkSettings() {
return dynamic_cast<storm::settings::modules::GlpkSettings const&>(manager().getModule(storm::settings::modules::GlpkSettings::moduleName));
}
storm::settings::modules::GurobiSettings const& gurobiSettings() {
return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
}
}
}

94
src/settings/SettingsManager.h

@ -79,11 +79,19 @@ namespace storm {
* it is present, name must correspond to a known module. Then, only the help text for this module is
* printed.
*
* @return moduleName The name of the module for which to show the help or "all" if the full help text is to
* @param moduleName The name of the module for which to show the help or "all" if the full help text is to
* be printed.
*/
void printHelp(std::string const& moduleName = "all") const;
/*!
* This function prints a help message for the specified module to the standard output.
*
* @param moduleName The name of the module for which to show the help.
* @param maxLength The maximal length of an option name (necessary for proper alignment).
*/
void printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength = 30) const;
/*!
* Retrieves the only existing instance of a settings manager.
*
@ -106,6 +114,14 @@ namespace storm {
* @return An object that provides access to the settings of the module.
*/
modules::ModuleSettings const& getModule(std::string const& moduleName) const;
/*!
* Retrieves the settings of the module with the given name.
*
* @param moduleName The name of the module for which to retrieve the settings.
* @return An object that provides access to the settings of the module.
*/
modules::ModuleSettings& getModule(std::string const& moduleName);
private:
/*!
@ -120,6 +136,7 @@ namespace storm {
virtual ~SettingsManager();
// The registered modules.
std::vector<std::string> moduleNames;
std::unordered_map<std::string, std::unique_ptr<modules::ModuleSettings>> modules;
// Mappings from all known option names to the options that match it. All options for one option name need
@ -150,6 +167,30 @@ namespace storm {
* Checks whether the given option is compatible with all options with the given name in the given mapping.
*/
static bool isCompatible(std::shared_ptr<Option> const& option, std::string const& optionName, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>> const& optionMap);
/*!
* Inserts the given option to the options with the given name in the given map.
*
* @param name The name of the option.
* @param option The option to add.
* @param optionMap The map into which the option is to be inserted.
*/
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);
/*!
* Retrieves the (print) length of the longest option of all modules.
*
* @return The length of the longest option.
*/
uint_fast64_t getPrintLengthOfLongestOption() const;
/*!
* Retrieves the (print) length of the longest option in the given module, so we can align the options.
*
* @param moduleName The module name for which to retrieve the length of the longest option.
* @return The length of the longest option name.
*/
uint_fast64_t getPrintLengthOfLongestOption(std::string const& moduleName) const;
};
/*!
@ -157,81 +198,78 @@ namespace storm {
*
* @return The only settings manager.
*/
SettingsManager& manager() {
return SettingsManager::manager();
}
SettingsManager const& manager();
/*!
* Retrieves the settings manager.
*
* @return The only settings manager.
*/
SettingsManager& mutableManager();
/*!
* Retrieves the general settings.
*
* @return An object that allows accessing the general settings.
*/
storm::settings::modules::GeneralSettings const& generalSettings() {
return dynamic_cast<storm::settings::modules::GeneralSettings const&>(manager().getModule(storm::settings::modules::GeneralSettings::moduleName));
}
storm::settings::modules::GeneralSettings const& generalSettings();
/*!
* Retrieves the general settings in a mutable form. This is only meant to be used for debug purposes or very
* rare cases where it is necessary.
*
* @return An object that allows accessing and modifying the general settings.
*/
storm::settings::modules::GeneralSettings& mutableGeneralSettings();
/*!
* Retrieves the debug settings.
*
* @return An object that allows accessing the debug settings.
*/
storm::settings::modules::DebugSettings const& debugSettings() {
return dynamic_cast<storm::settings::modules::DebugSettings const&>(manager().getModule(storm::settings::modules::DebugSettings::moduleName));
}
storm::settings::modules::DebugSettings const& debugSettings();
/*!
* Retrieves the counterexample generator settings.
*
* @return An object that allows accessing the counterexample generator settings.
*/
storm::settings::modules::CounterexampleGeneratorSettings const& counterexampleGeneratorSettings() {
return dynamic_cast<storm::settings::modules::CounterexampleGeneratorSettings const&>(manager().getModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName));
}
storm::settings::modules::CounterexampleGeneratorSettings const& counterexampleGeneratorSettings();
/*!
* Retrieves the CUDD settings.
*
* @return An object that allows accessing the CUDD settings.
*/
storm::settings::modules::CuddSettings const& cuddSettings() {
return dynamic_cast<storm::settings::modules::CuddSettings const&>(manager().getModule(storm::settings::modules::CuddSettings::moduleName));
}
storm::settings::modules::CuddSettings const& cuddSettings();
/*!
* Retrieves the settings of the gmm++-based equation solver.
*
* @return An object that allows accessing the settings of the gmm++-based equation solver.
*/
storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings() {
return dynamic_cast<storm::settings::modules::GmmxxEquationSolverSettings const&>(manager().getModule(storm::settings::modules::GmmxxEquationSolverSettings::moduleName));
}
storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings();
/*!
* Retrieves the settings of the native equation solver.
*
* @return An object that allows accessing the settings of the native equation solver.
*/
storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings() {
return dynamic_cast<storm::settings::modules::NativeEquationSolverSettings const&>(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName));
}
storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings();
/*!
* Retrieves the settings of glpk.
*
* @return An object that allows accessing the settings of glpk.
*/
storm::settings::modules::GlpkSettings const& glpkSettings() {
return dynamic_cast<storm::settings::modules::GlpkSettings const&>(manager().getModule(storm::settings::modules::GlpkSettings::moduleName));
}
storm::settings::modules::GlpkSettings const& glpkSettings();
/*!
* Retrieves the settings of Gurobi.
*
* @return An object that allows accessing the settings of Gurobi.
*/
storm::settings::modules::GurobiSettings const& gurobiSettings() {
return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
}
storm::settings::modules::GurobiSettings const& gurobiSettings();
} // namespace settings
} // namespace storm

8
src/settings/modules/CuddSettings.cpp

@ -6,10 +6,10 @@ namespace storm {
namespace settings {
namespace modules {
const std::string moduleName = "cudd";
const std::string precisionOptionName = "precision";
const std::string maximalMemoryOptionName = "maxmem";
const std::string reorderOptionName = "reorder";
const std::string CuddSettings::moduleName = "cudd";
const std::string CuddSettings::precisionOptionName = "precision";
const std::string CuddSettings::maximalMemoryOptionName = "maxmem";
const std::string CuddSettings::reorderOptionName = "reorder";
CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());

2
src/settings/modules/DebugSettings.cpp

@ -16,7 +16,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Print debug output.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Print even more debug output.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, logfileOptionName, false, "If specified, the log output will also be written to this file.").setShortName(logfileOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to write the log.").build()).build());
}
bool DebugSettings::isDebugSet() const {

7
src/settings/modules/GeneralSettings.cpp

@ -1,6 +1,7 @@
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
namespace storm {
namespace settings {
@ -183,6 +184,10 @@ namespace storm {
return this->getOption(fixDeadlockOptionName).getHasOptionBeenSet();
}
std::unique_ptr<storm::settings::SettingMemento> GeneralSettings::overrideFixDeadlocksSet(bool stateToSet) {
return this->overrideOption(fixDeadlockOptionName, stateToSet);
}
bool GeneralSettings::isTimeoutSet() const {
return this->getOption(timeoutOptionName).getHasOptionBeenSet();
}
@ -208,7 +213,7 @@ namespace storm {
} else if (lpSolverName == "glpk") {
return GeneralSettings::LpSolver::glpk;
}
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << equationSolverName << "'.");
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'.");
}
bool GeneralSettings::isConstantsSet() const {

10
src/settings/modules/GeneralSettings.h

@ -214,6 +214,15 @@ namespace storm {
*/
bool isFixDeadlocksSet() const;
/*!
* Overrides the option to fix deadlocks by setting it to the specified value. As soon as the returned
* memento goes out of scope, the original value is restored.
*
* @param stateToSet The value that is to be set for the fix-deadlocks option.
* @return The memento that will eventually restore the original value.
*/
std::unique_ptr<storm::settings::SettingMemento> overrideFixDeadlocksSet(bool stateToSet);
/*!
* Retrieves whether the timeout option was set.
*
@ -288,7 +297,6 @@ namespace storm {
static const std::string lpSolverOptionName;
static const std::string constantsOptionName;
static const std::string constantsOptionShortName;
};
} // namespace modules

12
src/settings/modules/GlpkSettings.cpp

@ -11,8 +11,16 @@ namespace storm {
const std::string GlpkSettings::outputOptionName = "output";
GlpkSettings::GlpkSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk'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());
this->addOption(storm::settings::OptionBuilder(moduleName, outputOptionName, true, "If set, the glpk output will be printed to the command line.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets glpk'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 GlpkSettings::isOutputSet() const {
return this->getOption(outputOptionName).getHasOptionBeenSet();
}
double GlpkSettings::getIntegerTolerance() const {
return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
} // namespace modules

56
src/settings/modules/GmmxxEquationSolverSettings.cpp

@ -17,19 +17,61 @@ namespace storm {
GmmxxEquationSolverSettings::GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> methods = {"bicgstab", "qmr", "gmres", "jacobi"};
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the gmm++ engine. Available are {bicgstab, qmr, gmres, jacobi}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("gmres").build()).build());
// Register available preconditioners.
std::vector<std::string> preconditioner = {"ilu", "diagonal", "ildlt", "none"};
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
std::vector<std::string> preconditioner = {"ilu", "diagonal", "none"};
this->addOption(storm::settings::OptionBuilder(moduleName, preconditionOptionName, true, "The preconditioning technique used for solving linear equation systems. Available are {ilu, diagonal, none}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the preconditioning method.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(preconditioner)).setDefaultValueString("ilu").build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("iterations", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
GmmxxEquationSolverSettings::LinearEquationTechnique GmmxxEquationSolverSettings::getLinearEquationSystemTechnique() const {
std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (linearEquationSystemTechniqueAsString == "bicgstab") {
return GmmxxEquationSolverSettings::LinearEquationTechnique::Bicgstab;
} else if (linearEquationSystemTechniqueAsString == "qmr") {
return GmmxxEquationSolverSettings::LinearEquationTechnique::Qmr;
} else if (linearEquationSystemTechniqueAsString == "gmres") {
return GmmxxEquationSolverSettings::LinearEquationTechnique::Gmres;
} else if (linearEquationSystemTechniqueAsString == "jacobi") {
return GmmxxEquationSolverSettings::LinearEquationTechnique::Jacobi;
}
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
std::string preconditioningTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (preconditioningTechniqueAsString == "ilu") {
return GmmxxEquationSolverSettings::PreconditioningTechnique::Ilu;
} else if (preconditioningTechniqueAsString == "diagonal") {
return GmmxxEquationSolverSettings::PreconditioningTechnique::Diagonal;
} else if (preconditioningTechniqueAsString == "none") {
return GmmxxEquationSolverSettings::PreconditioningTechnique::None;
}
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
}
uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
return this->getOption(restartOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
uint_fast64_t GmmxxEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
double GmmxxEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
GmmxxEquationSolverSettings::ConvergenceCriterion GmmxxEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GmmxxEquationSolverSettings::ConvergenceCriterion::Absolute : GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
}
} // namespace modules

18
src/settings/modules/GurobiSettings.cpp

@ -12,11 +12,23 @@ namespace storm {
const std::string GurobiSettings::outputOption = "output";
GurobiSettings::GurobiSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, threadsOption, true, "The number of threads that may be used by Gurobi.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of threads.").setDefaultValueUnsignedInteger(1).build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, outputOption, true, "If set, the Gurobi output will be printed to the command line.").build());
this->addAndRegisterOption(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());
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());
}
double GurobiSettings::getIntegerTolerance() const {
return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
uint_fast64_t GurobiSettings::getNumberOfThreads() const {
return this->getOption(threadsOption).getArgumentByName("count").getValueAsUnsignedInteger();
}
bool GurobiSettings::isOutputSet() const {
return this->getOption(outputOption).getHasOptionBeenSet();
}
} // namespace modules

55
src/settings/modules/ModuleSettings.cpp

@ -1,5 +1,8 @@
#include "src/settings/modules/ModuleSettings.h"
#include "src/settings/SettingMemento.h"
#include "src/exceptions/InvalidStateException.h"
namespace storm {
namespace settings {
namespace modules {
@ -24,29 +27,55 @@ namespace storm {
return this->getOption(name).setHasOptionBeenSet(false);
}
std::vector<std::shared_ptr<Option>> ModuleSettings::getOptions() const {
std::vector<std::shared_ptr<Option>> result;
result.reserve(this->options.size());
for (auto const& option : this->options) {
result.push_back(option.second);
}
return result;
std::vector<std::shared_ptr<Option>> const& ModuleSettings::getOptions() const {
return this->options;
}
Option const& ModuleSettings::getOption(std::string const& longName) const {
auto optionIterator = this->options.find(longName);
LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
auto optionIterator = this->optionMap.find(longName);
LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
return *optionIterator->second;
}
Option& ModuleSettings::getOption(std::string const& longName) {
auto optionIterator = this->options.find(longName);
LOG_THROW(optionIterator != this->options.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
auto optionIterator = this->optionMap.find(longName);
LOG_THROW(optionIterator != this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Cannot retrieve unknown option '" << longName << "'.");
return *optionIterator->second;
}
std::string const& ModuleSettings::getModuleName() const {
return this->moduleName;
}
std::unique_ptr<storm::settings::SettingMemento> ModuleSettings::overrideOption(std::string const& name, bool requiredStatus) {
bool currentStatus = this->isSet(name);
if (currentStatus) {
this->unset(name);
} else {
this->set(name);
}
return std::unique_ptr<storm::settings::SettingMemento>(new storm::settings::SettingMemento(*this, name, currentStatus));
}
bool ModuleSettings::isSet(std::string const& optionName) const {
return this->getOption(optionName).getHasOptionBeenSet();
}
void ModuleSettings::addOption(std::shared_ptr<Option> const& option) {
auto optionIterator = this->optionMap.find(option->getLongName());
LOG_THROW(optionIterator == this->optionMap.end(), storm::exceptions::IllegalFunctionCallException, "Unable to register the option '" << option->getLongName() << "' in module '" << this->getModuleName() << "', because an option with this name already exists.");
this->optionMap.emplace(option->getLongName(), option);
this->options.push_back(option);
}
uint_fast64_t ModuleSettings::getPrintLengthOfLongestOption() const {
uint_fast64_t length = 0;
for (auto const& option : this->options) {
length = std::max(length, option->getPrintLength());
}
return length;
}
} // namespace modules
} // namespace settings
} // namespace storm

16
src/settings/modules/ModuleSettings.h

@ -60,7 +60,14 @@ namespace storm {
*
* @return A list of options of this module.
*/
std::vector<std::shared_ptr<Option>> getOptions() const;
std::vector<std::shared_ptr<Option>> const& getOptions() const;
/*!
* Retrieves the (print) length of the longest option.
*
* @return The length of the longest option.
*/
uint_fast64_t getPrintLengthOfLongestOption() const;
protected:
/*!
@ -115,7 +122,7 @@ namespace storm {
*
* @param option The option to add and register.
*/
void addOption(std::shared_ptr<Option> option) const;
void addOption(std::shared_ptr<Option> const& option);
private:
// The settings manager responsible for the settings.
@ -125,7 +132,10 @@ namespace storm {
std::string moduleName;
// A mapping of option names of the module to the actual options.
std::unordered_map<std::string, std::shared_ptr<Option>> options;
std::unordered_map<std::string, std::shared_ptr<Option>> optionMap;
// The list of known option names in the order they were registered.
std::vector<std::shared_ptr<Option>> options;
};
} // namespace modules

28
src/settings/modules/NativeEquationSolverSettings.cpp

@ -15,13 +15,33 @@ namespace storm {
NativeEquationSolverSettings::NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> methods = { "jacobi" };
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addAndRegisterOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, true, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
NativeEquationSolverSettings::LinearEquationTechnique NativeEquationSolverSettings::getLinearEquationSystemTechnique() const {
std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (linearEquationSystemTechniqueAsString == "jacobi") {
return NativeEquationSolverSettings::LinearEquationTechnique::Jacobi;
}
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
double NativeEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
NativeEquationSolverSettings::ConvergenceCriterion NativeEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative;
}
} // namespace modules

5
src/settings/modules/NativeEquationSolverSettings.h

@ -18,6 +18,11 @@ namespace storm {
// An enumeration of all available convergence criteria.
enum class ConvergenceCriterion { Absolute, Relative };
/*!
* Creates a new set of native equation solver settings that is managed by the given manager.
*
* @param settingsManager The responsible manager.
*/
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!

2
src/storm.cpp

@ -245,7 +245,7 @@ int main(const int argc, const char* argv[]) {
std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
// Determine whether we are required to use the MILP-version or the SAT-version.
bool useMILP = storm::settings::counterexampleGeneratorSettings().useMilpBasedMinimalCommandSetGeneration();
bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
// MinCMD Time Measurement, Start
std::chrono::high_resolution_clock::time_point minCmdStart = std::chrono::high_resolution_clock::now();

4
src/utility/CLI.h

@ -127,7 +127,7 @@ void printHeader(const int argc, const char* argv[]) {
* @return True iff the program should continue to run after parsing the options.
*/
bool parseOptions(const int argc, const char* argv[]) {
storm::settings::SettingsManager& manager = storm::settings::manager();
storm::settings::SettingsManager& manager = storm::settings::mutableManager();
try {
manager.setFromCommandLine(argc, argv);
} catch (storm::exceptions::OptionParserException& e) {
@ -138,7 +138,7 @@ bool parseOptions(const int argc, const char* argv[]) {
}
if (storm::settings::generalSettings().isHelpSet()) {
storm::settings::manager().printHelp();
storm::settings::manager().printHelp(storm::settings::generalSettings().getHelpModuleName());
return false;
}

18
test/functional/modelchecker/ActionTest.cpp

@ -27,7 +27,7 @@ TEST(ActionTest, BoundActionFunctionality) {
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -112,7 +112,7 @@ TEST(ActionTest, BoundActionSafety) {
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -173,7 +173,7 @@ TEST(ActionTest, FormulaActionFunctionality) {
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -245,7 +245,7 @@ TEST(ActionTest, FormulaActionFunctionality) {
TEST(ActionTest, FormulaActionSafety){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -278,7 +278,7 @@ TEST(ActionTest, FormulaActionSafety){
TEST(ActionTest, InvertActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -312,7 +312,7 @@ TEST(ActionTest, InvertActionFunctionality){
TEST(ActionTest, RangeActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -394,7 +394,7 @@ TEST(ActionTest, RangeActionFunctionality){
TEST(ActionTest, RangeActionSafety){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -434,7 +434,7 @@ TEST(ActionTest, RangeActionSafety){
TEST(ActionTest, SortActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
@ -547,7 +547,7 @@ TEST(ActionTest, SortActionSafety){
// Check that the path result has priority over the state result if for some erronous reason both are given.
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.

4
test/functional/modelchecker/FilterTest.cpp

@ -30,7 +30,7 @@ TEST(PrctlFilterTest, generalFunctionality) {
// Setup model and modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Find the best valued state to finally reach a 'b' state.
std::string input = "filter[sort(value, descending); range(0,0)](F b)";
@ -148,7 +148,7 @@ TEST(PrctlFilterTest, generalFunctionality) {
TEST(PrctlFilterTest, Safety) {
// Setup model and modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Make a stub formula as child.
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("a");

40
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp

@ -4,13 +4,11 @@
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/InternalOptionMemento.h"
#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@ -20,41 +18,39 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("one");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("three");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
auto done = std::make_shared<storm::properties::prctl::Ap<double>>("done");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(done);
result = reachabilityRewardFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - ((double)11/3)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@ -64,34 +60,32 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@ -100,26 +94,26 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
std::vector<double> result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
result = boundedUntilFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = reachabilityRewardFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 1.044879046), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 1.044879046), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}

38
test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@ -7,7 +7,6 @@
#include "src/parser/AutoParser.h"
TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
@ -24,44 +23,44 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("three");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("four");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
@ -76,11 +75,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@ -95,15 +94,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision());
result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
ASSERT_EQ(storm::models::MDP, abstractModel->getType());
@ -120,31 +118,31 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 25);
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision());
}

6
test/functional/parser/DeterministicSparseTransitionParserTest.cpp

@ -10,7 +10,7 @@
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/storage/SparseMatrix.h"
#include "src/settings/InternalOptionMemento.h"
#include "src/settings/SettingMemento.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
@ -192,7 +192,7 @@ TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) {
TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra");
@ -217,7 +217,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) {
TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false);
std::unique_ptr<storm::settings::SettingMemento> unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException);
}

6
test/functional/parser/MarkovAutomatonSparseTransitionParserTest.cpp

@ -14,7 +14,7 @@
#include "src/parser/MarkovAutomatonSparseTransitionParser.h"
#include "src/utility/cstring.h"
#include "src/parser/MarkovAutomatonParser.h"
#include "src/settings/InternalOptionMemento.h"
#include "src/settings/SettingMemento.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h"
@ -186,7 +186,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, Whitespaces) {
TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
// Parse a Markov Automaton transition file with the fixDeadlocks Flag set and test if it works.
storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra");
@ -205,7 +205,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, FixDeadlocks) {
TEST(MarkovAutomatonSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a Markov Automaton transition file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false);
std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
ASSERT_THROW(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_deadlock.tra"), storm::exceptions::WrongFormatException);
}

6
test/functional/parser/NondeterministicSparseTransitionParserTest.cpp

@ -10,7 +10,7 @@
#include "src/parser/NondeterministicSparseTransitionParser.h"
#include "src/storage/SparseMatrix.h"
#include "src/settings/InternalOptionMemento.h"
#include "src/settings/SettingMemento.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
@ -208,7 +208,7 @@ TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) {
TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
// Set the fixDeadlocks flag temporarily. It is set to its old value once the deadlockOption object is destructed.
storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true);
std::unique_ptr<storm::settings::SettingMemento> setDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
// Parse a transitions file with the fixDeadlocks Flag set and test if it works.
storm::storage::SparseMatrix<double> result(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"));
@ -249,7 +249,7 @@ TEST(NondeterministicSparseTransitionParserTest, FixDeadlocks) {
TEST(NondeterministicSparseTransitionParserTest, DontFixDeadlocks) {
// Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception.
storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false);
std::unique_ptr<storm::settings::SettingMemento> unsetDeadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(false);
ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_deadlock.tra"), storm::exceptions::WrongFormatException);
}

24
test/functional/solver/GlpkLpSolverTest.cpp

@ -25,16 +25,16 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue("x"));
ASSERT_LT(std::abs(xValue - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue("y"));
ASSERT_LT(std::abs(yValue - 6.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(yValue - 6.5), storm::settings::generalSettings().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 2.75), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 2.75), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, LPOptimizeMin) {
@ -55,16 +55,16 @@ TEST(GlpkLpSolver, LPOptimizeMin) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue("x"));
ASSERT_LT(std::abs(xValue - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(xValue - 1), storm::settings::generalSettings().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue("y"));
ASSERT_LT(std::abs(yValue - 0), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(yValue - 0), storm::settings::generalSettings().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 5.7), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 5.7), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, MILPOptimizeMax) {
@ -91,10 +91,10 @@ TEST(GlpkLpSolver, MILPOptimizeMax) {
ASSERT_EQ(6, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 3), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, MILPOptimizeMin) {
@ -121,10 +121,10 @@ TEST(GlpkLpSolver, MILPOptimizeMin) {
ASSERT_EQ(0, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue("z"));
ASSERT_LT(std::abs(zValue - 5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(zValue - 5), storm::settings::generalSettings().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::generalSettings().getPrecision());
}
TEST(GlpkLpSolver, LPInfeasible) {

68
test/functional/solver/GmmxxLinearEquationSolverTest.cpp

@ -27,9 +27,9 @@ TEST(GmmxxLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::GmmxxLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, gmres) {
@ -51,13 +51,13 @@ TEST(GmmxxLinearEquationSolver, gmres) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50));
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, qmr) {
@ -79,13 +79,13 @@ TEST(GmmxxLinearEquationSolver, qmr) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Qmr, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::QMR, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Qmr, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, bicgstab) {
@ -107,13 +107,13 @@ TEST(GmmxxLinearEquationSolver, bicgstab) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::BICGSTAB, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::BICGSTAB, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE);
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Bicgstab, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, jacobi) {
@ -135,13 +135,13 @@ TEST(GmmxxLinearEquationSolver, jacobi) {
std::vector<double> x(3);
std::vector<double> b = {11, -16, 1};
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::JACOBI, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE));
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Jacobi, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::JACOBI, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE);
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Jacobi, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, gmresilu) {
@ -163,13 +163,13 @@ TEST(GmmxxLinearEquationSolver, gmresilu) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::ILU, true, 50));
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Ilu, true, 50));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, gmresdiag) {
@ -191,13 +191,13 @@ TEST(GmmxxLinearEquationSolver, gmresdiag) {
std::vector<double> x(3);
std::vector<double> b = {16, -4, -7};
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::DIAGONAL, true, 50));
ASSERT_NO_THROW(storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Diagonal, true, 50));
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::GMRES, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::NONE, true, 50);
storm::solver::GmmxxLinearEquationSolver<double> solver(storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, 1e-6, 10000, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::None, true, 50);
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxLinearEquationSolver, MatrixVectorMultplication) {
@ -220,5 +220,5 @@ TEST(GmmxxLinearEquationSolver, MatrixVectorMultplication) {
storm::solver::GmmxxLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(A, x, nullptr, 4));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}

14
test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp

@ -17,10 +17,10 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}
TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
@ -45,21 +45,21 @@ TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 2));
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}

8
test/functional/solver/NativeLinearEquationSolverTest.cpp

@ -27,9 +27,9 @@ TEST(NativeLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::NativeLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(A, x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(NativeLinearEquationSolver, MatrixVectorMultplication) {
@ -52,5 +52,5 @@ TEST(NativeLinearEquationSolver, MatrixVectorMultplication) {
storm::solver::NativeLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(A, x, nullptr, 4));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
}

14
test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp

@ -17,10 +17,10 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
@ -45,21 +45,21 @@ TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 2));
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::SettingsManager::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::nativeEquationSolverSettings().getPrecision());
}

26
test/functional/storm-functional-tests.cpp

@ -29,37 +29,11 @@ void setUpLogging() {
// logger.addAppender(consoleLogAppender);
}
/*!
* Creates an empty settings object as the standard instance of the Settings class.
*/
void createEmptyOptions() {
const char* newArgv[] = {"storm-functional-tests"};
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
try {
storm::settings::SettingsManager::parse(1, newArgv);
} catch (storm::exceptions::OptionParserException& e) {
std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
std::cout << std::endl << s->getHelpText();
}
}
int main(int argc, char* argv[]) {
setUpLogging();
createEmptyOptions();
std::cout << "StoRM (Functional) Testing Suite" << std::endl;
testing::InitGoogleTest(&argc, argv);
// now all Google Test Options have been removed
storm::settings::SettingsManager* instance = storm::settings::SettingsManager::getInstance();
try {
storm::settings::SettingsManager::parse(argc, argv);
} catch (storm::exceptions::OptionParserException& e) {
std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
std::cout << std::endl << instance->getHelpText();
return false;
}
int result = RUN_ALL_TESTS();

Loading…
Cancel
Save