sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

The tests now run fine with the new option system. 

Former-commit-id: 6d6c510131
tempestpy_adaptions
dehnert 10 years ago
parent
266d660d89
commit
a995d7dd4a
18 changed files with 166 additions and 163 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 33
      src/settings/Argument.h
  2. 28
      src/settings/ArgumentBuilder.h
  3. 105
      src/settings/ArgumentTypeInferationHelper.cpp
  4. 61
      src/settings/ArgumentTypeInferationHelper.h
  5. 2
      src/settings/ArgumentValidators.h
  6. 1
      src/settings/Option.h
  7. 2
      src/settings/SettingsManager.cpp
  8. 1
      src/settings/SettingsManager.h
  9. 2
      src/settings/modules/CounterexampleGeneratorSettings.cpp
  10. 3
      src/settings/modules/GeneralSettings.cpp
  11. 4
      src/settings/modules/GmmxxEquationSolverSettings.cpp
  12. 6
      src/settings/modules/ModuleSettings.cpp
  13. 2
      src/settings/modules/NativeEquationSolverSettings.cpp
  14. 6
      src/solver/GmmxxLinearEquationSolver.cpp
  15. 2
      test/functional/solver/GlpkLpSolverTest.cpp
  16. 26
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  17. 30
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  18. 15
      test/performance/storm-performance-tests.cpp

33
src/settings/Argument.h
View File

