Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SchedulerTrackingHelper.h
Go to the documentation of this file.
1#pragma once
2#include <memory>
3#include <vector>
4
7
8namespace storm::solver::helper {
9
10template<typename ValueType, storm::OptimizationDirection Dir, bool TrivialRowGrouping>
12 public:
13 RobustSchedulerTrackingBackend(std::vector<uint64_t>& schedulerStorage, std::vector<uint64_t> const& robustIndices, bool applyUpdates)
14 : schedulerStorage(schedulerStorage), robustIndices(robustIndices), applyUpdates(applyUpdates) {
15 // intentionally empty
16 }
18 isConverged = true;
19 }
20
21 void processRobustRow(ValueType&& value, uint64_t row, std::vector<std::pair<ValueType, std::pair<ValueType, uint64_t>>> const& info) {
22 currStart = robustIndices[row];
23 for (uint64_t i = 0; i < info.size(); ++i) {
24 isConverged &= schedulerStorage[currStart + i] == info[i].second.second;
25 schedulerStorage[currStart + i] = info[i].second.second;
26 }
27 best = value;
28 }
29
30 void applyUpdate(ValueType& currValue, uint64_t rowGroup) {
31 if (applyUpdates) {
32 currValue = best;
33 }
34 }
35
36 void endOfIteration() const {}
37
38 bool converged() const {
39 return isConverged;
40 }
41
42 bool constexpr abort() const {
43 return false;
44 }
45
46 private:
47 std::vector<uint64_t>& schedulerStorage;
48 std::vector<uint64_t> const& robustIndices;
49
50 ValueType best;
51
52 uint64_t currStart;
53
54 bool const applyUpdates;
55
56 bool isConverged;
57
58 std::vector<std::pair<uint64_t, ValueType>> currValues;
59};
60
64template<typename ValueType, typename SolutionType = ValueType, bool TrivialRowGrouping = false>
66 public:
71
86 bool computeScheduler(std::vector<SolutionType>& operandIn, std::vector<ValueType> const& offsets, storm::OptimizationDirection const& dir,
87 std::vector<uint64_t>& schedulerStorage, bool robust, std::vector<SolutionType>* operandOut = nullptr,
88 boost::optional<std::vector<uint64_t>> const& robustIndices = boost::none) const;
89
90 private:
94 template<storm::OptimizationDirection Dir, storm::OptimizationDirection RobustDir>
95 bool computeScheduler(std::vector<SolutionType>& operandIn, std::vector<ValueType> const& offsets, std::vector<uint64_t>& schedulerStorage,
96 std::vector<SolutionType>* operandOut, boost::optional<std::vector<uint64_t>> const& robustIndices = boost::none) const;
97
98 private:
99 std::shared_ptr<ValueIterationOperator<ValueType, TrivialRowGrouping, SolutionType>> viOperator;
100};
101
102} // namespace storm::solver::helper
void applyUpdate(ValueType &currValue, uint64_t rowGroup)
RobustSchedulerTrackingBackend(std::vector< uint64_t > &schedulerStorage, std::vector< uint64_t > const &robustIndices, bool applyUpdates)
void processRobustRow(ValueType &&value, uint64_t row, std::vector< std::pair< ValueType, std::pair< ValueType, uint64_t > > > const &info)
Helper class to extract optimal scheduler choices from a MinMax equation system solution.
bool computeScheduler(std::vector< SolutionType > &operandIn, std::vector< ValueType > const &offsets, storm::OptimizationDirection const &dir, std::vector< uint64_t > &schedulerStorage, bool robust, std::vector< SolutionType > *operandOut=nullptr, boost::optional< std::vector< uint64_t > > const &robustIndices=boost::none) const
Computes the optimal choices from the given solution.
This class represents the Value Iteration Operator (also known as Bellman operator).