Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
IterativeMinMaxLinearEquationSolver.h
Go to the documentation of this file.
1#pragma once
2
3#include <variant>
6
8
11
13
15
16namespace storm {
17
18class Environment;
19
20namespace solver {
21
22template<typename ValueType, typename SolutionType = ValueType>
24 public:
25 IterativeMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<SolutionType>>&& linearEquationSolverFactory);
27 std::unique_ptr<LinearEquationSolverFactory<SolutionType>>&& linearEquationSolverFactory);
29 std::unique_ptr<LinearEquationSolverFactory<SolutionType>>&& linearEquationSolverFactory);
30
31 virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
32 std::vector<ValueType> const& b) const override;
33
34 virtual void clearCache() const override;
35
37 boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
38 bool const& hasInitialScheduler = false) const override;
39
40 private:
41 MinMaxMethod getMethod(Environment const& env, bool isExactMode) const;
42
43 bool solveInducedEquationSystem(Environment const& env, std::unique_ptr<LinearEquationSolver<SolutionType>>& linearEquationSolver,
44 std::vector<uint64_t> const& scheduler, std::vector<SolutionType>& x, std::vector<ValueType>& subB,
45 std::vector<ValueType> const& originalB, OptimizationDirection dir) const;
46 bool solveEquationsPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
47 bool performPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b,
48 std::vector<storm::storage::sparse::state_type>&& initialPolicy) const;
49 bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
50
51 bool solveEquationsValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
52 bool solveEquationsOptimisticValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
53 std::vector<ValueType> const& b) const;
54 bool solveEquationsGuessingValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
55 std::vector<ValueType> const& b) const;
56 bool solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
57 std::vector<ValueType> const& b) const;
58 bool solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
59 std::vector<ValueType> const& b) const;
60 bool solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
61
62 bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
63
64 void setUpViOperator() const;
65 void extractScheduler(std::vector<SolutionType>& x, std::vector<ValueType> const& b, OptimizationDirection const& dir,
66 UncertaintyResolutionMode uncertaintyResolutionMode, bool updateX = true) const;
67
69 std::unique_ptr<LinearEquationSolverFactory<SolutionType>> linearEquationSolverFactory;
70
71 // possibly cached data
72
73 // two different VI operators, one for trivialrowgrouping, one without
74 mutable std::shared_ptr<storm::solver::helper::ValueIterationOperator<ValueType, true, SolutionType>> viOperatorTriv;
75 mutable std::shared_ptr<storm::solver::helper::ValueIterationOperator<ValueType, false, SolutionType>> viOperatorNontriv;
76
77 mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector; // A.rowGroupCount() entries
78};
79
80} // namespace solver
81} // namespace storm
virtual void clearCache() const override
Clears the currently cached data that has been stored during previous calls of the solver.
IterativeMinMaxLinearEquationSolver(std::unique_ptr< LinearEquationSolverFactory< SolutionType > > &&linearEquationSolverFactory)
virtual bool internalSolveEquations(Environment const &env, OptimizationDirection dir, std::vector< SolutionType > &x, std::vector< ValueType > const &b) const override
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool const &hasInitialScheduler=false) const override
Retrieves the requirements of this solver for solving equations with the current settings.
An interface that represents an abstract linear equation solver.
A class that holds a possibly non-square matrix in the compressed row storage format.