@ -43,7 +43,7 @@ namespace storm {
* to this argument.
* @param isOptional A flag indicating whether the argument is optional.
*/
Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
// Intentionally left empty.
}
@ -56,9 +56,9 @@ namespace storm {
* to this argument.
* @param isOptional A flag indicating whether the argument is optional.
*/
Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(defaultValue), hasDefaultValue(true) {
// Intentionally left empty.
}
Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
this->setDefaultValue(defaultValue);
}
virtual bool getIsOptional() const override {
return this->isOptional;
@ -106,8 +106,12 @@ namespace storm {
* @return The value of the argument.
*/
T const& getArgumentValue() const {
LOG_THROW(this->getHasBeenSet(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was not set.");
return this->argumentValue;
LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was neither set nor specifies a default value.");
if (this->getHasBeenSet()) {
return this->argumentValue;
} else {
return this->defaultValue;
}
}
virtual bool getHasDefaultValue() const override {
@ -123,9 +127,9 @@ namespace storm {
virtual std::string getValueAsString() const override {
switch (this->argumentType) {
case ArgumentType::String:
return ArgumentTypeInferation::inferToString(ArgumentType::String, this->getArgumentValue());
return inferToString(ArgumentType::String, this->getArgumentValue());
case ArgumentType::Boolean: {
bool iValue = ArgumentTypeInferation::inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
bool iValue = inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
if (iValue) {
return "true";
} else {
@ -139,7 +143,7 @@ namespace storm {
virtual int_fast64_t getValueAsInteger() const override {
switch (this->argumentType) {
case ArgumentType::Integer:
return ArgumentTypeInferation::inferToInteger(ArgumentType::Integer, this->getArgumentValue());
return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
}
}
@ -148,7 +152,7 @@ namespace storm {
virtual uint_fast64_t getValueAsUnsignedInteger() const override {
switch (this->argumentType) {
case ArgumentType::UnsignedInteger:
return ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
}
}
@ -157,7 +161,7 @@ namespace storm {
virtual double getValueAsDouble() const override {
switch (this->argumentType) {
case ArgumentType::Double:
return ArgumentTypeInferation::inferToDouble(ArgumentType::Double, this->getArgumentValue());
return inferToDouble(ArgumentType::Double, this->getArgumentValue());
default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
}
}
@ -166,7 +170,7 @@ namespace storm {
virtual bool getValueAsBoolean() const override {
switch (this->argumentType) {
case ArgumentType::Boolean:
return ArgumentTypeInferation::inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
}
}
@ -190,6 +194,11 @@ namespace storm {
// A flag indicating whether a default value has been provided.
bool hasDefaultValue;
/*!
* Sets the default value of the argument to the provided value.
*
* @param newDefault The new default value of the argument.
*/
void setDefaultValue(T const& newDefault) {
LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
this->defaultValue = newDefault;

28
src/settings/ArgumentBuilder.h
View File

@ -12,7 +12,6 @@
#include <string>
#include "src/settings/ArgumentType.h"
#include "src/settings/ArgumentTypeInferationHelper.h"
#include "src/settings/ArgumentBase.h"
#include "src/settings/Argument.h"
#include "src/settings/ArgumentValidators.h"
@ -97,13 +96,14 @@ namespace storm {
*/
ArgumentBuilder& setIsOptional(bool isOptional) {
this->isOptional = isOptional;
LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to make argument '" << this->name << "' optional without default value.");
return *this;
}
#define PPCAT_NX(A, B) A ## B
#define PPCAT(A, B) PPCAT_NX(A, B)
#define MACROaddValidationFunction(funcName, funcType) ArgumentBuilder& PPCAT(addValidationFunction, funcName) (storm::settings::Argument< funcType >::userValidationFunction_t userValidationFunction) { \
LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type.") \
LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type."); \
( PPCAT(this->userValidationFunctions_, funcName) ).push_back(userValidationFunction); \
return *this; \
}
@ -117,12 +117,12 @@ return *this; \
#define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \
LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type.") \
LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type."); \
PPCAT(this->defaultValue_, funcName) = defaultValue; \
this->hasDefaultValue = true; \
return *this; \
}
// Add the methods to set a default value.
MACROsetDefaultValue(String, std::string)
MACROsetDefaultValue(Integer, int_fast64_t)
@ -141,38 +141,38 @@ return *this; \
switch (this->type) {
case ArgumentType::String: {
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, userValidationFunctions_String, this->isOptional, this->defaultValue_String));
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->userValidationFunctions_String, this->isOptional, this->defaultValue_String));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, userValidationFunctions_String));
return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->userValidationFunctions_String));
}
break;
}
case ArgumentType::Integer:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer));
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, userValidationFunctions_Integer));
return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->userValidationFunctions_Integer));
}
break;
case ArgumentType::UnsignedInteger:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, userValidationFunctions_UnsignedInteger));
return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->userValidationFunctions_UnsignedInteger));
}
break;
case ArgumentType::Double:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, userValidationFunctions_Double, this->isOptional, this->defaultValue_Double));
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->userValidationFunctions_Double, this->isOptional, this->defaultValue_Double));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, userValidationFunctions_Double));
return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->userValidationFunctions_Double));
}
break;
case ArgumentType::Boolean:
if (this->hasDefaultValue) {
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean));
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean));
} else {
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, userValidationFunctions_Boolean));
return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->userValidationFunctions_Boolean));
}
break;
}

105
src/settings/ArgumentTypeInferationHelper.cpp
View File

