Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
IterativeMinMaxLinearEquationSolver.h
Go to the documentation of this file.
1#pragma once
2
4
6
9
11
13
14namespace storm {
15
16class Environment;
17
18namespace solver {
19
20template<typename ValueType, typename SolutionType = ValueType>
22 public:
24 IterativeMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
26 std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
28 std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
29
30 virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
31 std::vector<ValueType> const& b) const override;
32
33 virtual void clearCache() const override;
34
36 boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none,
37 bool const& hasInitialScheduler = false) const override;
38
39 private:
40 MinMaxMethod getMethod(Environment const& env, bool isExactMode) const;
41
42 bool solveInducedEquationSystem(Environment const& env, std::unique_ptr<LinearEquationSolver<ValueType>>& linearEquationSolver,
43 std::vector<uint64_t> const& scheduler, std::vector<SolutionType>& x, std::vector<ValueType>& subB,
44 std::vector<ValueType> const& originalB) const;
45 bool solveEquationsPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
46 bool performPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b,
47 std::vector<storm::storage::sparse::state_type>&& initialPolicy) const;
48 bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
49
50 bool solveEquationsValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
51 bool solveEquationsOptimisticValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
52 std::vector<ValueType> const& b) const;
53 bool solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
54 std::vector<ValueType> const& b) const;
55 bool solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
56 std::vector<ValueType> const& b) const;
57 bool solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
58
59 bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
60
61 void setUpViOperator() const;
62 void extractScheduler(std::vector<SolutionType>& x, std::vector<ValueType> const& b, OptimizationDirection const& dir, bool robust,
63 bool updateX = true) const;
64
65 void createLinearEquationSolver(Environment const& env) const;
66
68 std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
69
70 // possibly cached data
71 mutable std::shared_ptr<storm::solver::helper::ValueIterationOperator<ValueType, false, SolutionType>> viOperator;
72 mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector; // A.rowGroupCount() entries
73};
74
75} // namespace solver
76} // namespace storm
virtual void clearCache() const override
Clears the currently cached data that has been stored during previous calls of the solver.
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.
OptimizationDirectionSetting direction
The optimization direction to use for calls to functions that do not provide it explicitly....
bool hasInitialScheduler() const
Returns true iff an initial scheduler is set.
storm::storage::SparseMatrix< ValueType > const * A
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18