From 5a1039838f1d36c41c25085cf1c35c528c274661 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 14 Feb 2016 16:32:38 +0100 Subject: [PATCH] made everything compile again and all tests passing Former-commit-id: 65c66fb58fce0a6947ea7bf2b15eb980f42ee86c --- .../MILPMinimalLabelSetGenerator.h | 4 +- src/logic/Bound.h | 3 +- src/parser/FormulaParser.cpp | 37 ++++++++++++------- src/solver/AbstractEquationSolver.h | 2 +- src/solver/GmmxxLinearEquationSolver.cpp | 2 +- .../GmmxxMinMaxLinearEquationSolver.cpp | 19 ++++++---- src/solver/MinMaxLinearEquationSolver.cpp | 36 ++++++++++++++---- src/solver/MinMaxLinearEquationSolver.h | 21 ++++------- src/solver/NativeLinearEquationSolver.cpp | 4 +- .../NativeMinMaxLinearEquationSolver.cpp | 20 ++++++---- src/solver/SolveGoal.cpp | 5 +-- src/solver/SolveGoal.h | 6 ++- src/solver/TerminationCondition.cpp | 6 +-- src/solver/TerminationCondition.h | 2 - src/storage/TotalScheduler.cpp | 4 ++ src/storage/TotalScheduler.h | 9 ++++- src/utility/solver.cpp | 5 +-- src/utility/solver.h | 2 +- .../GmmxxMinMaxLinearEquationSolverTest.cpp | 6 +-- test/functional/utility/VectorTest.cpp | 8 ++-- 20 files changed, 123 insertions(+), 78 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index e2255721c..87f02c668 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -985,7 +985,7 @@ namespace storm { STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); bool strictBound = comparisonType == storm::logic::ComparisonType::Less; - double bound = probabilityOperator.getBound(); + double threshold = probabilityOperator.getThreshold(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; @@ -1015,7 +1015,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet()); + boost::container::flat_set usedLabelSet = getMinimalLabelSet(probabilityOperator.getSubformula(), labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::counterexampleGeneratorSettings().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/logic/Bound.h b/src/logic/Bound.h index 58f8b5448..d0a98853c 100644 --- a/src/logic/Bound.h +++ b/src/logic/Bound.h @@ -14,7 +14,8 @@ namespace storm { ComparisonType comparisonType; ValueType threshold; - friend std::ostream& operator<<(std::ostream& out, Bound const& bound); + template + friend std::ostream& operator<<(std::ostream& out, Bound const& bound); }; template diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index e3c0c9718..c919280b4 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -97,7 +97,7 @@ namespace storm { qi::rule>(), Skipper> start; - qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule, boost::optional>>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule(), Skipper> probabilityOperator; qi::rule(), Skipper> rewardOperator; qi::rule(), Skipper> expectedTimeOperator; @@ -149,10 +149,11 @@ namespace storm { std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::pair, boost::optional>> createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; + std::shared_ptr createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); @@ -305,7 +306,7 @@ namespace storm { pathFormula = conditionalFormula; pathFormula.name("path formula"); - operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; + operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -469,20 +470,28 @@ namespace storm { return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::pair, boost::optional>> FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { + if (comparisonType && threshold) { + return std::make_pair(optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get())); + } else { + return std::make_pair(optimizationDirection, boost::none); + } + } + + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); } - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, operatorInformation.first, operatorInformation.second, subformula)); } - std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); } - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(operatorInformation.first, operatorInformation.second, subformula)); } std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { diff --git a/src/solver/AbstractEquationSolver.h b/src/solver/AbstractEquationSolver.h index e110318f6..904e459bd 100644 --- a/src/solver/AbstractEquationSolver.h +++ b/src/solver/AbstractEquationSolver.h @@ -29,7 +29,7 @@ namespace storm { /*! * Retrieves whether a custom termination condition has been set. */ - bool hasCustomTerminationCondition() { + bool hasCustomTerminationCondition() const { return static_cast(this->terminationCondition); } diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index ad5729774..3b7bbf476 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -171,7 +171,7 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations) { + while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute D^-1 * (b - LU * x) and store result in nextX. gmm::mult(*gmmLU, *currentX, tmpX); gmm::add(b, gmm::scaled(tmpX, -storm::utility::one()), tmpX); diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index e24019e79..d5dcbb627 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -5,6 +5,7 @@ #include "src/settings/SettingsManager.h" #include "src/adapters/GmmxxAdapter.h" #include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/storage/TotalScheduler.h" #include "src/utility/vector.h" #include "src/settings/modules/GeneralSettings.h" @@ -53,7 +54,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 && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); @@ -92,7 +93,7 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); + std::vector scheduler(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(rowGroupIndices.size() - 1); @@ -119,13 +120,13 @@ 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 && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::Ilu, this->relative, 50); - storm::utility::vector::selectVectorValues(subB, this->policy, rowGroupIndices, b); + storm::utility::vector::selectVectorValues(subB, scheduler, rowGroupIndices, b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -139,8 +140,7 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(this->policy)); - + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(scheduler)); // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -156,6 +156,11 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + this->scheduler = std::make_unique(std::move(scheduler)); + } // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index f0c2e4869..4f9627a20 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -8,9 +8,8 @@ namespace storm { namespace solver { - AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : - precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackPolicy(trackPolicy) - { + template + AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackScheduler(trackScheduler) { if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) { useValueIteration = (storm::settings::generalSettings().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); @@ -19,13 +18,34 @@ namespace storm { } } - void AbstractMinMaxLinearEquationSolver::setPolicyTracking(bool setToTrue) { - trackPolicy = setToTrue; + template + void AbstractMinMaxLinearEquationSolver::setTrackScheduler(bool trackScheduler) { + this->trackScheduler = trackScheduler; } - std::vector AbstractMinMaxLinearEquationSolver::getPolicy() const { - STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); - return policy; + template + bool AbstractMinMaxLinearEquationSolver::isTrackSchedulerSet() const { + return this->trackScheduler; } + + template + storm::storage::Scheduler const& AbstractMinMaxLinearEquationSolver::getScheduler() const { + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return *scheduler.get(); + } + + template + void AbstractMinMaxLinearEquationSolver::setOptimizationDirection(OptimizationDirection d) { + direction = convert(d); + } + + template + void AbstractMinMaxLinearEquationSolver::resetOptimizationDirection() { + direction = OptimizationDirectionSetting::Unset; + } + + template class AbstractMinMaxLinearEquationSolver; + template class AbstractMinMaxLinearEquationSolver; + } } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 42963ac29..f33fdc6e1 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -5,6 +5,8 @@ #include #include +#include + #include "src/solver/AbstractEquationSolver.h" #include "src/solver/SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" @@ -26,20 +28,13 @@ namespace storm { template class AbstractMinMaxLinearEquationSolver : public AbstractEquationSolver { public: - void setSchedulerTracking(bool trackScheduler = true); + void setTrackScheduler(bool trackScheduler = true); + bool isTrackSchedulerSet() const; - std::vector getScheduler() const { - STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); - return scheduler.get(); - } + storm::storage::Scheduler const& getScheduler() const; - void setOptimizationDirection(OptimizationDirection d) { - direction = convert(d); - } - - void resetOptimizationDirection() { - direction = OptimizationDirectionSetting::Unset; - } + void setOptimizationDirection(OptimizationDirection d); + void resetOptimizationDirection(); protected: AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech); @@ -63,7 +58,7 @@ namespace storm { bool trackScheduler; // The scheduler (if it could be successfully generated). - boost::optional> scheduler; + mutable boost::optional> scheduler; }; /*! diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 414ff1a5e..cb59a2253 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -51,7 +51,7 @@ namespace storm { A.performSuccessiveOverRelaxationStep(omega, x, b); // Now check if the process already converged within our precision. - converged = storm::utility::vector::equalModuloPrecision(x, *tmpX, static_cast(precision), relative); + converged = storm::utility::vector::equalModuloPrecision(x, *tmpX, static_cast(precision), relative) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); // If we did not yet converge, we need to copy the contents of x to *tmpX. if (!converged) { @@ -87,7 +87,7 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < maximalNumberOfIterations) { + while (!converged && iterationCount < maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Compute D^-1 * (b - LU * x) and store result in nextX. jacobiDecomposition.first.multiplyWithVector(*currentX, tmpX); storm::utility::vector::subtractVectors(b, tmpX, tmpX); diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 1a0881402..629385e8f 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -2,7 +2,7 @@ #include - +#include "src/storage/TotalScheduler.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/NativeEquationSolverSettings.h" @@ -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 && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && (!this->hasCustomTerminationCondition() || this->getTerminationCondition().terminateNow(*currentX))) { // Compute x' = A*x + b. this->A.multiplyWithVector(*currentX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); @@ -93,7 +93,7 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); + std::vector scheduler(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1); @@ -121,13 +121,13 @@ 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 && !this->earlyTermination->terminateNow(*currentX)) { + while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); NativeLinearEquationSolver nativeLinearEquationSolver(submatrix); - storm::utility::vector::selectVectorValues(subB, this->policy, this->A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -141,7 +141,7 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy)); + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(scheduler)); // Determine whether the method converged. @@ -158,8 +158,12 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } - + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + this->scheduler = std::make_unique(std::move(scheduler)); + } + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. if (currentX == copyX) { diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index b135fba59..642077c05 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -17,7 +17,7 @@ namespace storm { std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { std::unique_ptr> p = factory.create(matrix); p->setOptimizationDirection(goal.direction()); - p->setTerminationCondition(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); + p->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); return p; } @@ -34,8 +34,7 @@ namespace storm { template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { std::unique_ptr> solver = factory.create(matrix); - solver->setOptimizationDirection(goal.direction()); - solver->setTerminationCondition(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); + solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.thresholdValue(), goal.boundIsStrict(), goal.minimize())); return solver; } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index b87fa0837..fb28dfbb3 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -77,12 +77,16 @@ namespace storm { return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::GreaterEqual); } + bool boundIsStrict() const { + return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::Less); + } + ValueType const& thresholdValue() const { return bound.threshold; } storm::storage::BitVector const& relevantValues() const { - return relevantValues; + return relevantValueVector; } private: diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp index 98434e407..f640ac7e0 100644 --- a/src/solver/TerminationCondition.cpp +++ b/src/solver/TerminationCondition.cpp @@ -29,9 +29,9 @@ namespace storm { } template - bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(const std::vector& currentValues) const { - STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch."); - ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, filter) : storm::utility::vector::max_if(currentValues, filter); + bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + STORM_LOG_ASSERT(currentValues.size() == this->filter.size(), "Vectors sizes mismatch."); + ValueType currentValue = useMinimum ? storm::utility::vector::min_if(currentValues, this->filter) : storm::utility::vector::max_if(currentValues, this->filter); return this->strict ? currentValue > this->threshold : currentValue >= this->threshold; } diff --git a/src/solver/TerminationCondition.h b/src/solver/TerminationCondition.h index 4ea5f5c3d..42437bc68 100644 --- a/src/solver/TerminationCondition.h +++ b/src/solver/TerminationCondition.h @@ -38,8 +38,6 @@ namespace storm { bool terminateNow(std::vector const& currentValue) const; protected: - ValueType threshold; - storm::storage::BitVector filter; bool useMinimum; }; } diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp index ae609a4f4..6ae99d212 100644 --- a/src/storage/TotalScheduler.cpp +++ b/src/storage/TotalScheduler.cpp @@ -11,6 +11,10 @@ namespace storm { // Intentionally left empty. } + TotalScheduler::TotalScheduler(std::vector&& choices) : choices(std::move(choices)) { + // Intentionally left empty. + } + void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { if (state > choices.size()) { throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::setChoice: scheduler cannot not define a choice for state " << state << "."; diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h index 32173ac63..6f95edf71 100644 --- a/src/storage/TotalScheduler.h +++ b/src/storage/TotalScheduler.h @@ -25,7 +25,14 @@ namespace storm { * @param choices A vector whose i-th entry defines the choice of state i. */ TotalScheduler(std::vector const& choices); - + + /*! + * Creates a total scheduler that defines the choices for states according to the given vector. + * + * @param choices A vector whose i-th entry defines the choice of state i. + */ + TotalScheduler(std::vector&& choices); + void setChoice(uint_fast64_t state, uint_fast64_t choice) override; bool isChoiceDefined(uint_fast64_t state) const override; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 42195cde3..dbb798cb2 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -105,8 +105,7 @@ namespace storm { } template - std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackPolicy) const { - + std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackScheduler) const { std::unique_ptr> p1; switch (solverType) { @@ -127,7 +126,7 @@ namespace storm { break; } } - p1->setPolicyTracking(trackPolicy); + p1->setTrackScheduler(trackScheduler); return p1; } diff --git a/src/utility/solver.h b/src/utility/solver.h index cf2c63663..446b22c7a 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -113,7 +113,7 @@ namespace storm { /*! * Creates a new min/max linear equation solver instance with the given matrix. */ - virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackPolicy = false) const; + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackScheduler = false) const; void setSolverType(storm::solver::EquationSolverTypeSelection solverType); void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index ff91e660a..1839b1016 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -39,7 +39,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio double bound = 0.8; storm::solver::GmmxxMinMaxLinearEquationSolver solver(A); - solver.setEarlyTerminationCriterion(std::make_unique>(storm::storage::BitVector(1, true), bound, true)); + + solver.setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true)); ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Minimize, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -47,11 +48,10 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); bound = 0.6; - solver.setEarlyTerminationCriterion(std::make_unique>(storm::storage::BitVector(1, true), bound, true)); + solver.setTerminationCondition(std::make_unique>(storm::storage::BitVector(A.getRowGroupCount(), true), bound, false, true)); ASSERT_NO_THROW(solver.solveEquationSystem(storm::OptimizationDirection::Maximize, x, b)); ASSERT_LT(std::abs(x[0] - 0.989991), 0.989991 - bound - storm::settings::gmmxxEquationSolverSettings().getPrecision()); - } TEST(GmmxxMinMaxLinearEquationSolver, MatrixVectorMultiplication) { diff --git a/test/functional/utility/VectorTest.cpp b/test/functional/utility/VectorTest.cpp index 9494d6146..0cef4cd9c 100644 --- a/test/functional/utility/VectorTest.cpp +++ b/test/functional/utility/VectorTest.cpp @@ -18,8 +18,8 @@ TEST(VectorTest, max_if) { storm::storage::BitVector f1(5, {2,4}); storm::storage::BitVector f2(5, {3,4}); - ASSERT_EQ(34.0, storm::utility::vector::max_if(a,f1,0.0)); - ASSERT_EQ(16.0, storm::utility::vector::max_if(a,f2,0.0)); + ASSERT_EQ(34.0, storm::utility::vector::max_if(a, f1)); + ASSERT_EQ(16.0, storm::utility::vector::max_if(a, f2)); } @@ -28,6 +28,6 @@ TEST(VectorTest, min_if) { storm::storage::BitVector f1(5, {2,4}); storm::storage::BitVector f2(5, {3,4}); - ASSERT_EQ(16.0, storm::utility::vector::min_if(a,f1,100.0)); - ASSERT_EQ(8.0, storm::utility::vector::min_if(a,f2,100.0)); + ASSERT_EQ(16.0, storm::utility::vector::min_if(a, f1)); + ASSERT_EQ(8.0, storm::utility::vector::min_if(a, f2)); }