diff --git a/CMakeLists.txt b/CMakeLists.txt index 3f4158c90..7dbacb448 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -149,6 +149,7 @@ file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB_RECURSE STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) +file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) @@ -173,6 +174,7 @@ source_group(models FILES ${STORM_MODELS_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) +source_group(solver FILES ${STORM_SOLVER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(ir FILES ${STORM_IR_FILES}) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 6c4c6486a..5f5c14d03 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -1,7 +1,7 @@ #include "src/adapters/ExplicitModelAdapter.h" #include "src/storage/SparseMatrix.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "src/exceptions/WrongFormatException.h" #include "src/ir/Program.h" @@ -32,8 +32,8 @@ namespace adapters { allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionMap() { // Get variables from program. this->initializeVariables(); - storm::settings::Settings* s = storm::settings::instance(); - this->precision = s->get("precision"); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + this->precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); } ExplicitModelAdapter::~ExplicitModelAdapter() { @@ -214,8 +214,7 @@ namespace adapters { res->push_back(commands); } // Sort the result in the vague hope that having small lists at the beginning will speed up the expanding. - // This is how lambdas may look like in C++... - res->sort([](const std::list& a, const std::list& b){ return a.size() < b.size(); }); + res->sort([] (const std::list& a, const std::list& b) -> bool { return a.size() < b.size(); }); return res; } @@ -540,7 +539,7 @@ namespace adapters { this->numberOfChoices += this->transitionMap[curIndex].size(); if (this->transitionMap[curIndex].size() == 0) { // This is a deadlock state. - if (storm::settings::instance()->isSet("fix-deadlocks")) { + if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { this->numberOfTransitions++; this->numberOfChoices++; this->transitionMap[curIndex].emplace_back(); diff --git a/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h index 6a1f82096..4e615c0af 100644 --- a/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h @@ -86,7 +86,7 @@ private: */ virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector& b) const { // Get the settings object to customize linear solving. - storm::settings::Settings* s = storm::settings::instance(); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); // Transform the submatric matrix to the eigen format to use its solvers Eigen::SparseMatrix* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(matrix); @@ -97,8 +97,9 @@ private: // decomposition failed LOG4CPLUS_ERROR(logger, "Decomposition of matrix failed!"); } - solver.setMaxIterations(s->get("maxiter")); - solver.setTolerance(s->get("precision")); + uint_fast64_t maxIterations = s->getOptionByLongName("maxIterations").getArgument(0).getValueAsUnsignedInteger(); + solver.setMaxIterations(static_cast(maxIterations)); + solver.setTolerance(s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); std::cout << matrix.toString(nullptr) << std::endl; std::cout << **vector << std::endl; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index eda3ddb63..551b7a42b 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -18,7 +18,7 @@ #include "src/models/Mdp.h" #include "src/utility/vector.h" #include "src/utility/graph.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" namespace storm { namespace modelchecker { @@ -648,9 +648,9 @@ namespace storm { storm::storage::BitVector const& maybeStates, std::vector* guessedScheduler = nullptr, std::pair, std::vector>* distancePairs = nullptr) const { - storm::settings::Settings* s = storm::settings::instance(); - double precision = s->get("precision"); - if (s->get("use-heuristic-presolve")) { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); + if (s->isSet("useHeuristicPresolve")) { // Compute both the most probable paths to target states as well as the most probable path to non-target states. // Note that here target state means a state does not *not* satisfy the property that is to be reached // if we want to minimize the reachability probability. diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h index 61f67a623..69f62c15c 100644 --- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h @@ -60,12 +60,12 @@ private: */ void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { // Get the settings object to customize solving. - storm::settings::Settings* s = storm::settings::instance(); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); // Get relevant user-defined settings for solving the equations. - double precision = s->get("precision"); - unsigned maxIterations = s->get("maxiter"); - bool relative = s->get("relative"); + double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); + uint_fast64_t maxIterations = s->getOptionByLongName("maxIterations").getArgument(0).getValueAsUnsignedInteger(); + bool relative = s->getOptionByLongName("relative").getArgument(0).getValueAsBoolean(); // Now, we need to determine the SCCs of the MDP and a topological sort. std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index 48655e302..b5763da25 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -14,7 +14,7 @@ #include "AtomicPropositionsLabeling.h" #include "AbstractNondeterministicModel.h" #include "src/storage/SparseMatrix.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" namespace storm { @@ -121,8 +121,8 @@ private: */ bool checkValidityOfProbabilityMatrix() { // Get the settings object to customize linear solving. - storm::settings::Settings* s = storm::settings::instance(); - double precision = s->get("precision"); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) { T sum = this->getTransitionMatrix().getRowSum(row); if (sum == 0) continue; diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 1813ef0ce..f3eb385b9 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -17,7 +17,7 @@ #include "AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" namespace storm { @@ -126,8 +126,8 @@ private: */ bool checkValidityOfProbabilityMatrix() { // Get the settings object to customize linear solving. - storm::settings::Settings* s = storm::settings::instance(); - double precision = s->get("precision"); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) { // not square diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 9a1fcb610..ffe10cde7 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -15,7 +15,7 @@ #include "AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "src/models/AbstractNondeterministicModel.h" namespace storm { @@ -122,8 +122,8 @@ private: */ bool checkValidityOfProbabilityMatrix() { // Get the settings object to customize linear solving. - storm::settings::Settings* s = storm::settings::instance(); - double precision = s->get("precision"); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + double precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) { T sum = this->getTransitionMatrix().getRowSum(row); if (sum == 0) continue; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 6e3f99630..f72ce391e 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -23,7 +23,7 @@ #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" #include "boost/integer/integer_mask.hpp" -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -210,7 +210,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st int_fast64_t row, lastRow = -1, col; double val; - bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); + bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; @@ -278,7 +278,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st } } - if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; + if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; /* * Finalize Matrix. diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index b94e40868..799204dd1 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -21,7 +21,7 @@ #include #include -#include "src/utility/Settings.h" +#include "src/settings/Settings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" #include "boost/integer/integer_mask.hpp" @@ -283,7 +283,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP int_fast64_t source, target, lastsource = -1, choice, lastchoice = -1; uint_fast64_t curRow = -1; double val; - bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); + bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; /* @@ -383,7 +383,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP rowMapping.at(node) = curRow + 1; } - if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; + if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; /* * Finalize matrix. diff --git a/src/settings/Argument.h b/src/settings/Argument.h index 401bfcaed..07ec9bc73 100644 --- a/src/settings/Argument.h +++ b/src/settings/Argument.h @@ -27,6 +27,8 @@ namespace storm { public: typedef std::function userValidationFunction_t; + typedef T argumentType_t; + /* T argumentValue; ArgumentType argumentType; diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h index c134e4418..754aadd5e 100644 --- a/src/settings/ArgumentBuilder.h +++ b/src/settings/ArgumentBuilder.h @@ -15,6 +15,7 @@ #include "ArgumentTypeInferationHelper.h" #include "ArgumentBase.h" #include "Argument.h" +#include "ArgumentValidators.h" #include "src/exceptions/IllegalFunctionCallException.h" #include "src/exceptions/IllegalArgumentTypeException.h" @@ -26,43 +27,6 @@ namespace storm { public: ~ArgumentBuilder() {} - template - static std::function rangeValidatorIncluding(T const lowerBound, T const upperBound) { - return std::bind([](T const lowerBound, T const upperBound, T const value, std::string& errorMessageTarget) -> bool { - bool lowerBoundCondition = (lowerBound <= value); - bool upperBoundCondition = (value <= upperBound); - if (!lowerBoundCondition) { - std::ostringstream stream; - stream << " Lower Bound Condition not met: " << lowerBound << " is not <= " << value; - errorMessageTarget.append(stream.str()); - } - if (!upperBoundCondition) { - std::ostringstream stream; - stream << " Upper Bound Condition not met: " << value << " is not <= " << upperBound; - errorMessageTarget.append(stream.str()); - } - return (lowerBoundCondition && upperBoundCondition); - }, lowerBound, upperBound, std::placeholders::_1, std::placeholders::_2); - } - template - static std::function rangeValidatorExcluding(T const lowerBound, T const upperBound) { - return std::bind([](T const lowerBound, T const upperBound, T const value, std::string& errorMessageTarget) -> bool { - bool lowerBoundCondition = (lowerBound < value); - bool upperBoundCondition = (value < upperBound); - if (!lowerBoundCondition) { - std::ostringstream stream; - stream << " Lower Bound Condition not met: " << lowerBound << " is not < " << value; - errorMessageTarget.append(stream.str()); - } - if (!upperBoundCondition) { - std::ostringstream stream; - stream << " Upper Bound Condition not met: " << value << " is not < " << upperBound; - errorMessageTarget.append(stream.str()); - } - return (lowerBoundCondition && upperBoundCondition); - }, lowerBound, upperBound, std::placeholders::_1, std::placeholders::_2); - } - /* Preparation Functions for all ArgumentType's diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h new file mode 100644 index 000000000..4d0ce8170 --- /dev/null +++ b/src/settings/ArgumentValidators.h @@ -0,0 +1,125 @@ +#ifndef STORM_SETTINGS_ARGUMENTVALIDATORS_H_ +#define STORM_SETTINGS_ARGUMENTVALIDATORS_H_ + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "Argument.h" + +namespace storm { + namespace settings { + class ArgumentValidators { + public: + // Integer - int_fast64_t + static std::function integerRangeValidatorIncluding(int_fast64_t const lowerBound, int_fast64_t const upperBound) { + return rangeValidatorIncluding(lowerBound, upperBound); + } + static std::function integerRangeValidatorExcluding(int_fast64_t const lowerBound, int_fast64_t const upperBound) { + return rangeValidatorExcluding(lowerBound, upperBound); + } + + // UnsignedInteger - uint_fast64_t + static std::function unsignedIntegerRangeValidatorIncluding(uint_fast64_t const lowerBound, uint_fast64_t const upperBound) { + return rangeValidatorIncluding(lowerBound, upperBound); + } + static std::function unsignedIntegerRangeValidatorExcluding(uint_fast64_t const lowerBound, uint_fast64_t const upperBound) { + return rangeValidatorExcluding(lowerBound, upperBound); + } + + // Double - double + static std::function doubleRangeValidatorIncluding(double const lowerBound, double const upperBound) { + return rangeValidatorIncluding(lowerBound, upperBound); + } + static std::function doubleRangeValidatorExcluding(double const lowerBound, double const upperBound) { + return rangeValidatorExcluding(lowerBound, upperBound); + } + + static std::function existingReadableFileValidator() { + return [] (std::string const fileName, std::string& errorMessageTarget) -> bool { + std::ifstream targetFile(fileName); + bool isFileGood = targetFile.good(); + + if (!isFileGood) { + std::ostringstream stream; + stream << "Given file does not exist or is not readable by this process: \"" << fileName << "\"" << std::endl; + errorMessageTarget.append(stream.str()); + } + return isFileGood; + }; + } + + static std::function stringInListValidator(std::vector list) { + return [list] (std::string const inputString, std::string& errorMessageTarget) -> bool { + bool containsElement = false; + std::string const lowerInputString = storm::utility::StringHelper::stringToLower(inputString); + for (auto it = list.cbegin(); it != list.cend(); ++it) { + if (storm::utility::StringHelper::stringToLower(*it).compare(lowerInputString) == 0) { + return true; + } + } + + std::ostringstream stream; + stream << "The given Input \"" << inputString << "\" is not in the list of valid Items ("; + bool first = true; + for (auto it = list.cbegin(); it != list.cend(); ++it) { + if (!first) { + stream << ", "; + } + stream << *it; + first = false; + } + stream << ")" << std::endl; + errorMessageTarget.append(stream.str()); + + return false; + }; + } + private: + template + static std::function rangeValidatorIncluding(T const lowerBound, T const upperBound) { + return std::bind([](T const lowerBound, T const upperBound, T const value, std::string& errorMessageTarget) -> bool { + bool lowerBoundCondition = (lowerBound <= value); + bool upperBoundCondition = (value <= upperBound); + if (!lowerBoundCondition) { + std::ostringstream stream; + stream << " Lower Bound Condition not met: " << lowerBound << " is not <= " << value; + errorMessageTarget.append(stream.str()); + } + if (!upperBoundCondition) { + std::ostringstream stream; + stream << " Upper Bound Condition not met: " << value << " is not <= " << upperBound; + errorMessageTarget.append(stream.str()); + } + return (lowerBoundCondition && upperBoundCondition); + }, lowerBound, upperBound, std::placeholders::_1, std::placeholders::_2); + } + template + static std::function rangeValidatorExcluding(T const lowerBound, T const upperBound) { + return std::bind([](T const lowerBound, T const upperBound, T const value, std::string& errorMessageTarget) -> bool { + bool lowerBoundCondition = (lowerBound < value); + bool upperBoundCondition = (value < upperBound); + if (!lowerBoundCondition) { + std::ostringstream stream; + stream << " Lower Bound Condition not met: " << lowerBound << " is not < " << value; + errorMessageTarget.append(stream.str()); + } + if (!upperBoundCondition) { + std::ostringstream stream; + stream << " Upper Bound Condition not met: " << value << " is not < " << upperBound; + errorMessageTarget.append(stream.str()); + } + return (lowerBoundCondition && upperBoundCondition); + }, lowerBound, upperBound, std::placeholders::_1, std::placeholders::_2); + } + }; + } +} + +#endif // STORM_SETTINGS_ARGUMENTVALIDATORS_H_ \ No newline at end of file diff --git a/src/settings/Settings.cpp b/src/settings/Settings.cpp index 97c504bfb..b244eb1e2 100644 --- a/src/settings/Settings.cpp +++ b/src/settings/Settings.cpp @@ -211,7 +211,10 @@ storm::settings::Settings& storm::settings::Settings::addOption(Option* option) // Copy Shared_ptr this->options.insert(std::make_pair(lowerLongName, std::shared_ptr