@ -2,126 +2,127 @@
namespace storm {
namespace settings {
template <typename T>
ArgumentType ArgumentTypeInferation::inferToEnumType() {
ArgumentType inferToEnumType() {
LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer type of argument.");
}
template <>
ArgumentType ArgumentTypeInferation::inferToEnumType<std::string>() {
ArgumentType inferToEnumType<std::string>() {
return ArgumentType::String;
}
template <>
ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>() {
ArgumentType inferToEnumType<int_fast64_t>() {
return ArgumentType::Integer;
}
template <>
ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>() {
ArgumentType inferToEnumType<uint_fast64_t>() {
return ArgumentType::UnsignedInteger;
}
template <>
ArgumentType ArgumentTypeInferation::inferToEnumType<double>() {
ArgumentType inferToEnumType<double>() {
return ArgumentType::Double;
}
template <>
ArgumentType ArgumentTypeInferation::inferToEnumType<bool>() {
ArgumentType inferToEnumType<bool>() {
return ArgumentType::Boolean;
}
template <typename T>
std::string const& ArgumentTypeInferation::inferToString(ArgumentType const& argumentType, T const& value) {
std::string const& inferToString(ArgumentType const& argumentType, T const& value) {
LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument value.");
}
template <>
std::string const& ArgumentTypeInferation::inferToString<std::string>(ArgumentType const& argumentType, std::string const& value) {
std::string const& inferToString<std::string>(ArgumentType const& argumentType, std::string const& value) {
LOG_THROW(argumentType == ArgumentType::String, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument.");
return value;
}
template <typename T>
int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType const& argumentType, T const& value) {
int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value) {
LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument value.");
}
template <>
int_fast64_t ArgumentTypeInferation::inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value) {
int_fast64_t inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value) {
LOG_THROW(argumentType == ArgumentType::Integer, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
return value;
}
template <typename T>
uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType const& argumentType, T const& value) {
uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value) {
LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer unsigned integer from non-unsigned argument value.");
}
template <>
uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value) {
uint_fast64_t inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value) {
LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
return value;
}
template <typename T>
double ArgumentTypeInferation::inferToDouble(ArgumentType const& argumentType, T const& value) {
double inferToDouble(ArgumentType const& argumentType, T const& value) {
LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument value.");
}
template <>
double ArgumentTypeInferation::inferToDouble<double>(ArgumentType const& argumentType, double const& value) {
LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument.");
double inferToDouble<double>(ArgumentType const& argumentType, double const& value) {
LOG_THROW(argumentType == ArgumentType::Double, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument.");
return value;
}
template <typename T>
bool ArgumentTypeInferation::inferToBoolean(ArgumentType const& argumentType, T const& value) {
bool inferToBoolean(ArgumentType const& argumentType, T const& value) {
LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument value.");
}
template <>
bool ArgumentTypeInferation::inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value) {
bool inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value) {
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);
template ArgumentType inferToEnumType<std::string>();
template ArgumentType inferToEnumType<int_fast64_t>();
template ArgumentType inferToEnumType<uint_fast64_t>();
template ArgumentType inferToEnumType<double>();
template ArgumentType inferToEnumType<bool>();
template std::string const& inferToString<std::string>(ArgumentType const& argumentType, std::string const& value);
template std::string const& inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template std::string const& inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template std::string const& inferToString<double>(ArgumentType const& argumentType, double const& value);
template std::string const& inferToString<bool>(ArgumentType const& argumentType, bool const& value);
template int_fast64_t inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
template int_fast64_t inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template int_fast64_t inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template int_fast64_t inferToInteger<double>(ArgumentType const& argumentType, double const& value);
template int_fast64_t inferToInteger<bool>(ArgumentType const& argumentType, bool const& value);
template uint_fast64_t inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
template uint_fast64_t inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template uint_fast64_t inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template uint_fast64_t inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value);
template uint_fast64_t inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value);
template double inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value);
template double inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template double inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template double inferToDouble<double>(ArgumentType const& argumentType, double const& value);
template double inferToDouble<bool>(ArgumentType const& argumentType, bool const& value);
template bool inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value);
template bool inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
template bool inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
template bool inferToBoolean<double>(ArgumentType const& argumentType, double const& value);
template bool inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value);
}
}

61
src/settings/ArgumentTypeInferationHelper.h
View File

@ -9,30 +9,47 @@
#include "src/exceptions/InternalTypeErrorException.h"
namespace storm {
namespace settings {
namespace settings {
/*!
* This class serves as a helper class to infer the types of arguments.
* This function infers the type in our enum of possible types from the template parameter.
*
* @return The argument type that has been inferred.
*/
class ArgumentTypeInferation {
public:
// Specialized function template that infers the Type of T to our local enum
/*!
* This function infers the type in our enum of possible types from the template parameter.
*
* @return The argument type that has been inferred.
*/
template <typename T>
static ArgumentType inferToEnumType();
// Specialized function templates that allow casting the given value to the correct type. If the conversion
// fails, an exception is thrown.
template <typename T> static std::string const& inferToString(ArgumentType const& argumentType, T const& value);
template <typename T> static int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value);
template <typename T> static uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value);
template <typename T> static double inferToDouble(ArgumentType const& argumentType, T const& value);
template <typename T> static bool inferToBoolean(ArgumentType const& argumentType, T const& value);
};
} // namespace settings
template <typename T>
ArgumentType inferToEnumType();
// Specialized function templates that allow casting the given value to the correct type. If the conversion
// fails, an exception is thrown.
template <typename T>
std::string const& inferToString(ArgumentType const& argumentType, T const& value);
template <>
std::string const& inferToString(ArgumentType const& argumentType, std::string const& value);
template <typename T>
int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value);
template <>
int_fast64_t inferToInteger(ArgumentType const& argumentType, int_fast64_t const& value);
template <typename T>
uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value);
template <>
uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, uint_fast64_t const& value);
template <typename T>
double inferToDouble(ArgumentType const& argumentType, T const& value);
template <>
double inferToDouble(ArgumentType const& argumentType, double const& value);
template <typename T>
bool inferToBoolean(ArgumentType const& argumentType, T const& value);
template <>
bool inferToBoolean(ArgumentType const& argumentType, bool const& value);
} // namespace settings
} // namespace storm
#endif // STORM_SETTINGS_ARGUMENTTYPEINFERATIONHELPER_H_

