diff --git a/CMakeLists.txt b/CMakeLists.txt index ef0a82022..41d058a4b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -371,10 +371,11 @@ endif() ############################################################# file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) +file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) -set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE};") file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) +file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp) file(GLOB STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) @@ -410,10 +411,15 @@ file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/perf # Additional include files like the storm-config.h file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) +set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN}) +list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_CLI}) +set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE}) + # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) +source_group(cli FILES ${STORM_CLI_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(logic FILES ${STORM_LOGIC_FILES}) source_group(generated FILES ${STORM_BUILD_HEADERS} ${STORM_BUILD_SOURCES}) @@ -492,8 +498,8 @@ endif() ## All link_directories() calls MUST be made before this point # ## # ############################################################################### -add_library(storm ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) -add_executable(storm-main ${STORM_MAIN_FILE}) +add_library(storm ${STORM_LIB_SOURCES}) +add_executable(storm-main ${STORM_MAIN_SOURCES}) target_link_libraries(storm-main storm) set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm") add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES}) diff --git a/src/utility/cli.cpp b/src/cli/cli.cpp similarity index 98% rename from src/utility/cli.cpp rename to src/cli/cli.cpp index d21e21420..7a9ea6f3c 100644 --- a/src/utility/cli.cpp +++ b/src/cli/cli.cpp @@ -1,9 +1,12 @@ #include "cli.h" +#include "../utility/storm.h" #include "src/settings/modules/DebugSettings.h" #include "src/exceptions/OptionParserException.h" +#include "src/utility/storm-version.h" + // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB # include "tbb/tbb_stddef.h" @@ -30,7 +33,6 @@ #endif namespace storm { - namespace utility { namespace cli { std::string getCurrentWorkingDirectory() { char temp[512]; @@ -196,14 +198,14 @@ namespace storm { LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); } if (storm::settings::debugSettings().isLogfileSet()) { - initializeFileLogging(); + storm::utility::initializeFileLogging(); } return true; } void processOptions() { if (storm::settings::debugSettings().isLogfileSet()) { - initializeFileLogging(); + storm::utility::initializeFileLogging(); } storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); @@ -253,5 +255,4 @@ namespace storm { } } - } -} \ No newline at end of file + } \ No newline at end of file diff --git a/src/cli/cli.h b/src/cli/cli.h new file mode 100644 index 000000000..896b7bee2 --- /dev/null +++ b/src/cli/cli.h @@ -0,0 +1,29 @@ +#ifndef STORM_UTILITY_CLI_H_ +#define STORM_UTILITY_CLI_H_ + +#include <string> + +namespace storm { + namespace cli { + + std::string getCurrentWorkingDirectory(); + + void printHeader(const int argc, const char* argv[]); + + void printUsage(); + + /*! + * Parses the given command line arguments. + * + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ + bool parseOptions(const int argc, const char* argv[]); + + + void processOptions(); + } +} + +#endif diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 8aa20c54f..762c8126d 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -4,6 +4,7 @@ #include "src/storage/dd/CuddOdd.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index bf5a7a48a..03838e6c0 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -3,11 +3,16 @@ #include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" -#include "src/models/symbolic/Mdp.h" - #include "src/utility/solver.h" +#include "src/storage/dd/DdType.h" namespace storm { + namespace models { + namespace symbolic { + template<storm::dd::DdType T> class Mdp; + } + } + namespace modelchecker { template<storm::dd::DdType DdType, typename ValueType> class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType> { diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h index f24ece9ab..9565a4bc9 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h @@ -3,7 +3,6 @@ #include "src/modelchecker/AbstractModelChecker.h" -#include "src/models/sparse/Model.h" namespace storm { namespace modelchecker { diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index ec3433dec..03b863d6c 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -2,11 +2,19 @@ #define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_ #include "src/modelchecker/AbstractModelChecker.h" -#include "src/models/symbolic/Model.h" + +#include "src/storage/dd/DdType.h" namespace storm { + namespace models { + namespace symbolic { + template<storm::dd::DdType Type> class Model; + } + } + namespace modelchecker { + template<storm::dd::DdType Type> class SymbolicPropositionalModelChecker : public AbstractModelChecker { public: diff --git a/src/models/ModelBase.h b/src/models/ModelBase.h index 24f6d627d..4bbe31b64 100644 --- a/src/models/ModelBase.h +++ b/src/models/ModelBase.h @@ -5,7 +5,6 @@ #include "src/models/ModelType.h" #include "src/utility/macros.h" -#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace models { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 334422dba..bf1b5c3e4 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -4,7 +4,6 @@ #include "src/models/sparse/DeterministicModel.h" #include "src/utility/OsDetection.h" -#include "src/utility/constants.h" #include "src/adapters/CarlAdapter.h" namespace storm { diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index bf9da8713..514d2ee0c 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -9,11 +9,14 @@ #include "src/models/ModelBase.h" #include "src/models/sparse/StateLabeling.h" #include "src/storage/sparse/StateType.h" -#include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" #include "src/utility/OsDetection.h" namespace storm { + namespace storage { + class BitVector; + } + namespace models { namespace sparse { diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 7c31e3fa1..408f8af7c 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -3,6 +3,7 @@ #include <boost/algorithm/string/join.hpp> #include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/InvalidOperationException.h" #include "src/adapters/AddExpressionAdapter.h" diff --git a/src/solver/AllowEarlyTerminationCondition.cpp b/src/solver/AllowEarlyTerminationCondition.cpp new file mode 100644 index 000000000..d58fd1903 --- /dev/null +++ b/src/solver/AllowEarlyTerminationCondition.cpp @@ -0,0 +1,54 @@ +#include "AllowEarlyTerminationCondition.h" +#include "src/utility/vector.h" + +namespace storm { + namespace solver { + + template<typename ValueType> + TerminateAfterFilteredSumPassesThresholdValue<ValueType>::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove) : + terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove) + { + // Intentionally left empty. + } + + template<typename ValueType> + bool TerminateAfterFilteredSumPassesThresholdValue<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const { + assert(currentValues.size() >= filter.size()); + ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); + + if(this->terminateIfAboveThreshold) { + return currentThreshold >= this->terminationThreshold; + } else { + return currentThreshold <= this->terminationThreshold; + } + + } + + template<typename ValueType> + TerminateAfterFilteredExtremumPassesThresholdValue<ValueType>::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove, bool useMinimum) : + terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove), useMinimumAsExtremum(useMinimum) + { + // Intentionally left empty. + } + + template<typename ValueType> + bool TerminateAfterFilteredExtremumPassesThresholdValue<ValueType>::terminateNow(const std::vector<ValueType>& currentValues) const { + assert(currentValues.size() >= filter.size()); + + ValueType initVal = terminateIfAboveThreshold ? terminationThreshold - 1 : terminationThreshold + 1; + ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); + + if(this->terminateIfAboveThreshold) { + return currentThreshold >= this->terminationThreshold; + } else { + return currentThreshold <= this->terminationThreshold; + } + + } + + + template class TerminateAfterFilteredExtremumPassesThresholdValue<double>; + template class TerminateAfterFilteredSumPassesThresholdValue<double>; + + } +} diff --git a/src/solver/AllowEarlyTerminationCondition.h b/src/solver/AllowEarlyTerminationCondition.h new file mode 100644 index 000000000..e2e3000b4 --- /dev/null +++ b/src/solver/AllowEarlyTerminationCondition.h @@ -0,0 +1,54 @@ +#ifndef ALLOWEARLYTERMINATIONCONDITION_H +#define ALLOWEARLYTERMINATIONCONDITION_H + +#include <vector> +#include "src/storage/BitVector.h" + + +namespace storm { + namespace solver { + template<typename ValueType> + class AllowEarlyTerminationCondition { + public: + virtual bool terminateNow(std::vector<ValueType> const& currentValues) const = 0; + }; + + template<typename ValueType> + class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition<ValueType> { + public: + bool terminateNow(std::vector<ValueType> const& currentValues) const { return false; } + }; + + template<typename ValueType> + class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition<ValueType> { + public: + TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove); + bool terminateNow(std::vector<ValueType> const& currentValues) const; + + protected: + ValueType terminationThreshold; + storm::storage::BitVector filter; + bool terminateIfAboveThreshold; + }; + + template<typename ValueType> + class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition<ValueType>{ + public: + TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove, bool useMinimum); + bool terminateNow(std::vector<ValueType> const& currentValue) const; + + protected: + ValueType terminationThreshold; + storm::storage::BitVector filter; + bool terminateIfAboveThreshold; + bool useMinimumAsExtremum; + }; + } +} + + + + + +#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ + diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index b4357b6d4..11f5171c2 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -53,7 +53,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); @@ -119,7 +119,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Take the sub-matrix according to the current choices storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 680ee7ee0..f0c2e4869 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -19,6 +19,10 @@ namespace storm { } } + void AbstractMinMaxLinearEquationSolver::setPolicyTracking(bool setToTrue) { + trackPolicy = setToTrue; + } + std::vector<storm::storage::sparse::state_type> AbstractMinMaxLinearEquationSolver::getPolicy() const { STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); return policy; diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 6e6887cd8..b5d53a68e 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -5,6 +5,7 @@ #include <cstdint> #include "SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" +#include "AllowEarlyTerminationCondition.h" namespace storm { namespace storage { @@ -55,7 +56,7 @@ namespace storm { protected: MinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), - A(matrix) { + A(matrix), earlyTermination(new NoEarlyTerminationCondition<ValueType>()) { // Intentionally left empty. } @@ -101,7 +102,13 @@ namespace storm { */ virtual void performMatrixVectorMultiplication(bool minimize, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const = 0; + + void setEarlyTerminationCondition(std::unique_ptr<AllowEarlyTerminationCondition<ValueType>> v) { + earlyTermination = std::move(v); + } + protected: + std::unique_ptr<AllowEarlyTerminationCondition<ValueType>> earlyTermination; storm::storage::SparseMatrix<ValueType> const& A; }; diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 87ee3b043..4ac37ac3e 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -53,7 +53,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Compute x' = A*x + b. this->A.multiplyWithVector(*currentX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); @@ -121,7 +121,7 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < this->maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations && !this->earlyTermination->terminateNow(*currentX)) { // Take the sub-matrix according to the current choices storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); diff --git a/src/solver/SolverSelectionOptions.h b/src/solver/SolverSelectionOptions.h index cfba09a15..51f448644 100644 --- a/src/solver/SolverSelectionOptions.h +++ b/src/solver/SolverSelectionOptions.h @@ -11,7 +11,8 @@ namespace storm { ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk) - ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx) + ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Topological) + } } diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 3b0fba916..d66591f76 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -13,6 +13,7 @@ #include "src/storage/Distribution.h" #include "src/utility/constants.h" #include "src/utility/OsDetection.h" +#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace utility { diff --git a/src/storm.cpp b/src/storm.cpp index 2ed0a42d3..3b060120b 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -1,22 +1,22 @@ // Include other headers. #include "src/exceptions/BaseException.h" #include "src/utility/macros.h" -#include "src/utility/cli.h" - +#include "src/cli/cli.h" +#include "src/utility/initialize.h" /*! * Main entry point of the executable storm. */ int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::utility::cli::printHeader(argc, argv); - bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv); + storm::cli::printHeader(argc, argv); + bool optionsCorrect = storm::cli::parseOptions(argc, argv); if (!optionsCorrect) { return -1; } // From this point on we are ready to carry out the actual computations. - storm::utility::cli::processOptions(); + storm::cli::processOptions(); // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 66927c131..05d5bf479 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -81,30 +81,56 @@ namespace storm { } template<typename ValueType> - std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); - switch (equationSolver) { - case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix)); - case storm::solver::EquationSolverType::Native: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix)); - default: return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix)); - } + MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver) + { + setSolverType(solver); + prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS; } - + template<typename ValueType> - std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> GmmxxMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const { - return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix)); + void MinMaxLinearEquationSolverFactory<ValueType>::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { + if(solverTypeSel == storm::solver::EquationSolverTypeSelection::FROMSETTINGS) { + this->solverType = storm::settings::generalSettings().getEquationSolver(); + } else { + this->solverType = storm::solver::convert(solverTypeSel); + } + } - template<typename ValueType> - std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> NativeMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const { - return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix)); - } + void MinMaxLinearEquationSolverFactory<ValueType>::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { + this->prefTech = preferredTech; + } + template<typename ValueType> - std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const { - return std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>(new storm::solver::TopologicalMinMaxLinearEquationSolver<ValueType>(matrix)); + std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy) const { + + std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p1; + + switch (solverType) { + case storm::solver::EquationSolverType::Gmmxx: + { + p1.reset(new storm::solver::GmmxxMinMaxLinearEquationSolver<ValueType>(matrix, this->prefTech)); + break; + } + case storm::solver::EquationSolverType::Native: + { + p1.reset(new storm::solver::NativeMinMaxLinearEquationSolver<ValueType>(matrix, this->prefTech)); + break; + } + case storm::solver::EquationSolverType::Topological: + { + STORM_LOG_THROW(prefTech == storm::solver::MinMaxTechniqueSelection::PolicyIteration, storm::exceptions::NotImplementedException, "Policy iteration for topological solver is not supported."); + p1.reset(new storm::solver::TopologicalMinMaxLinearEquationSolver<ValueType>(matrix)); + break; + } + } + p1->setPolicyTracking(trackPolicy); + return p1; + } + std::unique_ptr<storm::solver::LpSolver> LpSolverFactory::create(std::string const& name) const { storm::solver::LpSolverType lpSolver = storm::settings::generalSettings().getLpSolver(); switch (lpSolver) { @@ -134,9 +160,7 @@ namespace storm { template class GmmxxLinearEquationSolverFactory<double>; template class NativeLinearEquationSolverFactory<double>; template class MinMaxLinearEquationSolverFactory<double>; - template class GmmxxMinMaxLinearEquationSolverFactory<double>; - template class NativeMinMaxLinearEquationSolverFactory<double>; - template class TopologicalMinMaxLinearEquationSolverFactory<double>; + } } } \ No newline at end of file diff --git a/src/utility/solver.h b/src/utility/solver.h index 58a7d1018..bcece2fb5 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -7,7 +7,7 @@ #include "src/solver/LinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/storage/dd/DdType.h" -#include "src/utility/ExtendSettingEnumWithSelectionField.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace solver { @@ -80,30 +80,22 @@ namespace storm { template<typename ValueType> class MinMaxLinearEquationSolverFactory { public: + MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solverType = storm::solver::EquationSolverTypeSelection::FROMSETTINGS); /*! * Creates a new nondeterministic linear equation solver instance with the given matrix. */ - virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const; - }; - - template<typename ValueType> - class NativeMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> { - public: - virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override; - }; - - template<typename ValueType> - class GmmxxMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> { - public: - virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override; - }; - - template<typename ValueType> - class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> { - public: - virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override; + virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy = false) const; + void setSolverType(storm::solver::EquationSolverTypeSelection solverType); + void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); + + protected: + /// The type of solver which should be created. + storm::solver::EquationSolverType solverType; + /// The preferred technique to be used by the solver. + /// Notice that we save the selection enum here, which allows different solvers to use different techniques. + storm::solver::MinMaxTechniqueSelection prefTech; }; - + class LpSolverFactory { public: /*! diff --git a/src/utility/cli.h b/src/utility/storm.h similarity index 96% rename from src/utility/cli.h rename to src/utility/storm.h index c28394f6d..35960d474 100644 --- a/src/utility/cli.h +++ b/src/utility/storm.h @@ -1,5 +1,6 @@ -#ifndef STORM_UTILITY_CLI_H_ -#define STORM_UTILITY_CLI_H_ + +#ifndef STORM_H +#define STORM_H #include <iostream> #include <iomanip> @@ -15,8 +16,6 @@ // Headers that provide auxiliary functionality. -#include "src/utility/storm-version.h" -#include "src/utility/OsDetection.h" #include "src/settings/SettingsManager.h" @@ -72,25 +71,9 @@ #include "src/exceptions/NotImplementedException.h" namespace storm { - namespace utility { - namespace cli { - - std::string getCurrentWorkingDirectory(); - - void printHeader(const int argc, const char* argv[]); - - void printUsage(); - - /*! - * Parses the given command line arguments. - * - * @param argc The argc argument of main(). - * @param argv The argv argument of main(). - * @return True iff the program should continue to run after parsing the options. - */ - bool parseOptions(const int argc, const char* argv[]); - - template<typename ValueType> + + + template<typename ValueType> std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>()) { return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : ""); } @@ -411,9 +394,8 @@ namespace storm { } } - void processOptions(); - } - } + } -#endif +#endif /* STORM_H */ + diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index e1808f717..5be1cd015 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -11,6 +11,7 @@ #include "src/parser/FormulaParser.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/settings/SettingsManager.h" @@ -41,7 +42,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); - storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -138,7 +139,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); - storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index c829a94b6..39faff058 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -28,7 +28,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -92,7 +92,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -144,7 +144,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index d0f752f0c..af1e54175 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -40,8 +40,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); - storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); - + storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); @@ -137,7 +136,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(); - storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 14622dae2..61b5bf654 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -27,7 +27,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -91,7 +91,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -113,7 +113,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>(); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -143,7 +143,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(3172ull, mdp->getNumberOfStates()); ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -207,7 +207,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -239,7 +239,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -280,7 +280,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -366,7 +366,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -488,7 +488,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index f741eabc0..e2e563cc6 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -87,7 +87,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // ------------- state rewards -------------- std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = 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", "")->as<storm::models::sparse::Mdp<double>>(); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -112,7 +112,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // -------------------------------- state and transition reward ------------------------ std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = 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")->as<storm::models::sparse::Mdp<double>>(); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -143,7 +143,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index 6c659e7b7..bc6642e7c 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -25,6 +25,35 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) { ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::gmmxxEquationSolverSettings().getPrecision()); } +// TODO add better tests here. +TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTermination) { + storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix<double> A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector<double> x(1); + std::vector<double> b = {0.099, 0.5}; + + double bound = 0.8; + storm::solver::GmmxxMinMaxLinearEquationSolver<double> solver(A); + solver.setEarlyTerminationCondition(std::unique_ptr<storm::solver::AllowEarlyTerminationCondition<double>>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue<double>(storm::storage::BitVector(1, true), bound, true, true))); + ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + bound = 0.6; + solver.setEarlyTerminationCondition(std::unique_ptr<storm::solver::AllowEarlyTerminationCondition<double>>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue<double>(storm::storage::BitVector(1, true), bound, true, true))); + + ASSERT_NO_THROW(solver.solveEquationSystem(false, x, b)); + ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); + +} + TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 9d14e2782..33f70d595 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -24,7 +24,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -82,7 +82,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 2d572d5f1..5bf41d01d 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -25,7 +25,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -83,7 +83,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index 5b63a8ddd..2d0eb8399 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -67,7 +67,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>())); + storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");