From 1086ffc1cc76a53eea4672bdad8eb37d8b945815 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 26 Aug 2015 14:57:42 +0200 Subject: [PATCH 1/2] Added allow early termination for min/max solvers Former-commit-id: eaad511158cef680b1119e97d0d02b09c444a4eb --- src/solver/AllowEarlyTerminationCondition.cpp | 54 ++++++++++++++++ src/solver/AllowEarlyTerminationCondition.h | 54 ++++++++++++++++ .../GmmxxMinMaxLinearEquationSolver.cpp | 4 +- src/solver/MinMaxLinearEquationSolver.cpp | 4 ++ src/solver/MinMaxLinearEquationSolver.h | 9 ++- .../NativeMinMaxLinearEquationSolver.cpp | 4 +- src/solver/SolverSelectionOptions.h | 3 +- src/utility/solver.cpp | 62 +++++++++++++------ src/utility/solver.h | 34 ++++------ .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 4 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 8 +-- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 5 +- .../NativeMdpPrctlModelCheckerTest.cpp | 18 +++--- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 8 +-- .../GmmxxMinMaxLinearEquationSolverTest.cpp | 29 +++++++++ .../GmmxxMdpPrctlModelCheckerTest.cpp | 4 +- .../NativeMdpPrctlModelCheckerTest.cpp | 4 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 4 +- 18 files changed, 238 insertions(+), 74 deletions(-) create mode 100644 src/solver/AllowEarlyTerminationCondition.cpp create mode 100644 src/solver/AllowEarlyTerminationCondition.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 + TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove) : + terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove) + { + // Intentionally left empty. + } + + template + bool TerminateAfterFilteredSumPassesThresholdValue::terminateNow(const std::vector& 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 + TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateIfAbove, bool useMinimum) : + terminationThreshold(threshold), filter(filter), terminateIfAboveThreshold(terminateIfAbove), useMinimumAsExtremum(useMinimum) + { + // Intentionally left empty. + } + + template + bool TerminateAfterFilteredExtremumPassesThresholdValue::terminateNow(const std::vector& 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; + template class TerminateAfterFilteredSumPassesThresholdValue; + + } +} 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 +#include "src/storage/BitVector.h" + + +namespace storm { + namespace solver { + template + class AllowEarlyTerminationCondition { + public: + virtual bool terminateNow(std::vector const& currentValues) const = 0; + }; + + template + class NoEarlyTerminationCondition : public AllowEarlyTerminationCondition { + public: + bool terminateNow(std::vector const& currentValues) const { return false; } + }; + + template + class TerminateAfterFilteredSumPassesThresholdValue : public AllowEarlyTerminationCondition { + public: + TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove); + bool terminateNow(std::vector const& currentValues) const; + + protected: + ValueType terminationThreshold; + storm::storage::BitVector filter; + bool terminateIfAboveThreshold; + }; + + template + class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition{ + public: + TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool terminateAbove, bool useMinimum); + bool terminateNow(std::vector 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 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 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 #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 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()) { // Intentionally left empty. } @@ -101,7 +102,13 @@ namespace storm { */ virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + + void setEarlyTerminationCondition(std::unique_ptr> v) { + earlyTermination = std::move(v); + } + protected: + std::unique_ptr> earlyTermination; storm::storage::SparseMatrix 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 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/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 - std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); - switch (equationSolver) { - case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); - case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); - default: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); - } + MinMaxLinearEquationSolverFactory::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solver) + { + setSolverType(solver); + prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS; } - + template - std::unique_ptr> GmmxxMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); + void MinMaxLinearEquationSolverFactory::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 - std::unique_ptr> NativeMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); - } + void MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { + this->prefTech = preferredTech; + } + template - std::unique_ptr> TopologicalMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - return std::unique_ptr>(new storm::solver::TopologicalMinMaxLinearEquationSolver(matrix)); + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackPolicy) const { + + std::unique_ptr> p1; + + switch (solverType) { + case storm::solver::EquationSolverType::Gmmxx: + { + p1.reset(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix, this->prefTech)); + break; + } + case storm::solver::EquationSolverType::Native: + { + p1.reset(new storm::solver::NativeMinMaxLinearEquationSolver(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(matrix)); + break; + } + } + p1->setPolicyTracking(trackPolicy); + return p1; + } + std::unique_ptr 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; template class NativeLinearEquationSolverFactory; template class MinMaxLinearEquationSolverFactory; - template class GmmxxMinMaxLinearEquationSolverFactory; - template class NativeMinMaxLinearEquationSolverFactory; - template class TopologicalMinMaxLinearEquationSolverFactory; + } } } \ 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 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> create(storm::storage::SparseMatrix const& matrix) const; - }; - - template - class NativeMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - }; - - template - class GmmxxMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; - }; - - template - class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory { - public: - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix 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/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index e1808f717..c148a92d9 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -138,7 +138,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -92,7 +92,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr 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> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); @@ -137,7 +136,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = model->as>(); - storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -91,7 +91,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -113,7 +113,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); - storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); @@ -207,7 +207,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -239,7 +239,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -280,7 +280,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -366,7 +366,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); @@ -488,7 +488,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { mdp.reset(new storm::models::sparse::Mdp(transitionMatrix, ap)); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr 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> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); @@ -87,7 +87,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // ------------- state rewards -------------- std::shared_ptr> 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::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); @@ -112,7 +112,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { // -------------------------------- state and transition reward ------------------------ std::shared_ptr> 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::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(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> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr 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 builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector x(1); + std::vector b = {0.099, 0.5}; + + double bound = 0.8; + storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); + solver.setEarlyTerminationCondition(std::unique_ptr>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue(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>(new storm::solver::TerminateAfterFilteredExtremumPassesThresholdValue(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 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Gmmxx))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr 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> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Topological))); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); From f219437acfb852b993e0dd42b68ba1f71c66a52d Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 26 Aug 2015 16:44:00 +0200 Subject: [PATCH 2/2] Faster compilation times! Former-commit-id: a8dc8fa612af10bb22a9200651e9a1bb466b3c61 --- CMakeLists.txt | 12 +++++-- src/{utility => cli}/cli.cpp | 11 +++--- src/cli/cli.h | 29 +++++++++++++++ .../prctl/HybridMdpPrctlModelChecker.cpp | 1 + .../prctl/HybridMdpPrctlModelChecker.h | 9 +++-- .../SparsePropositionalModelChecker.h | 1 - .../SymbolicPropositionalModelChecker.h | 10 +++++- src/models/ModelBase.h | 1 - src/models/sparse/Dtmc.h | 1 - src/models/sparse/Model.h | 5 ++- src/models/symbolic/Model.cpp | 1 + ...erministicModelBisimulationDecomposition.h | 1 + src/storm.cpp | 10 +++--- src/utility/{cli.h => storm.h} | 36 +++++-------------- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 1 + 15 files changed, 82 insertions(+), 47 deletions(-) rename src/{utility => cli}/cli.cpp (98%) create mode 100644 src/cli/cli.h rename src/utility/{cli.h => storm.h} (96%) 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 219e566ae..6198db9f3 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 + +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 class Mdp; + } + } + namespace modelchecker { template class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { 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 class Model; + } + } + namespace modelchecker { + template 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 #include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/InvalidOperationException.h" #include "src/adapters/AddExpressionAdapter.h" 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/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 #include @@ -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 + + + template std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional()) { 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 c148a92d9..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"