Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
LocalMonotonicityResult.h
Go to the documentation of this file.
1#ifndef STORM_LOCALMONOTONICITYRESULT_H
2#define STORM_LOCALMONOTONICITYRESULT_H
3
4#include <vector>
8
9namespace storm {
10namespace analysis {
11template<typename VariableType>
13 public:
15
22 LocalMonotonicityResult(uint_fast64_t numberOfStates);
23
24 LocalMonotonicityResult(std::shared_ptr<MonotonicityResult<VariableType>> globalResult, uint_fast64_t numberOfStates);
25
33 Monotonicity getMonotonicity(uint_fast64_t state, VariableType var) const;
34 std::shared_ptr<MonotonicityResult<VariableType>> getMonotonicity(uint_fast64_t state) const;
35
43 void setMonotonicity(uint_fast64_t state, VariableType var, Monotonicity mon);
44
50 std::shared_ptr<MonotonicityResult<VariableType>> getGlobalMonotonicityResult() const;
51
57 std::shared_ptr<LocalMonotonicityResult<VariableType>> copy();
58
64 bool isDone() const;
65 void setDone(bool done = true);
66
67 bool isNoMonotonicity() const;
68
69 void setConstant(uint_fast64_t state);
70
71 void setIndexMinimize(int index);
72 void setIndexMaximize(int index);
73 int getIndexMinimize() const;
74 int getIndexMaximize() const;
75
80 std::string toString() const;
81
82 void setMonotoneIncreasing(VariableType var);
83 void setMonotoneDecreasing(VariableType var);
84
85 bool isFixedParametersSet() const;
86
87 private:
88 std::vector<std::shared_ptr<MonotonicityResult<VariableType>>> stateMonRes;
89
90 std::shared_ptr<MonotonicityResult<VariableType>> globalMonotonicityResult;
91
92 void setMonotonicityResult(uint_fast64_t state, std::shared_ptr<MonotonicityResult<VariableType>> monRes);
93
94 void setGlobalMonotonicityResult(std::shared_ptr<MonotonicityResult<VariableType>> monRes);
95
96 void setStatesMonotone(storm::storage::BitVector statesMonotone);
97
98 storm::storage::BitVector statesMonotone;
99 bool done;
100
101 int indexMinimize = -1;
102 int indexMaximize = -1;
103 std::shared_ptr<MonotonicityResult<VariableType>> dummyPointer;
104
105 bool setFixedParameters = false;
106};
107} // namespace analysis
108} // namespace storm
109
110#endif // STORM_LOCALMONOTONICITYRESULT_H
void setMonotonicity(uint_fast64_t state, VariableType var, Monotonicity mon)
Sets the local Monotonicity of a parameter at a given state.
MonotonicityResult< VariableType >::Monotonicity Monotonicity
std::shared_ptr< LocalMonotonicityResult< VariableType > > copy()
Constructs a new LocalMonotonicityResult object that is a copy of the current one.
bool isDone() const
Checks if the LocalMonotonicity is done yet.
std::shared_ptr< MonotonicityResult< VariableType > > getGlobalMonotonicityResult() const
Returns the Global MonotonicityResult object that corresponds to this object.
std::string toString() const
Constructs a string output of all variables and their corresponding Monotonicity.
Monotonicity getMonotonicity(uint_fast64_t state, VariableType var) const
Returns the local Monotonicity of a parameter at a given state.
Monotonicity
The results of monotonicity checking for a single Parameter Region.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
LabParser.cpp.
Definition cli.cpp:18