Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SchedulerTrackingHelper.cpp
Go to the documentation of this file.
2
7
8namespace storm::solver::helper {
9
10template<typename ValueType, storm::OptimizationDirection Dir>
12 public:
13 SchedulerTrackingBackend(std::vector<uint64_t>& schedulerStorage,
14 std::vector<typename ValueIterationOperator<ValueType, false>::IndexType> const& rowGroupIndices, bool applyUpdates)
15 : schedulerStorage(schedulerStorage), applyUpdates(applyUpdates), rowGroupIndices(rowGroupIndices) {
16 // intentionally empty
17 }
19 isConverged = true;
20 }
21
22 void firstRow(ValueType&& value, uint64_t rowGroup, uint64_t row) {
23 currChoice = row - rowGroupIndices[rowGroup];
24 best = std::move(value);
25 }
26
27 void nextRow(ValueType&& value, uint64_t rowGroup, uint64_t row) {
28 if (best &= value) {
29 currChoice = row - rowGroupIndices[rowGroup];
30 } else if (*best == value) {
31 // For rows that are equally good, we prefer the previously selected one.
32 // This is necessary, e.g., for policy iteration correctness.
33 if (uint64_t rowChoice = row - rowGroupIndices[rowGroup]; rowChoice == schedulerStorage[rowGroup]) {
34 currChoice = rowChoice;
35 }
36 }
37 }
38
39 void applyUpdate(ValueType& currValue, uint64_t rowGroup) {
40 if (applyUpdates) {
41 currValue = std::move(*best);
42 }
43 auto& choice = schedulerStorage[rowGroup];
44 if (isConverged) {
45 isConverged = choice == currChoice;
46 }
47 choice = currChoice;
48 }
49
50 void endOfIteration() const {}
51
52 bool converged() const {
53 return isConverged;
54 }
55
56 bool constexpr abort() const {
57 return false;
58 }
59
60 private:
61 std::vector<uint64_t>& schedulerStorage;
62 bool const applyUpdates;
63 std::vector<typename ValueIterationOperator<ValueType, false>::IndexType> const& rowGroupIndices;
64
65 bool isConverged;
67 uint64_t currChoice;
68};
69
70template<typename ValueType, typename SolutionType, bool TrivialRowGrouping>
76
77template<typename ValueType, typename SolutionType, bool TrivialRowGrouping>
78template<storm::OptimizationDirection Dir, storm::OptimizationDirection RobustDir>
80 std::vector<ValueType> const& offsets,
81 std::vector<uint64_t>& schedulerStorage,
82 std::vector<SolutionType>* operandOut,
83 boost::optional<std::vector<uint64_t>> const& robustIndices) const {
84 bool const applyUpdates = operandOut != nullptr;
85 if constexpr (TrivialRowGrouping && std::is_same<SolutionType, double>::value) {
86 STORM_LOG_ASSERT(robustIndices, "Tracking scheduler with trivial row grouping but no robust indices => there is no scheduler.");
87 RobustSchedulerTrackingBackend<SolutionType, RobustDir, TrivialRowGrouping> backend(schedulerStorage, *robustIndices, applyUpdates);
88 if (applyUpdates) {
89 return viOperator->template applyRobust<RobustDir>(*operandOut, operandIn, offsets, backend);
90 } else {
91 return viOperator->template applyInPlaceRobust<RobustDir>(operandIn, offsets, backend);
92 }
93 } else {
94 STORM_LOG_WARN_COND(!robustIndices, "Only tracking nondeterminism, not ordering of intervals.");
95 SchedulerTrackingBackend<SolutionType, Dir> backend(schedulerStorage, viOperator->getRowGroupIndices(), applyUpdates);
96 if (applyUpdates) {
97 return viOperator->template applyRobust<RobustDir>(*operandOut, operandIn, offsets, backend);
98 } else {
99 return viOperator->template applyInPlaceRobust<RobustDir>(operandIn, offsets, backend);
100 }
101 }
102}
103
104template<typename ValueType, typename SolutionType, bool TrivialRowGrouping>
106 std::vector<ValueType> const& offsets,
108 std::vector<uint64_t>& schedulerStorage, bool robust,
109 std::vector<SolutionType>* operandOut,
110 boost::optional<std::vector<uint64_t>> const& robustIndices) const {
111 // TODO this currently assumes antagonistic intervals <-> !TrivialRowGrouping
112 if (maximize(dir)) {
113 if (robust && !TrivialRowGrouping) {
114 return computeScheduler<storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize>(operandIn, offsets, schedulerStorage,
115 operandOut, robustIndices);
116 } else {
117 return computeScheduler<storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize>(operandIn, offsets, schedulerStorage,
118 operandOut, robustIndices);
119 }
120 } else {
121 if (robust && !TrivialRowGrouping) {
122 return computeScheduler<storm::OptimizationDirection::Minimize, OptimizationDirection::Maximize>(operandIn, offsets, schedulerStorage, operandOut,
123 robustIndices);
124 } else {
125 return computeScheduler<storm::OptimizationDirection::Minimize, OptimizationDirection::Minimize>(operandIn, offsets, schedulerStorage, operandOut,
126 robustIndices);
127 }
128 }
129}
130
135
136} // namespace storm::solver::helper
SchedulerTrackingBackend(std::vector< uint64_t > &schedulerStorage, std::vector< typename ValueIterationOperator< ValueType, false >::IndexType > const &rowGroupIndices, bool applyUpdates)
void applyUpdate(ValueType &currValue, uint64_t rowGroup)
void firstRow(ValueType &&value, uint64_t rowGroup, uint64_t row)
void nextRow(ValueType &&value, uint64_t rowGroup, uint64_t row)
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.
SchedulerTrackingHelper(std::shared_ptr< ValueIterationOperator< ValueType, TrivialRowGrouping, SolutionType > > viOperator)
Initializes this helper with the given value iteration operator.
This class represents the Value Iteration Operator (also known as Bellman operator).
Stores and manages an extremal (maximal or minimal) value.
Definition Extremum.h:15
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
bool constexpr maximize(OptimizationDirection d)