Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
MinMaxLinearEquationSolverRequirements.cpp
Go to the documentation of this file.
2
5
6namespace storm {
7namespace solver {
8
10 : lowerBoundsRequirement(linearEquationSolverRequirements.lowerBounds()), upperBoundsRequirement(linearEquationSolverRequirements.upperBounds()) {
11 // Intentionally left empty.
12}
13
15 acyclicRequirement.enable(critical);
16 return *this;
17}
18
20 uniqueSolutionRequirement.enable(critical);
21 return *this;
22}
23
25 validInitialSchedulerRequirement.enable(critical);
26 return *this;
27}
28
30 lowerBoundsRequirement.enable(critical);
31 return *this;
32}
33
35 upperBoundsRequirement.enable(critical);
36 return *this;
37}
38
44
46 return acyclicRequirement;
47}
48
50 return uniqueSolutionRequirement;
51}
52
54 return validInitialSchedulerRequirement;
55}
56
58 return lowerBoundsRequirement;
59}
60
62 return upperBoundsRequirement;
63}
64
66 switch (element) {
68 return acyclic();
69 break;
71 return uniqueSolution();
72 break;
74 return validInitialScheduler();
75 break;
77 return lowerBounds();
78 break;
80 return upperBounds();
81 break;
82 }
83 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown ElementType");
84}
85
87 acyclicRequirement.clear();
88}
89
91 uniqueSolutionRequirement.clear();
92}
93
95 validInitialSchedulerRequirement.clear();
96}
97
99 lowerBoundsRequirement.clear();
100}
101
103 upperBoundsRequirement.clear();
104}
105
110
112 return acyclicRequirement || uniqueSolutionRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement;
113}
114
116 return acyclicRequirement.isCritical() || uniqueSolutionRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() ||
117 lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical();
118}
119
121 std::string res = "[";
122 bool first = true;
123 if (acyclic()) {
124 if (!first) {
125 res += ", ";
126 } else {
127 first = false;
128 }
129 res += "Acyclic";
130 if (acyclic().isCritical()) {
131 res += "(mandatory)";
132 }
133 }
134 if (uniqueSolution()) {
135 if (!first) {
136 res += ", ";
137 } else {
138 first = false;
139 }
140 res += "UniqueSolution";
141 if (uniqueSolution().isCritical()) {
142 res += "(mandatory)";
143 }
144 }
145 if (validInitialScheduler()) {
146 if (!first) {
147 res += ", ";
148 } else {
149 first = false;
150 }
151 res += "validInitialScheduler";
152 if (validInitialScheduler().isCritical()) {
153 res += "(mandatory)";
154 }
155 }
156 if (lowerBounds()) {
157 if (!first) {
158 res += ", ";
159 } else {
160 first = false;
161 }
162 res += "lowerBounds";
163 if (lowerBounds().isCritical()) {
164 res += "(mandatory)";
165 }
166 }
167 if (upperBounds()) {
168 if (!first) {
169 res += ", ";
170 } else {
171 first = false;
172 }
173 res += "upperBounds";
174 if (upperBounds().isCritical()) {
175 res += "(mandatory)";
176 }
177 }
178 res += "]";
179 return res;
180}
181
182} // namespace solver
183} // namespace storm
MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const &linearEquationSolverRequirements=LinearEquationSolverRequirements())
SolverRequirement const & get(Element const &element) const
MinMaxLinearEquationSolverRequirements & requireBounds(bool critical=true)
MinMaxLinearEquationSolverRequirements & requireUniqueSolution(bool critical=true)
MinMaxLinearEquationSolverRequirements & requireLowerBounds(bool critical=true)
MinMaxLinearEquationSolverRequirements & requireValidInitialScheduler(bool critical=true)
MinMaxLinearEquationSolverRequirements & requireUpperBounds(bool critical=true)
std::string getEnabledRequirementsAsString() const
Returns a string that enumerates the enabled requirements.
MinMaxLinearEquationSolverRequirements & requireAcyclic(bool critical=true)
bool isCritical() const
Returns true if the solver fails in case this requirement is not met.
void enable(bool critical=true)
Enables this requirement.
void clear()
Clears this requirement.
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
LabParser.cpp.
Definition cli.cpp:18