2
src/settings/ArgumentValidators.h
View File

@ -115,7 +115,7 @@ namespace storm {
}
}
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value " << inputString << " does not match any entry in the list of valid items.");
LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value '" << inputString << "' does not match any entry in the list of valid items.");
return false;
};
}

1
src/settings/Option.h
View File

@ -74,7 +74,6 @@ 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++) {

2
src/settings/SettingsManager.cpp
View File

@ -62,9 +62,7 @@ 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];

1
src/settings/SettingsManager.h
View File

@ -17,7 +17,6 @@
#include "src/settings/Argument.h"
#include "src/settings/ArgumentBuilder.h"
#include "src/settings/ArgumentType.h"
#include "src/settings/ArgumentTypeInferationHelper.h"
#include "src/settings/modules/ModuleSettings.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/DebugSettings.h"

2
src/settings/modules/CounterexampleGeneratorSettings.cpp
View File

@ -13,7 +13,7 @@ namespace storm {
const std::string CounterexampleGeneratorSettings::statisticsOptionName = "stats";
CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> techniques = {"sat", "milp"};
std::vector<std::string> techniques = {"maxsat", "milp"};
this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());

3
src/settings/modules/GeneralSettings.cpp
View File

@ -93,7 +93,8 @@ namespace storm {
}
double GeneralSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
double value = this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
return value;
}
bool GeneralSettings::isExportDotSet() const {

4
src/settings/modules/GmmxxEquationSolverSettings.cpp
View File

@ -25,7 +25,7 @@ namespace storm {
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->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->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(20000).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());
@ -47,7 +47,7 @@ namespace storm {
}
GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
std::string preconditioningTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
std::string preconditioningTechniqueAsString = this->getOption(preconditionOptionName).getArgumentByName("name").getValueAsString();
if (preconditioningTechniqueAsString == "ilu") {
return GmmxxEquationSolverSettings::PreconditioningTechnique::Ilu;
} else if (preconditioningTechniqueAsString == "diagonal") {

6
src/settings/modules/ModuleSettings.cpp
View File

@ -49,10 +49,10 @@ namespace storm {
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 {
if (requiredStatus) {
this->set(name);
} else {
this->unset(name);
}
return std::unique_ptr<storm::settings::SettingMemento>(new storm::settings::SettingMemento(*this, name, currentStatus));
}

2
src/settings/modules/NativeEquationSolverSettings.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
std::vector<std::string> methods = { "jacobi" };
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->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->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(20000).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());

6
src/solver/GmmxxLinearEquationSolver.cpp
View File

@ -24,11 +24,11 @@ namespace storm {
template<typename ValueType>
GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver() {
// Get the settings object to customize linear solving.
storm::settings::modules::GmmxxEquationSolverSettings const& settings =storm::settings::gmmxxEquationSolverSettings();
storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings();
// Get appropriate settings.
maximalNumberOfIterations = settings.getMaximalIterationCount();
precision = settings.getPrecision();;
precision = settings.getPrecision();
relative = settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
restart = settings.getRestartIterationCount();
@ -89,7 +89,7 @@ namespace storm {
} else if (preconditioner == Preconditioner::None) {
gmm::qmr(*gmmA, x, b, gmm::identity_matrix(), iter);
}
} else if (method == SolutionMethod::Qmr) {
} else if (method == SolutionMethod::Gmres) {
if (preconditioner == Preconditioner::Ilu) {
gmm::gmres(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmA), restart, iter);
} else if (preconditioner == Preconditioner::Diagonal) {

2
test/functional/solver/GlpkLpSolverTest.cpp
View File

@ -18,7 +18,7 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5)));
ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5)));
ASSERT_NO_THROW(solver.update());
ASSERT_NO_THROW(solver.optimize());
ASSERT_TRUE(solver.isOptimal());
ASSERT_FALSE(solver.isUnbounded());

