Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
IntervalterationHelper.h
Go to the documentation of this file.
1#include <functional>
2#include <memory>
3#include <optional>
4#include <vector>
5
10
11namespace storm::solver::helper {
12
13template<typename ValueType>
14struct IIData {
15 std::vector<ValueType> const& x;
16 std::vector<ValueType> const& y;
18};
19
24template<typename ValueType, bool TrivialRowGrouping>
26 public:
28
29 template<OptimizationDirection Dir>
30 SolverStatus II(std::pair<std::vector<ValueType>, std::vector<ValueType>>& xy, std::vector<ValueType> const& offsets, uint64_t& numIterations,
31 bool relative, ValueType const& precision, std::function<SolverStatus(IIData<ValueType> const&)> const& iterationCallback = {},
32 std::optional<storm::storage::BitVector> const& relevantValues = {}) const;
33
34 SolverStatus II(std::vector<ValueType>& operand, std::vector<ValueType> const& offsets, uint64_t& numIterations, bool relative, ValueType const& precision,
35 std::function<void(std::vector<ValueType>&)> const& prepareLowerBounds,
36 std::function<void(std::vector<ValueType>&)> const& prepareUpperBounds, std::optional<storm::OptimizationDirection> const& dir = {},
37 std::function<SolverStatus(IIData<ValueType> const&)> const& iterationCallback = {},
38 std::optional<storm::storage::BitVector> const& relevantValues = {}) const;
39
40 SolverStatus II(std::vector<ValueType>& operand, std::vector<ValueType> const& offsets, bool relative, ValueType const& precision,
41 std::function<void(std::vector<ValueType>&)> const& prepareLowerBounds,
42 std::function<void(std::vector<ValueType>&)> const& prepareUpperBounds, std::optional<storm::OptimizationDirection> const& dir = {},
43 std::function<SolverStatus(IIData<ValueType> const&)> const& iterationCallback = {},
44 std::optional<storm::storage::BitVector> const& relevantValues = {}) const;
45
46 private:
47 std::shared_ptr<ValueIterationOperator<ValueType, TrivialRowGrouping>> viOperator;
48};
49
50} // namespace storm::solver::helper
SolverStatus II(std::pair< std::vector< ValueType >, std::vector< ValueType > > &xy, std::vector< ValueType > const &offsets, uint64_t &numIterations, bool relative, ValueType const &precision, std::function< SolverStatus(IIData< ValueType > const &)> const &iterationCallback={}, std::optional< storm::storage::BitVector > const &relevantValues={}) const
This class represents the Value Iteration Operator (also known as Bellman operator).
std::vector< ValueType > const & y
std::vector< ValueType > const & x