Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GuessingValueIterationHelper.h
Go to the documentation of this file.
1#pragma once
2
3#include <vector>
4
6
10
11namespace storm::solver::helper {
12
13template<typename ValueType>
14struct GVIData {
15 std::vector<ValueType> const& x;
16 std::vector<ValueType> const& y;
18};
19
20namespace gviinternal {
21
22typedef uint64_t IndexType;
24
25template<typename ValueType>
27 public:
29
30 IndexType selectRowGroupToGuess(const std::vector<ValueType>& lowerX, const std::vector<ValueType>& upperX);
31
32 ValueType getMaxLength(std::vector<ValueType>& lower, std::vector<ValueType>& upper) const;
33 ValueType getSumLength(std::vector<ValueType>& lower, std::vector<ValueType>& upper) const;
34
35 private:
37 // this is only used to avoid reallocations
38 std::vector<ValueType> weights;
39
40 void swipeWeights();
41};
42
43} // namespace gviinternal
44
45template<typename ValueType, OptimizationDirection Dir>
46class GVIBackend;
47
52template<typename ValueType, bool TrivialRowGrouping>
54 public:
57
66 SolverStatus solveEquations(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, uint64_t& numIterations,
67 ValueType precision, std::optional<storm::solver::OptimizationDirection> dir,
68 std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
69
70 private:
71 std::shared_ptr<ValueIterationOperator<ValueType, TrivialRowGrouping>> viOperator;
73 std::vector<ValueType> guessLower, guessUpper;
74 gviinternal::IndexType selectRowGroupToGuess(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX);
75
76 template<OptimizationDirection Dir>
77 SolverStatus solveEquations(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, uint64_t& numIterations,
78 ValueType precision, std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
79
80 template<OptimizationDirection Dir>
81 void applyInPlace(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, GVIBackend<ValueType, Dir>& backend);
82
83 template<OptimizationDirection Dir>
84 std::pair<gviinternal::VerifyResult, SolverStatus> tryVerify(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX,
85 const std::vector<ValueType>& b, uint64_t& numIterations,
86 gviinternal::IndexType rowGroupToGuess, ValueType guessValue, ValueType precision,
87 std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
88
89 template<OptimizationDirection Dir>
90 SolverStatus doIterations(std::vector<ValueType>& lowerX, std::vector<ValueType>& upperX, const std::vector<ValueType>& b, uint64_t& numIterations,
91 std::optional<uint64_t> maxIterations, const ValueType& precision,
92 std::function<SolverStatus(GVIData<ValueType> const&)> const& iterationCallback);
93};
94} // namespace storm::solver::helper
SolverStatus solveEquations(std::vector< ValueType > &lowerX, std::vector< ValueType > &upperX, const std::vector< ValueType > &b, uint64_t &numIterations, ValueType precision, std::optional< storm::solver::OptimizationDirection > dir, std::function< SolverStatus(GVIData< ValueType > const &)> const &iterationCallback)
This class represents the Value Iteration Operator (also known as Bellman operator).
ValueType getSumLength(std::vector< ValueType > &lower, std::vector< ValueType > &upper) const
ValueType getMaxLength(std::vector< ValueType > &lower, std::vector< ValueType > &upper) const
IndexType selectRowGroupToGuess(const std::vector< ValueType > &lowerX, const std::vector< ValueType > &upperX)
A class that holds a possibly non-square matrix in the compressed row storage format.
std::vector< ValueType > const & x
std::vector< ValueType > const & y