26
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -1,15 +1,13 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/InternalOptionMemento.h"
#include "src/settings/SettingMemento.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/parser/AutoParser.h"
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/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@ -19,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, 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);
@ -28,7 +26,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
std::vector<double> result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.2296800237), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
@ -37,7 +35,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.05073232193), storm::settings::gmmxxEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
@ -46,14 +44,12 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.22742171078), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.22742171078), 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/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@ -63,7 +59,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, 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);
@ -72,7 +68,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
std::vector<double> result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
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);
@ -81,7 +77,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
result = boundedUntilFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.9993949793), 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);
@ -90,5 +86,5 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
result = reachabilityRewardFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 1.025106273), storm::settings::gmmxxEquationSolverSettings().getPrecision());
}

30
test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
View File

@ -7,7 +7,6 @@
#include "src/parser/AutoParser.h"
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/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
@ -24,37 +23,36 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*eventuallyFormula, 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::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.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 0.0), 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] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 6.172433512), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[0] - 6.1724344), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
// Increase the maximal number of iterations, because the solver does not converge otherwise.
// This is done in the main cpp unit
@ -74,7 +72,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("all_coins_equal_0");
@ -83,7 +81,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkOptimizingOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 0.4374282832), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("all_coins_equal_1");
@ -92,7 +90,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 0.5293286369), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("agree");
@ -102,27 +100,27 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
result = mc.checkOptimizingOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 0.10414097), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 50ull);
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 1725.593313), storm::settings::nativeEquationSolverSettings().getPrecision());
result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_LT(std::abs(result[31168] - 2183.142422), storm::settings::nativeEquationSolverSettings().getPrecision());
}

15
test/performance/storm-performance-tests.cpp
View File

@ -29,23 +29,8 @@ void setUpLogging() {
// logger.addAppender(consoleLogAppender);
}
/*!
* Creates an empty settings object as the standard instance of the Settings class.
*/
void createEmptyOptions() {
const char* newArgv[] = {"storm-performance-tests", "--maxiter", "20000"};
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
try {
storm::settings::SettingsManager::parse(3, 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 (Performance) Testing Suite" << std::endl;
testing::InitGoogleTest(&argc, argv);

Write Preview
Loading…
Cancel
Save