From dee44056d19819763dea474ed6f5924563e53f7f Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Feb 2016 19:07:46 +0100 Subject: [PATCH 1/8] work towards generating schedulers (and some other related stuff) Former-commit-id: 23cbcb5fb566784da77aacdd4e180afe775495d8 --- .../MILPMinimalLabelSetGenerator.h | 3 +- .../SMTMinimalCommandSetGenerator.h | 4 +- src/modelchecker/CheckTask.h | 18 ++-- .../helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 4 +- .../helper/MDPModelCheckingHelperReturnType.h | 25 +++-- .../prctl/helper/SparseMdpPrctlHelper.cpp | 18 ++-- .../prctl/helper/SparseMdpPrctlHelper.h | 4 +- src/solver/LinearEquationSolver.h | 9 +- src/solver/MinMaxLinearEquationSolver.h | 39 ++++---- src/solver/SolveGoal.cpp | 46 ++++++--- src/solver/SolveGoal.h | 94 +++++++++++++------ 12 files changed, 163 insertions(+), 103 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 17825b23d..e2255721c 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -923,7 +923,6 @@ namespace storm { } public: - static boost::container::flat_set getMinimalLabelSet(storm::logic::Formula const& pathFormula, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { @@ -934,7 +933,7 @@ namespace storm { double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { storm::modelchecker::helper::SparseMdpPrctlHelper modelcheckerHelper; - std::vector result = std::move(modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).result); + std::vector result = std::move(modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).values); for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 7c85f7644..3026ab74e 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1628,7 +1628,7 @@ namespace storm { if (checkThresholdFeasible) { storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).result); + std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).values); for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -1692,7 +1692,7 @@ namespace storm { storm::models::sparse::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).result); + std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()).values); LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index cf66f4f06..959c8f96a 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -30,7 +30,7 @@ namespace storm { */ CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; - this->produceStrategies = true; + this->produceSchedulers = true; this->qualitative = false; if (formula.isOperatorFormula()) { @@ -76,7 +76,7 @@ namespace storm { */ template CheckTask replaceFormula(NewFormulaType const& newFormula) const { - return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceStrategies); + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers); } /*! @@ -166,10 +166,10 @@ namespace storm { } /*! - * Retrieves whether strategies are to be produced (if supported). + * Retrieves whether scheduler(s) are to be produced (if supported). */ - bool isProduceStrategiesSet() const { - return produceStrategies; + bool isProduceSchedulersSet() const { + return produceSchedulers; } private: @@ -185,10 +185,10 @@ namespace storm { * together with the flag that indicates only initial states of the model are relevant. * @param qualitative A flag specifying whether the property needs to be checked qualitatively, i.e. compared * with bounds 0/1. - * @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve + * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceStrategies) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceStrategies(produceStrategies) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { // Intentionally left empty. } @@ -210,9 +210,9 @@ namespace storm { // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; - // If supported by the model checker and the model formalism, strategies to achieve a value will be produced + // If supported by the model checker and the model formalism, schedulers to achieve a value will be produced // if this flag is set. - bool produceStrategies; + bool produceSchedulers; }; } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index fac6e5864..d926917a5 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -184,7 +184,7 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { - return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result); + return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values); } template diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index eb4025551..b13906151 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -87,8 +87,8 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), false, *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.values))); } template diff --git a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index a68a5889e..fac823940 100644 --- a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -12,33 +12,30 @@ namespace storm { namespace modelchecker { - - namespace helper { template struct MDPSparseModelCheckingHelperReturnType { + MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; - explicit MDPSparseModelCheckingHelperReturnType(std::vector && res) : result(std::move(res)) - { - + MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr && scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { + // Intentionally left empty. } - MDPSparseModelCheckingHelperReturnType(std::vector && res, std::unique_ptr && pSched) : - result(std::move(res)), partScheduler(std::move(pSched)) {} - - virtual ~MDPSparseModelCheckingHelperReturnType() { } + virtual ~MDPSparseModelCheckingHelperReturnType() { + // Intentionally left empty. + } + // The values computed for the states. + std::vector values; - std::vector result; - std::unique_ptr partScheduler; + // A scheduler, if it was computed. + std::unique_ptr scheduler; }; } - + } } - #endif /* MDPMODELCHECKINGRETURNTYPE_H */ - diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 2f4d9389d..85817b1b2 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -73,7 +73,7 @@ namespace storm { template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. @@ -128,17 +128,15 @@ namespace storm { return MDPSparseModelCheckingHelperReturnType(std::move(result)); } - template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { storm::solver::SolveGoal goal(dir); - return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, getPolicy, minMaxLinearEquationSolverFactory)); + return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, producePolicy, minMaxLinearEquationSolverFactory)); } template std::vector SparseMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique) { - if (useMecBasedTechnique) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, psiStates); storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount()); @@ -148,9 +146,9 @@ namespace storm { } } - return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).result); + return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).values); } else { - std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result; + std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values; for (auto& element : result) { element = storm::utility::one() - element; } @@ -519,14 +517,14 @@ namespace storm { initialStatesBitVector.set(initialState); storm::storage::BitVector allStates(initialStatesBitVector.size(), true); - std::vector conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, conditionStates, false, false, minMaxLinearEquationSolverFactory).result); + std::vector conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, conditionStates, false, false, minMaxLinearEquationSolverFactory).values); // If the conditional probability is undefined for the initial state, we return directly. if (storm::utility::isZero(conditionProbabilities[initialState])) { return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, storm::utility::infinity())); } - std::vector targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).result); + std::vector targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false, minMaxLinearEquationSolverFactory).values); storm::storage::BitVector statesWithProbabilityGreater0E(transitionMatrix.getRowGroupCount(), true); storm::storage::sparse::state_type state = 0; @@ -594,7 +592,7 @@ namespace storm { newGoalStates.set(newGoalState); storm::storage::SparseMatrix newTransitionMatrix = builder.build(); storm::storage::SparseMatrix newBackwardTransitions = newTransitionMatrix.transpose(true); - std::vector goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).result); + std::vector goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values); return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, dir == OptimizationDirection::Maximize ? goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]] : storm::utility::one() - goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]])); } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 706f61403..8567c445b 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -36,9 +36,9 @@ namespace storm { static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 61f26294e..512cefbdb 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -4,6 +4,7 @@ #include #include "src/storage/SparseMatrix.h" +#include "src/solver/AllowEarlyTerminationCondition.h" namespace storm { namespace solver { @@ -15,7 +16,6 @@ namespace storm { template class LinearEquationSolver { public: - virtual ~LinearEquationSolver() { // Intentionally left empty. } @@ -45,6 +45,13 @@ namespace storm { * vector must be equal to the number of rows of A. */ virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + + void setEarlyTerminationCriterion(std::unique_ptr> v) { + earlyTermination = std::move(v); + } + + // A termination criterion to be used (can be unset). + std::unique_ptr> earlyTermination; }; } // namespace solver diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 79d14907b..cf334c6ee 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -6,8 +6,8 @@ #include #include "SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" -#include "AllowEarlyTerminationCondition.h" -#include "OptimizationDirection.h" +#include "src/solver/AllowEarlyTerminationCondition.h" +#include "src/solver/OptimizationDirection.h" namespace storm { namespace storage { @@ -15,17 +15,18 @@ namespace storm { } namespace solver { - /** * Abstract base class which provides value-type independent helpers. */ class AbstractMinMaxLinearEquationSolver { - public: - void setPolicyTracking(bool setToTrue=true); + void setSchedulerTracking(bool trackScheduler = true); - std::vector getPolicy() const; + std::vector getScheduler() const { + STORM_LOG_THROW(scheduler, storm::exceptions::Invali, "Cannot retrieve scheduler, because none was generated."); + reutrn scheduler.get(); + } void setOptimizationDirection(OptimizationDirection d) { direction = convert(d); @@ -35,14 +36,16 @@ namespace storm { direction = OptimizationDirectionSetting::Unset; } + void setEarlyTerminationCriterion(std::unique_ptr> v) { + earlyTermination = std::move(v); + } protected: - AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech); + AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech); /// The direction in which to optimize, can be unset. OptimizationDirectionSetting direction; - /// The required precision for the iterative methods. double precision; @@ -55,11 +58,14 @@ namespace storm { /// Whether value iteration or policy iteration is to be used. bool useValueIteration; - /// Whether we track the policy we generate. - bool trackPolicy; + /// Whether we generate a scheduler during solving. + bool trackScheduler; - /// - mutable std::vector policy; + /// The scheduler (if it could be successfully generated). + boost::optional scheduler; + + // A termination criterion to be used (can be unset). + std::unique_ptr> earlyTermination; }; /*! @@ -77,7 +83,6 @@ namespace storm { } public: - virtual ~MinMaxLinearEquationSolver() { // Intentionally left empty. } @@ -107,6 +112,7 @@ namespace storm { assert(isSet(this->direction)); solveEquationSystem(convert(this->direction), x, b, multiplyResult, newX); } + /*! * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes * x[i+1] = min/max(A*x[i] + b) until x[n], where x[0] = x. After each multiplication and addition, the @@ -134,15 +140,8 @@ namespace storm { return performMatrixVectorMultiplication(convert(this->direction), x, b, n, multiplyResult); } - void setEarlyTerminationCriterion(std::unique_ptr> v) { - earlyTermination = std::move(v); - } - - protected: storm::storage::SparseMatrix const& A; - std::unique_ptr> earlyTermination; - }; } // namespace solver diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index f6d109569..4994f8ade 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -1,36 +1,56 @@ #include "SolveGoal.h" +#include + #include "src/utility/solver.h" +#include "src/solver/LinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" -#include namespace storm { namespace storage { - template class SparseMatrix; + template class SparseMatrix; } namespace solver { - template - 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); + template + 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->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.threshold, goal.minimize())); + p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); return p; } - template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - if(goal.isBounded()) { - return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + if (goal.isBounded()) { + return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); } - std::unique_ptr> p = factory.create(matrix); + std::unique_ptr> p = factory.create(matrix); + p->setOptimizationDirection(goal.direction()); + return p; + } + + template + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> p = factory.create(matrix); p->setOptimizationDirection(goal.direction()); + p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); return p; - } + } + + template + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + if (goal.isBounded()) { + return configureLinearEquationSolver(static_cast const&>(goal), factory, matrix); + } + return factory.create(matrix); + } - template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); } } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index fe573dd3a..7a8f9c661 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -10,59 +10,99 @@ namespace storm { namespace storage { - template class SparseMatrix; + template class SparseMatrix; } + namespace utility { namespace solver { - template class MinMaxLinearEquationSolverFactory; + template class MinMaxLinearEquationSolverFactory; + template class LinearEquationSolverFactory; } } - namespace solver { - template class MinMaxLinearEquationSolver; + template class MinMaxLinearEquationSolver; + template class LinearEquationSolver; class SolveGoal { public: - SolveGoal(bool minimize) : optDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) {} - SolveGoal(OptimizationDirection d) : optDirection(d) {} - virtual ~SolveGoal() {} + SolveGoal(bool minimize) : optimizationDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) { + // Intentionally left empty. + } + + SolveGoal(OptimizationDirection d) : optimizationDirection(d) { + // Intentionally left empty. + } + + virtual ~SolveGoal() { + // Intentionally left empty. + } - bool minimize() const { return optDirection == OptimizationDirection::Minimize; } - OptimizationDirection direction() const { return optDirection; } - virtual bool isBounded() const { return false; } + bool minimize() const { + return optimizationDirection == OptimizationDirection::Minimize; + } + + OptimizationDirection direction() const { + return optimizationDirection; + } + + virtual bool isBounded() const { + return false; + } private: - OptimizationDirection optDirection; - + OptimizationDirection optimizationDirection; }; - - template + template class BoundedGoal : public SolveGoal { public: - BoundedGoal(OptimizationDirection dir, storm::logic::ComparisonType ct, VT const& threshold, storm::storage::BitVector const& relColumns) : SolveGoal(dir), boundType(ct), threshold(threshold), relevantColumnVector(relColumns) {} - BoundedGoal(OptimizationDirection dir, storm::logic::BoundInfo const& bi, storm::storage::BitVector const& relColumns) : SolveGoal(dir), boundType(bi.boundType), threshold(bi.bound), relevantColumnVector(relColumns) {} - virtual ~BoundedGoal() {} + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType ct, ValueType const& threshold, storm::storage::BitVector const& relColumns) : SolveGoal(optimizationDirection), boundType(ct), threshold(threshold), relevantColumnVector(relColumns) { + // Intentionally left empty. + } - bool isBounded() const override { return true; } + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::BoundInfo const& boundInfo, storm::storage::BitVector const& relevantColumns) : SolveGoal(optimizationDirection), boundType(boundInfo.boundType), threshold(boundInfo.bound), relevantColumnVector(relevantColumns) { + // Intentionally left empty. + } + + virtual ~BoundedGoal() { + // Intentionally left empty. + } + + bool isBounded() const override { + return true; + } bool boundIsALowerBound() const { - return (boundType == storm::logic::ComparisonType::Greater | - boundType == storm::logic::ComparisonType::GreaterEqual); + return (boundType == storm::logic::ComparisonType::Greater || boundType == storm::logic::ComparisonType::GreaterEqual); + } + + ValueType const& thresholdValue() const { + return threshold; } - VT thresholdValue() const { return threshold; } - storm::storage::BitVector relevantColumns() const { return relevantColumnVector; } + storm::storage::BitVector const& relevantColumns() const { + return relevantColumnVector; + } + + private: storm::logic::ComparisonType boundType; - VT threshold; + ValueType threshold; storm::storage::BitVector relevantColumnVector; }; - template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + } } From bdcd4b26a3013b9916a653f4e7b40c48d783aa52 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Feb 2016 17:28:59 +0100 Subject: [PATCH 2/8] refactoring early termination and solve goals and bounds Former-commit-id: 123835f655dc4a20b38ecf65e6b0b0bce0adba48 --- src/logic/Bound.h | 32 +++++++++ src/logic/BoundInfo.h | 19 ----- src/logic/ExpectedTimeOperatorFormula.cpp | 12 ++-- src/logic/ExpectedTimeOperatorFormula.h | 6 +- src/logic/LongRunAverageOperatorFormula.cpp | 12 ++-- src/logic/LongRunAverageOperatorFormula.h | 6 +- src/logic/OperatorFormula.cpp | 24 ++++--- src/logic/OperatorFormula.h | 19 ++--- src/logic/ProbabilityOperatorFormula.cpp | 12 ++-- src/logic/ProbabilityOperatorFormula.h | 6 +- src/logic/RewardOperatorFormula.cpp | 12 ++-- src/logic/RewardOperatorFormula.h | 6 +- src/modelchecker/AbstractModelChecker.cpp | 8 +-- src/modelchecker/CheckTask.h | 25 ++++--- .../prctl/SparseMdpPrctlModelChecker.h | 2 - src/solver/AbstractEquationSolver.h | 53 ++++++++++++++ src/solver/AllowEarlyTerminationCondition.cpp | 48 ------------- src/solver/AllowEarlyTerminationCondition.h | 52 -------------- src/solver/LinearEquationSolver.h | 18 ++--- src/solver/MinMaxLinearEquationSolver.h | 48 ++++++------- src/solver/SolveGoal.cpp | 24 +++---- src/solver/SolveGoal.h | 19 +++-- src/solver/TerminationCondition.cpp | 41 +++++++++++ src/solver/TerminationCondition.h | 53 ++++++++++++++ src/utility/vector.h | 71 +++++++++++-------- 25 files changed, 346 insertions(+), 282 deletions(-) create mode 100644 src/logic/Bound.h delete mode 100644 src/logic/BoundInfo.h create mode 100644 src/solver/AbstractEquationSolver.h delete mode 100644 src/solver/AllowEarlyTerminationCondition.cpp delete mode 100644 src/solver/AllowEarlyTerminationCondition.h create mode 100644 src/solver/TerminationCondition.cpp create mode 100644 src/solver/TerminationCondition.h diff --git a/src/logic/Bound.h b/src/logic/Bound.h new file mode 100644 index 000000000..58f8b5448 --- /dev/null +++ b/src/logic/Bound.h @@ -0,0 +1,32 @@ +#ifndef STORM_LOGIC_BOUND_H_ +#define STORM_LOGIC_BOUND_H_ + +#include "src/logic/ComparisonType.h" + +namespace storm { + namespace logic { + template + struct Bound { + Bound(ComparisonType comparisonType, ValueType const& threshold) : comparisonType(comparisonType), threshold(threshold) { + // Intentionally left empty. + } + + ComparisonType comparisonType; + ValueType threshold; + + friend std::ostream& operator<<(std::ostream& out, Bound const& bound); + }; + + template + std::ostream& operator<<(std::ostream& out, Bound const& bound) { + out << bound.comparisonType << bound.threshold; + return out; + } + } + + template + using Bound = typename logic::Bound; +} + +#endif /* STORM_LOGIC_BOUND_H_ */ + diff --git a/src/logic/BoundInfo.h b/src/logic/BoundInfo.h deleted file mode 100644 index 453d9eb08..000000000 --- a/src/logic/BoundInfo.h +++ /dev/null @@ -1,19 +0,0 @@ - -#ifndef BOUNDINFO_H -#define BOUNDINFO_H - -#include "ComparisonType.h" - - -namespace storm { - namespace logic { - template - struct BoundInfo { - BT bound; - ComparisonType boundType; - }; - } -} - -#endif /* BOUNDINFO_H */ - diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp index 98ed6d8cc..ed21be228 100644 --- a/src/logic/ExpectedTimeOperatorFormula.cpp +++ b/src/logic/ExpectedTimeOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ExpectedTimeOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -34,12 +34,12 @@ namespace storm { return this->getSubformula().containsNestedProbabilityOperators(); } - ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr ExpectedTimeOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h index b9b6d57ee..5702610c2 100644 --- a/src/logic/ExpectedTimeOperatorFormula.h +++ b/src/logic/ExpectedTimeOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class ExpectedTimeOperatorFormula : public OperatorFormula { public: ExpectedTimeOperatorFormula(std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); ExpectedTimeOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ExpectedTimeOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~ExpectedTimeOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp index d72317b7d..cfeb30692 100644 --- a/src/logic/LongRunAverageOperatorFormula.cpp +++ b/src/logic/LongRunAverageOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : LongRunAverageOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -34,12 +34,12 @@ namespace storm { return this->getSubformula().containsNestedProbabilityOperators(); } - LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr LongRunAverageOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h index 161823314..89e119f48 100644 --- a/src/logic/LongRunAverageOperatorFormula.h +++ b/src/logic/LongRunAverageOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class LongRunAverageOperatorFormula : public OperatorFormula { public: LongRunAverageOperatorFormula(std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); LongRunAverageOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + LongRunAverageOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~LongRunAverageOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 768b6b3d0..a9cdc09ae 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), comparisonType(comparisonType), bound(bound), optimalityType(optimalityType) { + OperatorFormula::OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : UnaryStateFormula(subformula), bound(bound), optimalityType(optimalityType) { // Intentionally left empty. } @@ -11,19 +11,27 @@ namespace storm { } ComparisonType OperatorFormula::getComparisonType() const { - return comparisonType.get(); + return bound.get().comparisonType; } - void OperatorFormula::setComparisonType(ComparisonType t) { - comparisonType = boost::optional(t); + void OperatorFormula::setComparisonType(ComparisonType newComparisonType) { + bound.get().comparisonType = newComparisonType; } - double OperatorFormula::getBound() const { + double OperatorFormula::getThreshold() const { + return bound.get().threshold; + } + + void OperatorFormula::setThreshold(double newThreshold) { + bound.get().threshold = newThreshold; + } + + Bound const& OperatorFormula::getBound() const { return bound.get(); } - void OperatorFormula::setBound(double b) { - bound = boost::optional(b); + void OperatorFormula::setBound(Bound const& newBound) { + bound = newBound; } bool OperatorFormula::hasOptimalityType() const { @@ -43,7 +51,7 @@ namespace storm { out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); } if (hasBound()) { - out << getComparisonType() << getBound(); + out << getBound(); } else { out << "=?"; } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index 5c120bf2f..7660799a4 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -4,14 +4,14 @@ #include #include "src/logic/UnaryStateFormula.h" +#include "src/logic/Bound.h" #include "src/solver/OptimizationDirection.h" -#include "src/logic/ComparisonType.h" namespace storm { namespace logic { class OperatorFormula : public UnaryStateFormula { public: - OperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + OperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~OperatorFormula() { // Intentionally left empty. @@ -19,20 +19,21 @@ namespace storm { bool hasBound() const; ComparisonType getComparisonType() const; - void setComparisonType(ComparisonType); - double getBound() const; - void setBound(double); + void setComparisonType(ComparisonType newComparisonType); + double getThreshold() const; + void setThreshold(double newThreshold); + Bound const& getBound() const; + void setBound(Bound const& newBound); bool hasOptimalityType() const; - OptimizationDirection const& getOptimalityType() const; + storm::solver::OptimizationDirection const& getOptimalityType() const; virtual bool isOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; protected: std::string operatorSymbol; - boost::optional comparisonType; - boost::optional bound; - boost::optional optimalityType; + boost::optional> bound; + boost::optional optimalityType; }; } } diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp index e6cde140d..1f4615556 100644 --- a/src/logic/ProbabilityOperatorFormula.cpp +++ b/src/logic/ProbabilityOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::none, bound, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula) : ProbabilityOperatorFormula(boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -42,12 +42,12 @@ namespace storm { return this->getSubformula().containsProbabilityOperator(); } - ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) { + ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula) { // Intentionally left empty. } std::shared_ptr ProbabilityOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h index 7f30dd92d..8bae11548 100644 --- a/src/logic/ProbabilityOperatorFormula.h +++ b/src/logic/ProbabilityOperatorFormula.h @@ -8,10 +8,10 @@ namespace storm { class ProbabilityOperatorFormula : public OperatorFormula { public: ProbabilityOperatorFormula(std::shared_ptr const& subformula); - ProbabilityOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(Bound const& bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); ProbabilityOperatorFormula(OptimizationDirection optimalityType, std::shared_ptr const& subformula); - ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + ProbabilityOperatorFormula(boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~ProbabilityOperatorFormula() { // Intentionally left empty. diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp index 627263d36..791d1f5cc 100644 --- a/src/logic/RewardOperatorFormula.cpp +++ b/src/logic/RewardOperatorFormula.cpp @@ -2,19 +2,19 @@ namespace storm { namespace logic { - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, bound, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(comparisonType), boost::optional(bound), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), bound, subformula) { // Intentionally left empty. } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::optional(), boost::optional(), subformula) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula) : RewardOperatorFormula(rewardModelName, boost::optional(optimalityType), boost::none, subformula) { // Intentionally left empty. } @@ -55,12 +55,12 @@ namespace storm { this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); } - RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula), rewardModelName(rewardModelName) { + RewardOperatorFormula::RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula) : OperatorFormula(optimalityType, bound, subformula), rewardModelName(rewardModelName) { // Intentionally left empty. } std::shared_ptr RewardOperatorFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->rewardModelName, this->optimalityType, this->comparisonType, this->bound, this->getSubformula().substitute(substitution)); + return std::make_shared(this->rewardModelName, this->optimalityType, this->bound, this->getSubformula().substitute(substitution)); } std::ostream& RewardOperatorFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h index 37287c6e8..9e90ef01f 100644 --- a/src/logic/RewardOperatorFormula.h +++ b/src/logic/RewardOperatorFormula.h @@ -9,10 +9,10 @@ namespace storm { class RewardOperatorFormula : public OperatorFormula { public: RewardOperatorFormula(boost::optional const& rewardModelName, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, Bound const& bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, Bound const& bound, std::shared_ptr const& subformula); RewardOperatorFormula(boost::optional const& rewardModelName, OptimizationDirection optimalityType, std::shared_ptr const& subformula); - RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional comparisonType, boost::optional bound, std::shared_ptr const& subformula); + RewardOperatorFormula(boost::optional const& rewardModelName, boost::optional optimalityType, boost::optional> bound, std::shared_ptr const& subformula); virtual ~RewardOperatorFormula() { // Intentionally left empty. diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 764b02427..3b0d55ebf 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -175,7 +175,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThreshold()); } else { return result; } @@ -189,7 +189,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } @@ -203,7 +203,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } @@ -217,7 +217,7 @@ namespace storm { if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundValue()); + return result->asQuantitativeCheckResult().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold()); } else { return result; } diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index 959c8f96a..a3646e464 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -41,7 +41,7 @@ namespace storm { if (operatorFormula.hasBound()) { if (onlyInitialStatesRelevant) { - this->bound = std::make_pair(operatorFormula.getComparisonType(), static_cast(operatorFormula.getBound())); + this->bound = operatorFormula.getBound(); } if (!optimizationDirection) { @@ -54,7 +54,7 @@ namespace storm { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); if (probabilityOperatorFormula.hasBound()) { - if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { + if (probabilityOperatorFormula.getThreshold() == storm::utility::zero() || probabilityOperatorFormula.getThreshold() == storm::utility::one()) { this->qualitative = true; } } @@ -63,7 +63,7 @@ namespace storm { this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); if (rewardOperatorFormula.hasBound()) { - if (rewardOperatorFormula.getBound() == storm::utility::zero()) { + if (rewardOperatorFormula.getThreshold() == storm::utility::zero()) { this->qualitative = true; } } @@ -139,21 +139,21 @@ namespace storm { /*! * Retrieves the value of the bound (if set). */ - ValueType const& getBoundValue() const { - return bound.get().second; + ValueType const& getBoundThreshold() const { + return bound.get().threshold; } /*! * Retrieves the comparison type of the bound (if set). */ storm::logic::ComparisonType const& getBoundComparisonType() const { - return bound.get().first; + return bound.get().comparisonType; } /*! - * Retrieves the bound for the initial states (if set). + * Retrieves the bound (if set). */ - std::pair const& getBound() const { + storm::logic::Bound const& getBound() const { return bound.get(); } @@ -181,14 +181,13 @@ namespace storm { * @param rewardModelName If given, the checking has to be done wrt. to this reward model. * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values * for the initial states. - * @param initialStatesBound The bound with which the initial states will be compared. This may only be set - * together with the flag that indicates only initial states of the model are relevant. + * @param bound The bound with which the states will be compared. * @param qualitative A flag specifying whether the property needs to be checked qualitatively, i.e. compared * with bounds 0/1. * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { // Intentionally left empty. } @@ -204,8 +203,8 @@ namespace storm { // If set to true, the model checker may decide to only compute the values for the initial states. bool onlyInitialStatesRelevant; - // The bound with which the initial states will be compared. - boost::optional> bound; + // The bound with which the states will be compared. + boost::optional> bound; // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 340b5f33a..1a0d85b2c 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,8 +4,6 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/sparse/Mdp.h" #include "src/utility/solver.h" -#include "src/logic/BoundInfo.h" -#include "src/solver/MinMaxLinearEquationSolver.h" namespace storm { namespace modelchecker { diff --git a/src/solver/AbstractEquationSolver.h b/src/solver/AbstractEquationSolver.h new file mode 100644 index 000000000..e110318f6 --- /dev/null +++ b/src/solver/AbstractEquationSolver.h @@ -0,0 +1,53 @@ +#ifndef STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ +#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ + +#include "src/solver/TerminationCondition.h" + +namespace storm { + namespace solver { + + template + class AbstractEquationSolver { + public: + /*! + * Sets a custom termination condition that is used together with the regular termination condition of the + * solver. + * + * @param terminationCondition An object that can be queried whether to terminate early or not. + */ + void setTerminationCondition(std::unique_ptr> terminationCondition) { + this->terminationCondition = std::move(terminationCondition); + } + + /*! + * Removes a previously set custom termination condition. + */ + void resetTerminationCondition() { + this->terminationCondition = nullptr; + } + + /*! + * Retrieves whether a custom termination condition has been set. + */ + bool hasCustomTerminationCondition() { + return static_cast(this->terminationCondition); + } + + /*! + * Retrieves the custom termination condition (if any was set). + * + * @return The custom termination condition. + */ + TerminationCondition const& getTerminationCondition() const { + return *terminationCondition; + } + + protected: + // A termination condition to be used (can be unset). + std::unique_ptr> terminationCondition; + }; + + } +} + +#endif /* STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_ */ \ No newline at end of file diff --git a/src/solver/AllowEarlyTerminationCondition.cpp b/src/solver/AllowEarlyTerminationCondition.cpp deleted file mode 100644 index 2236c7c78..000000000 --- a/src/solver/AllowEarlyTerminationCondition.cpp +++ /dev/null @@ -1,48 +0,0 @@ -#include "AllowEarlyTerminationCondition.h" -#include "src/utility/vector.h" - -namespace storm { - namespace solver { - - template - TerminateAfterFilteredSumPassesThresholdValue::TerminateAfterFilteredSumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold) : - terminationThreshold(threshold), filter(filter) - { - // 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); - - return currentThreshold >= this->terminationThreshold; - - - } - - template - TerminateAfterFilteredExtremumPassesThresholdValue::TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum) : - terminationThreshold(threshold), filter(filter), useMinimumAsExtremum(useMinimum) - { - // Intentionally left empty. - } - - template - bool TerminateAfterFilteredExtremumPassesThresholdValue::terminateNow(const std::vector& currentValues) const { - assert(currentValues.size() >= filter.size()); - - ValueType initVal = terminationThreshold - 1; - ValueType currentThreshold = useMinimumAsExtremum ? storm::utility::vector::max_if(currentValues, filter, initVal) : storm::utility::vector::max_if(currentValues, filter, initVal); - - return currentThreshold >= this->terminationThreshold; - - - } - - - template class TerminateAfterFilteredExtremumPassesThresholdValue; - template class TerminateAfterFilteredSumPassesThresholdValue; - - } -} diff --git a/src/solver/AllowEarlyTerminationCondition.h b/src/solver/AllowEarlyTerminationCondition.h deleted file mode 100644 index be9084c70..000000000 --- a/src/solver/AllowEarlyTerminationCondition.h +++ /dev/null @@ -1,52 +0,0 @@ -#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 terminateNow(std::vector const& currentValues) const; - - protected: - ValueType terminationThreshold; - storm::storage::BitVector filter; - }; - - template - class TerminateAfterFilteredExtremumPassesThresholdValue : public AllowEarlyTerminationCondition{ - public: - TerminateAfterFilteredExtremumPassesThresholdValue(storm::storage::BitVector const& filter, ValueType threshold, bool useMinimum); - bool terminateNow(std::vector const& currentValue) const; - - protected: - ValueType terminationThreshold; - storm::storage::BitVector filter; - bool useMinimumAsExtremum; - }; - } -} - - - - - -#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ - diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 512cefbdb..e85fe3cce 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -3,8 +3,9 @@ #include +#include "src/solver/AbstractEquationSolver.h" + #include "src/storage/SparseMatrix.h" -#include "src/solver/AllowEarlyTerminationCondition.h" namespace storm { namespace solver { @@ -13,8 +14,8 @@ namespace storm { * An interface that represents an abstract linear equation solver. In addition to solving a system of linear * equations, the functionality to repeatedly multiply a matrix with a given vector is provided. */ - template - class LinearEquationSolver { + template + class LinearEquationSolver : public AbstractEquationSolver { public: virtual ~LinearEquationSolver() { // Intentionally left empty. @@ -30,7 +31,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; + virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -44,14 +45,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; - - void setEarlyTerminationCriterion(std::unique_ptr> v) { - earlyTermination = std::move(v); - } - - // A termination criterion to be used (can be unset). - std::unique_ptr> earlyTermination; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; }; } // namespace solver diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index cf334c6ee..42963ac29 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -4,11 +4,15 @@ #include #include #include -#include "SolverSelectionOptions.h" + +#include "src/solver/AbstractEquationSolver.h" +#include "src/solver/SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" -#include "src/solver/AllowEarlyTerminationCondition.h" +#include "src/storage/Scheduler.h" #include "src/solver/OptimizationDirection.h" +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace storage { template class SparseMatrix; @@ -17,15 +21,16 @@ namespace storm { namespace solver { /** - * Abstract base class which provides value-type independent helpers. + * Abstract base class of min-max linea equation solvers. */ - class AbstractMinMaxLinearEquationSolver { + template + class AbstractMinMaxLinearEquationSolver : public AbstractEquationSolver { public: void setSchedulerTracking(bool trackScheduler = true); std::vector getScheduler() const { - STORM_LOG_THROW(scheduler, storm::exceptions::Invali, "Cannot retrieve scheduler, because none was generated."); - reutrn scheduler.get(); + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return scheduler.get(); } void setOptimizationDirection(OptimizationDirection d) { @@ -35,37 +40,30 @@ namespace storm { void resetOptimizationDirection() { direction = OptimizationDirectionSetting::Unset; } - - void setEarlyTerminationCriterion(std::unique_ptr> v) { - earlyTermination = std::move(v); - } - + protected: AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech); - /// The direction in which to optimize, can be unset. + // The direction in which to optimize, can be unset. OptimizationDirectionSetting direction; - /// The required precision for the iterative methods. + // The required precision for the iterative methods. double precision; - /// Sets whether the relative or absolute error is to be considered for convergence detection. + // Sets whether the relative or absolute error is to be considered for convergence detection. bool relative; - /// The maximal number of iterations to do before iteration is aborted. + // The maximal number of iterations to do before iteration is aborted. uint_fast64_t maximalNumberOfIterations; - /// Whether value iteration or policy iteration is to be used. + // Whether value iteration or policy iteration is to be used. bool useValueIteration; - /// Whether we generate a scheduler during solving. + // Whether we generate a scheduler during solving. bool trackScheduler; - /// The scheduler (if it could be successfully generated). - boost::optional scheduler; - - // A termination criterion to be used (can be unset). - std::unique_ptr> earlyTermination; + // The scheduler (if it could be successfully generated). + boost::optional> scheduler; }; /*! @@ -74,11 +72,9 @@ namespace storm { * provided. */ template - class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { + class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { 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), earlyTermination(new NoEarlyTerminationCondition()) { + 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) { // Intentionally left empty. } diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp index 4994f8ade..b135fba59 100644 --- a/src/solver/SolveGoal.cpp +++ b/src/solver/SolveGoal.cpp @@ -14,33 +14,33 @@ namespace storm { namespace solver { template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + 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->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); + p->setTerminationCondition(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); return p; } template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { if (goal.isBounded()) { return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); } - std::unique_ptr> p = factory.create(matrix); - p->setOptimizationDirection(goal.direction()); - return p; + std::unique_ptr> solver = factory.create(matrix); + solver->setOptimizationDirection(goal.direction()); + return solver; } template - std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - std::unique_ptr> p = factory.create(matrix); - p->setOptimizationDirection(goal.direction()); - p->setEarlyTerminationCriterion(std::make_unique>(goal.relevantColumns(), goal.thresholdValue(), goal.minimize())); - return p; + 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())); + return solver; } template - std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { + std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::utility::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { if (goal.isBounded()) { return configureLinearEquationSolver(static_cast const&>(goal), factory, matrix); } diff --git a/src/solver/SolveGoal.h b/src/solver/SolveGoal.h index 7a8f9c661..b87fa0837 100644 --- a/src/solver/SolveGoal.h +++ b/src/solver/SolveGoal.h @@ -5,7 +5,7 @@ #include "src/solver/OptimizationDirection.h" #include "src/logic/ComparisonType.h" -#include "src/logic/BoundInfo.h" +#include "src/logic/Bound.h" #include "src/storage/BitVector.h" namespace storm { @@ -57,11 +57,11 @@ namespace storm { template class BoundedGoal : public SolveGoal { public: - BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType ct, ValueType const& threshold, storm::storage::BitVector const& relColumns) : SolveGoal(optimizationDirection), boundType(ct), threshold(threshold), relevantColumnVector(relColumns) { + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType comparisonType, ValueType const& threshold, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(comparisonType, threshold), relevantValueVector(relevantValues) { // Intentionally left empty. } - BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::BoundInfo const& boundInfo, storm::storage::BitVector const& relevantColumns) : SolveGoal(optimizationDirection), boundType(boundInfo.boundType), threshold(boundInfo.bound), relevantColumnVector(relevantColumns) { + BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::Bound const& bound, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(bound), relevantValueVector(relevantValues) { // Intentionally left empty. } @@ -74,21 +74,20 @@ namespace storm { } bool boundIsALowerBound() const { - return (boundType == storm::logic::ComparisonType::Greater || boundType == storm::logic::ComparisonType::GreaterEqual); + return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::GreaterEqual); } ValueType const& thresholdValue() const { - return threshold; + return bound.threshold; } - storm::storage::BitVector const& relevantColumns() const { - return relevantColumnVector; + storm::storage::BitVector const& relevantValues() const { + return relevantValues; } private: - storm::logic::ComparisonType boundType; - ValueType threshold; - storm::storage::BitVector relevantColumnVector; + Bound bound; + storm::storage::BitVector relevantValueVector; }; template diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp new file mode 100644 index 000000000..98434e407 --- /dev/null +++ b/src/solver/TerminationCondition.cpp @@ -0,0 +1,41 @@ +#include "src/solver/TerminationCondition.h" +#include "src/utility/vector.h" + +#include "src/utility/macros.h" + +namespace storm { + namespace solver { + + template + bool NoTerminationCondition::terminateNow(std::vector const& currentValues) const { + return false; + } + + template + TerminateIfFilteredSumExceedsThreshold::TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict) : threshold(threshold), filter(filter), strict(strict) { + // Intentionally left empty. + } + + template + bool TerminateIfFilteredSumExceedsThreshold::terminateNow(std::vector const& currentValues) const { + STORM_LOG_ASSERT(currentValues.size() == filter.size(), "Vectors sizes mismatch."); + ValueType currentThreshold = storm::utility::vector::sum_if(currentValues, filter); + return strict ? currentThreshold > this->threshold : currentThreshold >= this->threshold; + } + + template + TerminateIfFilteredExtremumExceedsThreshold::TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum) : TerminateIfFilteredSumExceedsThreshold(filter, threshold, strict), useMinimum(useMinimum) { + // Intentionally left empty. + } + + 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); + return this->strict ? currentValue > this->threshold : currentValue >= this->threshold; + } + + template class TerminateIfFilteredSumExceedsThreshold; + template class TerminateIfFilteredExtremumExceedsThreshold; + } +} diff --git a/src/solver/TerminationCondition.h b/src/solver/TerminationCondition.h new file mode 100644 index 000000000..4ea5f5c3d --- /dev/null +++ b/src/solver/TerminationCondition.h @@ -0,0 +1,53 @@ +#ifndef ALLOWEARLYTERMINATIONCONDITION_H +#define ALLOWEARLYTERMINATIONCONDITION_H + +#include +#include "src/storage/BitVector.h" + + +namespace storm { + namespace solver { + template + class TerminationCondition { + public: + virtual bool terminateNow(std::vector const& currentValues) const = 0; + }; + + template + class NoTerminationCondition : public TerminationCondition { + public: + bool terminateNow(std::vector const& currentValues) const; + }; + + template + class TerminateIfFilteredSumExceedsThreshold : public TerminationCondition { + public: + TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict); + bool terminateNow(std::vector const& currentValues) const; + + protected: + ValueType threshold; + storm::storage::BitVector filter; + bool strict; + }; + + template + class TerminateIfFilteredExtremumExceedsThreshold : public TerminateIfFilteredSumExceedsThreshold{ + public: + TerminateIfFilteredExtremumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict, bool useMinimum); + bool terminateNow(std::vector const& currentValue) const; + + protected: + ValueType threshold; + storm::storage::BitVector filter; + bool useMinimum; + }; + } +} + + + + + +#endif /* ALLOWEARLYTERMINATIONCONDITION_H */ + diff --git a/src/utility/vector.h b/src/utility/vector.h index 665569645..31b1a5493 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -388,55 +388,64 @@ namespace storm { */ template VT sum_if(std::vector const& values, storm::storage::BitVector const& filter) { - assert(values.size() >= filter.size()); + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); VT sum = storm::utility::zero(); - for(uint_fast64_t i : filter) { - sum += values[i]; + for(auto pos : filter) { + sum += values[pos]; } return sum; } /** - * Computes the maximum of the entries from the values that are set to one in the filter vector - * @param values - * @param filter - * @param smallestPossibleValue A value which is not larger than any value in values. If the filter is empty, this value is returned. - * @return The maximum over the subset of the values and the smallestPossibleValue. + * Computes the maximum of the entries from the values that are selected by the (non-empty) filter. + * @param values The values in which to search. + * @param filter The filter to use. + * @return The maximum over the selected values. */ template - VT max_if(std::vector const& values, storm::storage::BitVector const& filter, VT const& smallestPossibleValue) { - assert(values.size() >= filter.size()); + VT max_if(std::vector const& values, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); + STORM_LOG_ASSERT(!filter.empty(), "Empty selection."); + + auto it = filter.begin(); + auto ite = filter.end(); + + VT current = values[*it]; + ++it; - VT max = smallestPossibleValue; - for(uint_fast64_t i : filter) { - if(values[i] > max) { - max = values[i]; + for (; it != ite; ++it) { + if (values[*it] > current) { + current = values[*it]; } - } - return max; + } + return current; } /** - * Computes the minimum of the entries from the values that are set to one in the filter vector - * @param values - * @param filter - * @param largestPossibleValue A value which is not smaller than any value in values. If the filter is empty, this value is returned. - * @return The minimum over the subset of the values and the largestPossibleValue. + * Computes the minimum of the entries from the values that are selected by the (non-empty) filter. + * @param values The values in which to search. + * @param filter The filter to use. + * @return The minimum over the selected values. */ template - VT min_if(std::vector const& values, storm::storage::BitVector const& filter, VT const& largestPossibleValue) { - assert(values.size() >= filter.size()); - VT min = largestPossibleValue; - for(uint_fast64_t i : filter) { - if(values[i] < min) { - min = values[i]; + VT min_if(std::vector const& values, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch."); + STORM_LOG_ASSERT(!filter.empty(), "Empty selection."); + + auto it = filter.begin(); + auto ite = filter.end(); + + VT current = values[*it]; + ++it; + + for (; it != ite; ++it) { + if (values[*it] < current) { + current = values[*it]; } - } - return min; + } + return current; } - - /*! * Reduces the given source vector by selecting an element according to the given filter out of each row group. * From 2dd6a3dba227557ad3bec0e2ddc4085312aae03e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Feb 2016 17:43:40 +0100 Subject: [PATCH 3/8] minor change Former-commit-id: 32568cc5038d51a2abc35b544516ed01d5f64362 --- src/permissivesched/PermissiveSchedulers.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 7059cd1a0..21aa9227c 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -26,7 +26,7 @@ namespace storm { auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); MilpPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported"); - comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound()); + comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound().threshold); //comp.dumpLpToFile("milpdump.lp"); std::cout << "Found Solution: " << (comp.foundSolution() ? "yes" : "no") << std::endl; if(comp.foundSolution()) { @@ -54,7 +54,7 @@ namespace storm { auto solver = storm::utility::solver::getSmtSolver(*expressionManager); SmtPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported"); - comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound()); + comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound().threshold); if(comp.foundSolution()) { return boost::optional>(comp.getScheduler()); } else { From 5a1039838f1d36c41c25085cf1c35c528c274661 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 14 Feb 2016 16:32:38 +0100 Subject: [PATCH 4/8] 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)); } From 8f087597cc4d569e4f7dc2726700d64f2063fa1b Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Feb 2016 16:06:14 +0100 Subject: [PATCH 5/8] more work towards proper scheduler generation Former-commit-id: ee6237ef497637fe95908a3bd70c63f568f24532 --- .../SMTMinimalCommandSetGenerator.h | 4 +- src/modelchecker/CheckTask.h | 9 +++- .../helper/MDPModelCheckingHelperReturnType.h | 7 ++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 44 ++++++++++++++++--- .../prctl/helper/SparseMdpPrctlHelper.h | 4 +- .../ExplicitQuantitativeCheckResult.cpp | 16 +++++++ .../results/ExplicitQuantitativeCheckResult.h | 9 ++++ src/parser/PrismParser.cpp | 2 +- .../GmmxxMinMaxLinearEquationSolver.cpp | 13 +++--- src/solver/MinMaxLinearEquationSolver.cpp | 5 +++ src/solver/MinMaxLinearEquationSolver.h | 3 +- src/storage/PartialScheduler.cpp | 8 ++++ src/storage/PartialScheduler.h | 3 ++ src/utility/graph.cpp | 6 +-- src/utility/solver.cpp | 9 ++-- src/utility/solver.h | 4 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 36 +++++++++++++++ .../modelchecker/scheduler_generation.nm | 16 +++++++ 18 files changed, 163 insertions(+), 35 deletions(-) create mode 100644 test/functional/modelchecker/scheduler_generation.nm diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 3026ab74e..3f03440d3 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1763,7 +1763,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; @@ -1793,7 +1793,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, bound, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet()); + auto labelSet = getMinimalCommandSet(probabilityOperator.getSubformula(), program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::counterexampleGeneratorSettings().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index a3646e464..be56e29e1 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -30,7 +30,7 @@ namespace storm { */ CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; - this->produceSchedulers = true; + this->produceSchedulers = false; this->qualitative = false; if (formula.isOperatorFormula()) { @@ -165,6 +165,13 @@ namespace storm { return qualitative; } + /*! + * Sets whether to produce schedulers (if supported). + */ + void setProduceSchedulers(bool produceSchedulers) { + this->produceSchedulers = produceSchedulers; + } + /*! * Retrieves whether scheduler(s) are to be produced (if supported). */ diff --git a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index fac823940..4ce7bb23f 100644 --- a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -3,14 +3,13 @@ #include #include -#include "src/storage/PartialScheduler.h" +#include "src/storage/Scheduler.h" namespace storm { namespace storage { class BitVector; } - namespace modelchecker { namespace helper { template @@ -19,7 +18,7 @@ namespace storm { MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType const&) = delete; MDPSparseModelCheckingHelperReturnType(MDPSparseModelCheckingHelperReturnType&&) = default; - MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr && scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { + MDPSparseModelCheckingHelperReturnType(std::vector&& values, std::unique_ptr&& scheduler = nullptr) : values(std::move(values)), scheduler(std::move(scheduler)) { // Intentionally left empty. } @@ -31,7 +30,7 @@ namespace storm { std::vector values; // A scheduler, if it was computed. - std::unique_ptr scheduler; + std::unique_ptr scheduler; }; } diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 85817b1b2..cb03e5724 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1,4 +1,4 @@ -#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" + #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -12,6 +12,7 @@ #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" +#include "src/storage/TotalScheduler.h" #include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/LpSolver.h" @@ -56,7 +57,6 @@ namespace storm { return result; } - template std::vector SparseMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { @@ -73,7 +73,8 @@ namespace storm { template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only."); // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. @@ -96,7 +97,12 @@ namespace storm { // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - + + // If requested, we will produce a scheduler. + std::unique_ptr scheduler; + if (produceScheduler) { + scheduler = std::make_unique(transitionMatrix.getRowGroupCount()); + } // Check whether we need to compute exact probabilities for some states. if (qualitative) { @@ -119,20 +125,44 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + solver->setTrackScheduler(produceScheduler); solver->solveEquationSystem(x, b); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); + + if (produceScheduler) { + storm::storage::Scheduler const& subscheduler = solver->getScheduler(); + uint_fast64_t currentSubState = 0; + for (auto maybeState : maybeStates) { + scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); + ++currentSubState; + } + } + } + } + + // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for + // the states with probability 0 or 1 (depending on whether we maximize or minimize). + if (produceScheduler) { + storm::storage::PartialScheduler relevantQualitativeScheduler; + if (goal.minimize()) { + relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb0E(statesWithProbability0, transitionMatrix); + } else { + relevantQualitativeScheduler = storm::utility::graph::computeSchedulerProb1E(statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates); + } + for (auto const& stateChoicePair : relevantQualitativeScheduler) { + scheduler->setChoice(stateChoicePair.first, stateChoicePair.second); } } - return MDPSparseModelCheckingHelperReturnType(std::move(result)); + return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { storm::solver::SolveGoal goal(dir); - return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, producePolicy, minMaxLinearEquationSolverFactory)); + return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory)); } template diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 8567c445b..f09e40d4a 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -36,9 +36,9 @@ namespace storm { static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool producePolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 3f22b4ff2..08ca016fd 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -79,6 +79,22 @@ namespace storm { } } + template + bool ExplicitQuantitativeCheckResult::hasScheduler() const { + return static_cast(scheduler); + } + + template + void ExplicitQuantitativeCheckResult::setScheduler(std::unique_ptr&& scheduler) { + this->scheduler = std::move(scheduler); + } + + template + storm::storage::Scheduler const& ExplicitQuantitativeCheckResult::getScheduler() const { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return *scheduler.get(); + } + template std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out) const { out << "["; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 9734a176f..ee49b74ec 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -4,9 +4,11 @@ #include #include #include +#include #include "src/modelchecker/results/QuantitativeCheckResult.h" #include "src/storage/sparse/StateType.h" +#include "src/storage/Scheduler.h" #include "src/utility/OsDetection.h" namespace storm { @@ -51,9 +53,16 @@ namespace storm { virtual void oneMinus() override; + bool hasScheduler() const; + void setScheduler(std::unique_ptr&& scheduler); + storm::storage::Scheduler const& getScheduler() const; + private: // The values of the quantitative check result. boost::variant values; + + // An optional scheduler that accompanies the values. + boost::optional> scheduler; }; } } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index b2349ebf7..9040f3cf4 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -142,7 +142,7 @@ namespace storm { assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct>()]; assignmentDefinitionList.name("assignment list"); - updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; updateDefinition.name("update"); updateListDefinition %= +updateDefinition(qi::_r1) % "+"; diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index d5dcbb627..00c51e82c 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -16,12 +16,8 @@ namespace storm { template GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : - MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), \ - storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative,\ - storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), - gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { - - + MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + // Intentionally left empty. } template @@ -29,11 +25,12 @@ namespace storm { // Intentionally left empty. } - template void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { if (this->useValueIteration) { - // Set up the environment for the power method. If scratch memory was not provided, we need to create it. + STORM_LOG_THROW(!this->isTrackSchedulerSet(), storm::exceptions::InvalidSettingsException, "Unable to produce a scheduler when using value iteration. Use policy iteration instead."); + + // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(b.size()); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 4f9627a20..294b32c2a 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -23,6 +23,11 @@ namespace storm { this->trackScheduler = trackScheduler; } + template + bool AbstractMinMaxLinearEquationSolver::hasScheduler() const { + return static_cast(scheduler); + } + template bool AbstractMinMaxLinearEquationSolver::isTrackSchedulerSet() const { return this->trackScheduler; diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index f33fdc6e1..78781c68a 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -30,6 +30,7 @@ namespace storm { public: void setTrackScheduler(bool trackScheduler = true); bool isTrackSchedulerSet() const; + bool hasScheduler() const; storm::storage::Scheduler const& getScheduler() const; @@ -69,7 +70,7 @@ namespace storm { template class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { 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) { + MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackScheduler, MinMaxTechniqueSelection prefTech) : AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackScheduler, prefTech), A(matrix) { // Intentionally left empty. } diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp index 6f004c315..28076f7a1 100644 --- a/src/storage/PartialScheduler.cpp +++ b/src/storage/PartialScheduler.cpp @@ -22,6 +22,14 @@ namespace storm { return stateChoicePair->second; } + PartialScheduler::map_type::const_iterator PartialScheduler::begin() const { + return stateToChoiceMapping.begin(); + } + + PartialScheduler::map_type::const_iterator PartialScheduler::end() const { + return stateToChoiceMapping.end(); + } + std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) { out << "partial scheduler (defined on " << scheduler.stateToChoiceMapping.size() << " states) [ "; uint_fast64_t remainingEntries = scheduler.stateToChoiceMapping.size(); diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h index e5f9fffb2..4ae503348 100644 --- a/src/storage/PartialScheduler.h +++ b/src/storage/PartialScheduler.h @@ -19,6 +19,9 @@ namespace storm { uint_fast64_t getChoice(uint_fast64_t state) const override; + map_type::const_iterator begin() const; + map_type::const_iterator end() const; + friend std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler); private: diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index bac64948f..0aa8b2836 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -280,7 +280,7 @@ namespace storm { } } if (allSuccessorsInStates) { - result.setChoice(state, choice); + result.setChoice(state, choice - nondeterministicChoiceIndices[state]); break; } } @@ -304,7 +304,7 @@ namespace storm { } } if (oneSuccessorInStates) { - result.setChoice(state, choice); + result.setChoice(state, choice - nondeterministicChoiceIndices[state]); break; } } @@ -356,7 +356,7 @@ namespace storm { // If all successors for a given nondeterministic choice are in the prob1E state set, we // perform a backward search from that state. if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) { - result.setChoice(predecessorEntryIt->getColumn(), row); + result.setChoice(predecessorEntryIt->getColumn(), row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]); currentStates.set(predecessorEntryIt->getColumn(), true); stack.push_back(predecessorEntryIt->getColumn()); break; diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index dbb798cb2..013a800c4 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -91,17 +91,19 @@ namespace storm { } template - void MinMaxLinearEquationSolverFactory::setSolverType(storm::solver::EquationSolverTypeSelection solverTypeSel) { + MinMaxLinearEquationSolverFactory& 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); } - + return *this; } + template - void MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { + MinMaxLinearEquationSolverFactory& MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { this->prefTech = preferredTech; + return *this; } template @@ -128,7 +130,6 @@ namespace storm { } p1->setTrackScheduler(trackScheduler); return p1; - } template diff --git a/src/utility/solver.h b/src/utility/solver.h index 446b22c7a..ef8120b65 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -114,8 +114,8 @@ 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 trackScheduler = false) const; - void setSolverType(storm::solver::EquationSolverTypeSelection solverType); - void setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); + MinMaxLinearEquationSolverFactory& setSolverType(storm::solver::EquationSolverTypeSelection solverType); + MinMaxLinearEquationSolverFactory& setPreferredTechnique(storm::solver::MinMaxTechniqueSelection); protected: /// The type of solver which should be created. diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 23184f61f..14239a438 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -14,6 +14,8 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" +#include "src/parser/PrismParser.h" +#include "src/builder/ExplicitPrismModelBuilder.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> abstractModel = 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.trans.rew"); @@ -188,3 +190,37 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); } + +TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/scheduler_generation.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program); + EXPECT_EQ(4ul, model->getNumberOfStates()); + EXPECT_EQ(11ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(7ul, mdp->getNumberOfChoices()); + + auto solverFactory = std::make_unique>(storm::solver::EquationSolverTypeSelection::Gmmxx); + solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::PolicyIteration); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + checkTask.setProduceSchedulers(true); + + std::unique_ptr result = checker.check(checkTask); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); + checkTask.replaceFormula(*formula); + + result = checker.check(checkTask); + +} diff --git a/test/functional/modelchecker/scheduler_generation.nm b/test/functional/modelchecker/scheduler_generation.nm new file mode 100644 index 000000000..f5be3b746 --- /dev/null +++ b/test/functional/modelchecker/scheduler_generation.nm @@ -0,0 +1,16 @@ +mdp + +module one + + s : [0 .. 5] init 0; + + [] s=0 -> 0.5: (s'=1) + 0.5: (s'=3); + [] s=1 -> 0.4 : (s'=4) + 0.6: (s'=3); + [] s=1 -> 1: (s'=4); + [] s=1 -> 0.8: (s'=3) + 0.2: (s'=4); + [] s=0 | s = 2 -> 0.9: (s'=s) + 0.1 : (s'=3); + [] 3 <= s & s <= 4 -> 1: true; + +endmodule + +label "target" = s=3; From 3727018ef407b782f2dec2494a960e505dc1fe5f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Feb 2016 19:11:25 +0100 Subject: [PATCH 6/8] added functionality to sparse MDP helper to compute until probabilities just for maybe states (and produce the corresponding scheduler) Former-commit-id: 79aae02a133eca9339f581d01bcc386f19e0f7df --- .../prctl/SparseMdpPrctlModelChecker.cpp | 6 +++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 34 +++++++++++++------ .../prctl/helper/SparseMdpPrctlHelper.h | 2 ++ src/solver/MinMaxLinearEquationSolver.cpp | 8 ++++- src/solver/MinMaxLinearEquationSolver.h | 7 ++-- .../GmmxxMdpPrctlModelCheckerTest.cpp | 26 +++++++++++--- 6 files changed, 63 insertions(+), 20 deletions(-) diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index b13906151..710d926a7 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -88,7 +88,11 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; } template diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index cb03e5724..adec586dd 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -120,19 +120,13 @@ namespace storm { // the accumulated probability of going from state i to some 'yes' state. std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); - // Create vector for results for maybe states. - std::vector x(maybeStates.getNumberOfSetBits()); - - // Solve the corresponding system of equations. - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); - solver->setTrackScheduler(produceScheduler); - solver->solveEquationSystem(x, b); + MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeUntilProbabilitiesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, x); - + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); + if (produceScheduler) { - storm::storage::Scheduler const& subscheduler = solver->getScheduler(); + storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler; uint_fast64_t currentSubState = 0; for (auto maybeState : maybeStates) { scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); @@ -158,6 +152,26 @@ namespace storm { return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } + + template + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // If requested, we will produce a scheduler. + std::unique_ptr scheduler; + + // Create vector for results for maybe states. + std::vector x(submatrix.getRowGroupCount()); + + // Solve the corresponding system of equations. + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + solver->setTrackScheduler(produceScheduler); + solver->solveEquationSystem(x, b); + + if (produceScheduler) { + scheduler = std::make_unique(std::move(solver->getScheduler())); + } + + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + } template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index f09e40d4a..0b47759d7 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -37,6 +37,8 @@ namespace storm { static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 294b32c2a..5041469bc 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -34,7 +34,13 @@ namespace storm { } template - storm::storage::Scheduler const& AbstractMinMaxLinearEquationSolver::getScheduler() const { + storm::storage::TotalScheduler const& AbstractMinMaxLinearEquationSolver::getScheduler() const { + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return *scheduler.get(); + } + + template + storm::storage::TotalScheduler& AbstractMinMaxLinearEquationSolver::getScheduler() { STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); return *scheduler.get(); } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 78781c68a..71ea10ee2 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -10,7 +10,7 @@ #include "src/solver/AbstractEquationSolver.h" #include "src/solver/SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" -#include "src/storage/Scheduler.h" +#include "src/storage/TotalScheduler.h" #include "src/solver/OptimizationDirection.h" #include "src/exceptions/InvalidSettingsException.h" @@ -32,7 +32,8 @@ namespace storm { bool isTrackSchedulerSet() const; bool hasScheduler() const; - storm::storage::Scheduler const& getScheduler() const; + storm::storage::TotalScheduler const& getScheduler() const; + storm::storage::TotalScheduler& getScheduler(); void setOptimizationDirection(OptimizationDirection d); void resetOptimizationDirection(); @@ -59,7 +60,7 @@ namespace storm { bool trackScheduler; // The scheduler (if it could be successfully generated). - mutable boost::optional> scheduler; + mutable boost::optional> scheduler; }; /*! diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 14239a438..725e1376d 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -193,7 +193,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/scheduler_generation.nm"); - + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -206,7 +206,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { std::shared_ptr> mdp = model->as>(); EXPECT_EQ(7ul, mdp->getNumberOfChoices()); - + auto solverFactory = std::make_unique>(storm::solver::EquationSolverTypeSelection::Gmmxx); solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::PolicyIteration); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); @@ -218,9 +218,25 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { std::unique_ptr result = checker.check(checkTask); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0, scheduler.getChoice(0)); + EXPECT_EQ(1, scheduler.getChoice(1)); + EXPECT_EQ(0, scheduler.getChoice(2)); + EXPECT_EQ(0, scheduler.getChoice(3)); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); - checkTask.replaceFormula(*formula); - - result = checker.check(checkTask); + checkTask = storm::modelchecker::CheckTask(*formula); + checkTask.setProduceSchedulers(true); + result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1, scheduler2.getChoice(0)); + EXPECT_EQ(2, scheduler2.getChoice(1)); + EXPECT_EQ(0, scheduler2.getChoice(2)); + EXPECT_EQ(0, scheduler2.getChoice(3)); } From fa44d65ebd133112b1fbbdeb8c314c032f142e85 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Feb 2016 19:17:46 +0100 Subject: [PATCH 7/8] renamed policy to scheduler in some variable names Former-commit-id: cfbaaa533d73f0ec9684c9d87e28cccb97aa6622 --- src/solver/GmmxxMinMaxLinearEquationSolver.cpp | 6 +++--- src/solver/GmmxxMinMaxLinearEquationSolver.h | 4 ++-- src/solver/NativeMinMaxLinearEquationSolver.cpp | 11 ++--------- src/solver/NativeMinMaxLinearEquationSolver.h | 4 ++-- 4 files changed, 9 insertions(+), 16 deletions(-) diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index 00c51e82c..07052e6eb 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -15,13 +15,13 @@ namespace storm { namespace solver { template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : - MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) : + MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { // Intentionally left empty. } template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackPolicy, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { // Intentionally left empty. } diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h index 08432658e..accba556f 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -22,7 +22,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackScheduler = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -33,7 +33,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy = false); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler = false); virtual void performMatrixVectorMultiplication(OptimizationDirection d, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 629385e8f..22ccf956c 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -14,19 +14,12 @@ namespace storm { namespace solver { template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : - MinMaxLinearEquationSolver(A, storm::settings::nativeEquationSolverSettings().getPrecision(), \ - storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, \ - storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique) - { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) : MinMaxLinearEquationSolver(A, storm::settings::nativeEquationSolverSettings().getPrecision(), storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique) { // Intentionally left empty. } template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : - MinMaxLinearEquationSolver(A, precision, \ - relative, \ - maximalNumberOfIterations, trackPolicy, tech) { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech) { // Intentionally left empty. } diff --git a/src/solver/NativeMinMaxLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h index 5fcd76aa9..7920678fa 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -19,7 +19,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackScheduler = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -30,7 +30,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackPolicy = false); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackScheduler = false); virtual void performMatrixVectorMultiplication(OptimizationDirection dir, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; From 4970268ae1fdbacbdfee3505c27d5829d475d546 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Feb 2016 14:44:50 +0100 Subject: [PATCH 8/8] fixed gtest for xcode (cmake) Former-commit-id: b391eef46c2b9bc542916de3767ec8fbc607ecda --- resources/3rdparty/CMakeLists.txt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 694ab7265..32fa4c5a5 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -38,9 +38,9 @@ ExternalProject_Add( #TIMEOUT 10 DOWNLOAD_COMMAND "" SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/gtest-1.7.0" - # Force separate output paths for debug and release builds to allow easy - # identification of correct lib in subsequent TARGET_LINK_LIBRARIES - CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} + # Force the same output paths for debug and release builds so that + # we know in which place the binaries end up when using the Xcode generator + CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 # Disable install step INSTALL_COMMAND "" BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0"