Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MonotonicityResult.h
Go to the documentation of this file.
1#pragma once
2
3#include <map>
4#include <ostream>
5#include <set>
6
7#include <memory>
10
11namespace storm {
12namespace analysis {
13template<typename VariableType>
15 public:
19 enum class Monotonicity {
20 Incr,
21 Decr,
22 Constant,
23 Not,
24 Unknown
25 };
26
31
38 void addMonotonicityResult(VariableType var, Monotonicity mon);
39
46 void updateMonotonicityResult(VariableType var, Monotonicity mon, bool force = false);
47
54 Monotonicity getMonotonicity(VariableType var) const;
55 bool isMonotone(VariableType var) const;
56
62 std::map<VariableType, Monotonicity> getMonotonicityResult() const;
63
64 void splitBasedOnMonotonicity(std::set<VariableType> const& consideredVariables, std::set<VariableType>& monotoneIncr, std::set<VariableType>& monotoneDecr,
65 std::set<VariableType>& notMontone) const;
66
67 std::pair<std::set<VariableType>, std::set<VariableType>> splitVariables(std::set<VariableType> const& consideredVariables) const;
73 std::string toString() const;
74
78 bool isDone() const;
79
80 bool isDoneForVar(VariableType) const;
81
85 bool existsMonotonicity();
86
90 bool isAllMonotonicity() const;
91
95 void setDone(bool done = true);
96
100 void setSomewhereMonotonicity(bool done = true);
101
105 void setAllMonotonicity(bool done = true);
106
107 void setDoneForVar(VariableType);
108
109 void setDoneVariables(std::set<VariableType> doneVariables);
110
116 std::shared_ptr<MonotonicityResult<VariableType>> copy() const;
117
118 private:
119 std::map<VariableType, Monotonicity> monotonicityResult;
120 std::set<VariableType> doneVariables;
121 bool done;
122 bool somewhereMonotonicity;
123 bool allMonotonicity;
124};
125
126} // namespace analysis
127} // namespace storm
std::map< VariableType, Monotonicity > getMonotonicityResult() const
Returns the results so far.
void splitBasedOnMonotonicity(std::set< VariableType > const &consideredVariables, std::set< VariableType > &monotoneIncr, std::set< VariableType > &monotoneDecr, std::set< VariableType > &notMontone) const
Monotonicity
The results of monotonicity checking for a single Parameter Region.
@ Incr
the result is monotonically increasing
@ Unknown
the monotonicity result is unknown
@ Decr
the result is monotonically decreasing
void setDone(bool done=true)
Sets the done bool to the given truth value.
MonotonicityResult()
Constructs a new MonotonicityResult object.
void addMonotonicityResult(VariableType var, Monotonicity mon)
Adds a new variable with a given Monotonicity to the map.
void setAllMonotonicity(bool done=true)
Sets the allMonotonicity bool to the given truth value.
Monotonicity getMonotonicity(VariableType var) const
Returns the current monotonicity of a given parameter.
void setSomewhereMonotonicity(bool done=true)
Sets the somewhereMonotonicity bool to the given truth value.
void updateMonotonicityResult(VariableType var, Monotonicity mon, bool force=false)
Updates the Monotonicity of a variable based on its value so far and a new value.
std::pair< std::set< VariableType >, std::set< VariableType > > splitVariables(std::set< VariableType > const &consideredVariables) const
bool isAllMonotonicity() const
Returns if all Variables are monotone.
std::string toString() const
Constructs a string output of all variables and their corresponding Monotonicity.
std::shared_ptr< MonotonicityResult< VariableType > > copy() const
Constructs a new MonotonicityResult object that is a copy of the current one.
void setDoneVariables(std::set< VariableType > doneVariables)
bool existsMonotonicity()
Checks if there is any variable that is monotone.
bool isMonotone(VariableType var) const
bool isDone() const
Checks if the result is complete.
LabParser.cpp.
Definition cli.cpp:18