Storm 1.10.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 solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
55 std::vector<ValueType> const& b) const;
56 bool solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x,
57 std::vector<ValueType> const& b) const;
58 bool solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
59
60 bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector<SolutionType>& x, std::vector<ValueType> const& b) const;
61
62 void setUpViOperator() const;
63 void extractScheduler(std::vector<SolutionType>& x, std::vector<ValueType> const& b, OptimizationDirection const& dir, bool robust,
64 bool updateX = true) const;
65
66 void createLinearEquationSolver(Environment const& env) 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.
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