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); + } }