Storm 1.11.1.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
8
9namespace storm::solver::helper {
10
11template<typename ValueType, storm::OptimizationDirection Dir, bool TrivialRowGrouping>
13 public:
14 RobustSchedulerTrackingBackend(std::vector<uint64_t>& schedulerStorage, std::vector<uint64_t> const& robustIndices, bool applyUpdates)
15 : schedulerStorage(schedulerStorage), robustIndices(robustIndices), applyUpdates(applyUpdates) {
16 // intentionally empty
17 }
19 isConverged = true;
20 }
21
22 void processRobustRow(ValueType&& value, uint64_t row, std::vector<std::pair<ValueType, std::pair<ValueType, uint64_t>>> const& info) {
23 currStart = robustIndices[row];
24 for (uint64_t i = 0; i < info.size(); ++i) {
25 isConverged &= schedulerStorage[currStart + i] == info[i].second.second;
26 schedulerStorage[currStart + i] = info[i].second.second;
27 }
28 best = value;
29 }
30
31 void applyUpdate(ValueType& currValue, uint64_t /* rowGroup */) {
32 if (applyUpdates) {
33 currValue = best;
34 }
35 }
36
37 void endOfIteration() const {}
38
39 bool converged() const {
40 return isConverged;
41 }
42
43 bool constexpr abort() const {
44 return false;
45 }
46
47 private:
48 std::vector<uint64_t>& schedulerStorage;
49 std::vector<uint64_t> const& robustIndices;
50
51 ValueType best;
52
53 uint64_t currStart;
54
55 bool const applyUpdates;
56
57 bool isConverged;
58
59 std::vector<std::pair<uint64_t, ValueType>> currValues;
60};
61
65template<typename ValueType, typename SolutionType = ValueType, bool TrivialRowGrouping = false>
67 public:
72
87 bool computeScheduler(std::vector<SolutionType>& operandIn, std::vector<ValueType> const& offsets, storm::OptimizationDirection const& dir,
88 std::vector<uint64_t>& schedulerStorage, UncertaintyResolutionMode uncertaintyResolutionMode,
89 std::vector<SolutionType>* operandOut = nullptr, boost::optional<std::vector<uint64_t>> const& robustIndices = boost::none) const;
90
91 private:
95 template<storm::OptimizationDirection Dir, storm::OptimizationDirection RobustDir>
96 bool computeScheduler(std::vector<SolutionType>& operandIn, std::vector<ValueType> const& offsets, std::vector<uint64_t>& schedulerStorage,
97 std::vector<SolutionType>* operandOut, boost::optional<std::vector<uint64_t>> const& robustIndices = boost::none) const;
98
99 private:
100 std::shared_ptr<ValueIterationOperator<ValueType, TrivialRowGrouping, SolutionType>> viOperator;
101};
102
103} // namespace storm::solver::helper
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, UncertaintyResolutionMode uncertaintyResolutionMode, 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).