Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
AbstractModelChecker.cpp
Go to the documentation of this file.
2
3#include <boost/core/typeinfo.hpp>
4
35
36namespace storm {
37namespace modelchecker {
38
39template<typename ModelType>
41 return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this)));
42}
43
44template<typename ModelType>
47 return this->check(env, checkTask);
48}
49
50template<typename ModelType>
52 storm::logic::Formula const& formula = checkTask.getFormula();
53 STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException,
54 "The model checker (" << getClassName() << ") is not able to check the formula '" << formula << "'.");
55 if (formula.isStateFormula()) {
56 return this->checkStateFormula(env, checkTask.substituteFormula(formula.asStateFormula()));
57 }
58 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
59}
61template<typename ModelType>
64 storm::logic::Formula const& formula = checkTask.getFormula();
66 if (formula.isStateFormula() || formula.hasQualitativeResult()) {
67 return this->computeStateFormulaProbabilities(env, checkTask.substituteFormula(formula));
68 }
70 if (formula.isHOAPathFormula()) {
71 return this->computeHOAPathProbabilities(env, checkTask.substituteFormula(formula.asHOAPathFormula()));
72 } else if (formula.isConditionalProbabilityFormula()) {
73 return this->computeConditionalProbabilities(env, checkTask.substituteFormula(formula.asConditionalFormula()));
74 } else if (formula.info(false).containsComplexPathFormula()) {
75 // we need to do LTL model checking
76 return this->computeLTLProbabilities(env, checkTask.substituteFormula(formula.asPathFormula()));
77 } else if (formula.isBoundedUntilFormula()) {
78 return this->computeBoundedUntilProbabilities(env, checkTask.substituteFormula(formula.asBoundedUntilFormula()));
79 } else if (formula.isReachabilityProbabilityFormula()) {
80 return this->computeReachabilityProbabilities(env, checkTask.substituteFormula(formula.asReachabilityProbabilityFormula()));
81 } else if (formula.isGloballyFormula()) {
82 return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula()));
83 } else if (formula.isUntilFormula()) {
84 return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula()));
85 } else if (formula.isNextFormula()) {
86 return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula()));
87 }
88 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
89}
91template<typename ModelType>
94 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
95 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
97
98template<typename ModelType>
101 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
102 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
103}
105template<typename ModelType>
108 storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
110 return this->computeUntilProbabilities(env, checkTask.substituteFormula(newFormula));
111}
113template<typename ModelType>
116 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
117 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
118}
119
120template<typename ModelType>
123 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
124 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
125}
126
127template<typename ModelType>
130 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
131 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
132}
133
134template<typename ModelType>
137 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
138}
139
140template<typename ModelType>
143 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
144}
145
146template<typename ModelType>
148 Environment const& env, CheckTask<storm::logic::Formula, SolutionType> const& checkTask) {
149 // recurse
150 std::unique_ptr<CheckResult> resultPointer = this->check(env, checkTask.getFormula());
151 if (resultPointer->isExplicitQualitativeCheckResult()) {
152 STORM_LOG_ASSERT(ModelType::Representation == storm::models::ModelRepresentation::Sparse, "Unexpected model type.");
153 return std::make_unique<ExplicitQuantitativeCheckResult<SolutionType>>(resultPointer->asExplicitQualitativeCheckResult());
154 } else {
155 STORM_LOG_ASSERT(resultPointer->isSymbolicQualitativeCheckResult(), "Unexpected result type.");
156 STORM_LOG_ASSERT(ModelType::Representation != storm::models::ModelRepresentation::Sparse, "Unexpected model type.");
157 auto const& qualRes = resultPointer->asSymbolicQualitativeCheckResult<storm::models::GetDdType<ModelType::Representation>::ddType>();
158 return std::make_unique<SymbolicQuantitativeCheckResult<storm::models::GetDdType<ModelType::Representation>::ddType, SolutionType>>(qualRes);
159 }
160}
161
162template<typename ModelType>
163std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeRewards(Environment const& env,
165 storm::logic::Formula const& rewardFormula = checkTask.getFormula();
166 if (rewardFormula.isCumulativeRewardFormula()) {
167 return this->computeCumulativeRewards(env, checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula()));
168 } else if (rewardFormula.isInstantaneousRewardFormula()) {
169 return this->computeInstantaneousRewards(env, checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
170 } else if (rewardFormula.isReachabilityRewardFormula()) {
171 return this->computeReachabilityRewards(env, checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula()));
172 } else if (rewardFormula.isTotalRewardFormula()) {
173 return this->computeTotalRewards(env, checkTask.substituteFormula(rewardFormula.asTotalRewardFormula()));
174 } else if (rewardFormula.isLongRunAverageRewardFormula()) {
175 return this->computeLongRunAverageRewards(env, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
176 } else if (rewardFormula.isConditionalRewardFormula()) {
177 return this->computeConditionalRewards(env, checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
178 }
179 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid.");
180}
181
182template<typename ModelType>
185 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
186 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
187}
188
189template<typename ModelType>
192 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
193 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
194}
195
196template<typename ModelType>
199 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
200 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
201}
202
203template<typename ModelType>
206 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
207 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
208}
209
210template<typename ModelType>
213 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
214 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
215}
216
217template<typename ModelType>
220 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
221 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
222}
223
224template<typename ModelType>
227 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
228 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
229}
230
231template<typename ModelType>
232std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeTimes(Environment const& env,
234 storm::logic::Formula const& timeFormula = checkTask.getFormula();
235 if (timeFormula.isReachabilityTimeFormula()) {
236 return this->computeReachabilityTimes(env, checkTask.substituteFormula(timeFormula.asReachabilityTimeFormula()));
237 }
238 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
239 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
240}
241
242template<typename ModelType>
245 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
246 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
247}
248
249template<typename ModelType>
252 storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
253 if (stateFormula.isBinaryBooleanStateFormula()) {
254 return this->checkBinaryBooleanStateFormula(env, checkTask.substituteFormula(stateFormula.asBinaryBooleanStateFormula()));
255 } else if (stateFormula.isUnaryBooleanStateFormula()) {
256 return this->checkUnaryBooleanStateFormula(env, checkTask.substituteFormula(stateFormula.asUnaryBooleanStateFormula()));
257 } else if (stateFormula.isBooleanLiteralFormula()) {
258 return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
259 } else if (stateFormula.isProbabilityOperatorFormula()) {
260 return this->checkProbabilityOperatorFormula(env, checkTask.substituteFormula(stateFormula.asProbabilityOperatorFormula()));
261 } else if (stateFormula.isRewardOperatorFormula()) {
262 return this->checkRewardOperatorFormula(env, checkTask.substituteFormula(stateFormula.asRewardOperatorFormula()));
263 } else if (stateFormula.isTimeOperatorFormula()) {
264 return this->checkTimeOperatorFormula(env, checkTask.substituteFormula(stateFormula.asTimeOperatorFormula()));
265 } else if (stateFormula.isLongRunAverageOperatorFormula()) {
266 return this->checkLongRunAverageOperatorFormula(env, checkTask.substituteFormula(stateFormula.asLongRunAverageOperatorFormula()));
267 } else if (stateFormula.isAtomicExpressionFormula()) {
268 return this->checkAtomicExpressionFormula(env, checkTask.substituteFormula(stateFormula.asAtomicExpressionFormula()));
269 } else if (stateFormula.isAtomicLabelFormula()) {
270 return this->checkAtomicLabelFormula(env, checkTask.substituteFormula(stateFormula.asAtomicLabelFormula()));
271 } else if (stateFormula.isBooleanLiteralFormula()) {
272 return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
273 } else if (stateFormula.isGameFormula()) {
274 return this->checkGameFormula(env, checkTask.substituteFormula(stateFormula.asGameFormula()));
275 } else if (stateFormula.isMultiObjectiveFormula()) {
277 return this->checkLexObjectiveFormula(env, checkTask.substituteFormula(stateFormula.asMultiObjectiveFormula()));
278 } else {
279 return this->checkMultiObjectiveFormula(env, checkTask.substituteFormula(stateFormula.asMultiObjectiveFormula()));
280 }
281 } else if (stateFormula.isQuantileFormula()) {
282 return this->checkQuantileFormula(env, checkTask.substituteFormula(stateFormula.asQuantileFormula()));
283 }
284 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
285}
286
287template<typename ModelType>
290 storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula();
291 std::stringstream stream;
292 stream << stateFormula.getExpression();
293 return this->checkAtomicLabelFormula(env, checkTask.substituteFormula(storm::logic::AtomicLabelFormula(stream.str())));
294}
295
296template<typename ModelType>
299 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
300 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
301}
302
303template<typename ModelType>
306 storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
308 storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
309
310 std::unique_ptr<CheckResult> leftResult =
311 this->check(env, checkTask.template substituteFormula<storm::logic::Formula>(stateFormula.getLeftSubformula().asStateFormula()));
312 std::unique_ptr<CheckResult> rightResult =
313 this->check(env, checkTask.template substituteFormula<storm::logic::Formula>(stateFormula.getRightSubformula().asStateFormula()));
314
315 STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException,
316 "Expected qualitative results.");
317
318 if (stateFormula.isAnd()) {
319 leftResult->asQualitativeCheckResult() &= rightResult->asQualitativeCheckResult();
320 } else if (stateFormula.isOr()) {
321 leftResult->asQualitativeCheckResult() |= rightResult->asQualitativeCheckResult();
322 } else {
323 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
324 }
325
326 return leftResult;
327}
328
329template<typename ModelType>
332 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
333 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
334}
335
336template<typename ModelType>
339 storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
340 std::unique_ptr<CheckResult> result = this->computeProbabilities(env, checkTask.substituteFormula(stateFormula.getSubformula()));
341
342 if (checkTask.isBoundSet()) {
343 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
344 "Unable to perform comparison operation on non-quantitative result.");
345 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
346 } else {
347 return result;
348 }
349}
350
351template<typename ModelType>
354 storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
355 std::unique_ptr<CheckResult> result = this->computeRewards(env, checkTask.substituteFormula(stateFormula.getSubformula()));
356
357 if (checkTask.isBoundSet()) {
358 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
359 "Unable to perform comparison operation on non-quantitative result.");
360 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
361 } else {
362 return result;
363 }
364}
365
366template<typename ModelType>
369 storm::logic::TimeOperatorFormula const& stateFormula = checkTask.getFormula();
370 STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
371
372 std::unique_ptr<CheckResult> result = this->computeTimes(env, checkTask.substituteFormula(stateFormula.getSubformula()));
373
374 if (checkTask.isBoundSet()) {
375 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
376 "Unable to perform comparison operation on non-quantitative result.");
377 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
378 } else {
379 return result;
380 }
381}
382
383template<typename ModelType>
386 storm::logic::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula();
387 STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
388
389 std::unique_ptr<CheckResult> result =
390 this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(stateFormula.getSubformula().asStateFormula()));
391
392 if (checkTask.isBoundSet()) {
393 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
394 "Unable to perform comparison operation on non-quantitative result.");
395 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
396 } else {
397 return result;
398 }
399}
400
401template<typename ModelType>
404 storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
405 std::unique_ptr<CheckResult> subResult = this->check(env, checkTask.template substituteFormula<storm::logic::Formula>(stateFormula.getSubformula()));
406 STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result.");
407 if (stateFormula.isNot()) {
408 subResult->asQualitativeCheckResult().complement();
409 } else {
410 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
411 }
412 return subResult;
413}
414
415template<typename ModelType>
418 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
419 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
420}
421
422template<typename ModelType>
425 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
426 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
427}
428
429template<typename ModelType>
432 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
433 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
434}
435
436template<typename ModelType>
439 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
440 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
441}
442
444// Explicitly instantiate the template class.
446// Sparse
454
457
465
472
474
475// DD
500} // namespace modelchecker
501} // namespace storm
ModelCheckerEnvironment & modelchecker()
MultiObjectiveModelCheckerEnvironment & multi()
storm::expressions::Expression const & getExpression() const
Formula const & getRightSubformula() const
Formula const & getLeftSubformula() const
TotalRewardFormula & asTotalRewardFormula()
Definition Formula.cpp:429
HOAPathFormula & asHOAPathFormula()
Definition Formula.cpp:309
virtual bool isUnaryBooleanStateFormula() const
Definition Formula.cpp:48
RewardOperatorFormula & asRewardOperatorFormula()
Definition Formula.cpp:461
virtual bool isReachabilityRewardFormula() const
Definition Formula.cpp:152
virtual bool isGloballyFormula() const
Definition Formula.cpp:96
GameFormula & asGameFormula()
Definition Formula.cpp:365
virtual bool isBooleanLiteralFormula() const
Definition Formula.cpp:60
virtual bool isMultiObjectiveFormula() const
Definition Formula.cpp:28
UntilFormula & asUntilFormula()
Definition Formula.cpp:317
virtual bool isBinaryBooleanStateFormula() const
Definition Formula.cpp:44
virtual bool isNextFormula() const
Definition Formula.cpp:132
BoundedUntilFormula & asBoundedUntilFormula()
Definition Formula.cpp:325
virtual bool isInstantaneousRewardFormula() const
Definition Formula.cpp:148
static std::shared_ptr< Formula const > getTrueFormula()
Definition Formula.cpp:205
virtual bool isReachabilityTimeFormula() const
Definition Formula.cpp:164
LongRunAverageOperatorFormula & asLongRunAverageOperatorFormula()
Definition Formula.cpp:405
virtual bool isQuantileFormula() const
Definition Formula.cpp:32
virtual bool isReachabilityProbabilityFormula() const
Definition Formula.cpp:92
LongRunAverageRewardFormula & asLongRunAverageRewardFormula()
Definition Formula.cpp:445
BinaryBooleanStateFormula & asBinaryBooleanStateFormula()
Definition Formula.cpp:269
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:172
virtual bool isCumulativeRewardFormula() const
Definition Formula.cpp:144
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:453
BooleanLiteralFormula & asBooleanLiteralFormula()
Definition Formula.cpp:285
ConditionalFormula & asConditionalFormula()
Definition Formula.cpp:261
EventuallyFormula & asReachabilityTimeFormula()
Definition Formula.cpp:357
GloballyFormula & asGloballyFormula()
Definition Formula.cpp:373
AtomicExpressionFormula & asAtomicExpressionFormula()
Definition Formula.cpp:293
UnaryBooleanStateFormula & asUnaryBooleanStateFormula()
Definition Formula.cpp:277
StateFormula & asStateFormula()
Definition Formula.cpp:221
virtual bool isGameFormula() const
Definition Formula.cpp:168
virtual bool isUntilFormula() const
Definition Formula.cpp:80
QuantileFormula & asQuantileFormula()
Definition Formula.cpp:237
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:176
virtual bool isLongRunAverageRewardFormula() const
Definition Formula.cpp:156
PathFormula & asPathFormula()
Definition Formula.cpp:213
TimeOperatorFormula & asTimeOperatorFormula()
Definition Formula.cpp:413
InstantaneousRewardFormula & asInstantaneousRewardFormula()
Definition Formula.cpp:437
virtual bool isLongRunAverageOperatorFormula() const
Definition Formula.cpp:136
virtual bool isBoundedUntilFormula() const
Definition Formula.cpp:84
NextFormula & asNextFormula()
Definition Formula.cpp:397
EventuallyFormula & asReachabilityRewardFormula()
Definition Formula.cpp:341
virtual bool isHOAPathFormula() const
Definition Formula.cpp:100
virtual bool isConditionalRewardFormula() const
Definition Formula.cpp:116
virtual bool isTimeOperatorFormula() const
Definition Formula.cpp:140
virtual bool isStateFormula() const
Definition Formula.cpp:24
MultiObjectiveFormula & asMultiObjectiveFormula()
Definition Formula.cpp:229
virtual bool isTotalRewardFormula() const
Definition Formula.cpp:160
AtomicLabelFormula & asAtomicLabelFormula()
Definition Formula.cpp:301
CumulativeRewardFormula & asCumulativeRewardFormula()
Definition Formula.cpp:421
EventuallyFormula & asReachabilityProbabilityFormula()
Definition Formula.cpp:349
virtual bool isConditionalProbabilityFormula() const
Definition Formula.cpp:112
virtual bool isAtomicLabelFormula() const
Definition Formula.cpp:76
std::shared_ptr< Formula const > asSharedPointer()
Definition Formula.cpp:548
virtual bool isAtomicExpressionFormula() const
Definition Formula.cpp:72
virtual bool hasQualitativeResult() const
Definition Formula.cpp:188
FormulaInformation info(bool recurseIntoOperators=true) const
Definition Formula.cpp:201
Formula const & getSubformula() const
Formula const & getSubformula() const
virtual std::unique_ptr< CheckResult > computeProbabilities(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeCumulativeRewards(Environment const &env, CheckTask< storm::logic::CumulativeRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeGloballyProbabilities(Environment const &env, CheckTask< storm::logic::GloballyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkLongRunAverageOperatorFormula(Environment const &env, CheckTask< storm::logic::LongRunAverageOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
virtual std::unique_ptr< CheckResult > computeLTLProbabilities(Environment const &env, CheckTask< storm::logic::PathFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkRewardOperatorFormula(Environment const &env, CheckTask< storm::logic::RewardOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkAtomicLabelFormula(Environment const &env, CheckTask< storm::logic::AtomicLabelFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkQuantileFormula(Environment const &env, CheckTask< storm::logic::QuantileFormula, SolutionType > const &checkTask)
std::unique_ptr< CheckResult > computeStateFormulaProbabilities(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkUnaryBooleanStateFormula(Environment const &env, CheckTask< storm::logic::UnaryBooleanStateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkProbabilityOperatorFormula(Environment const &env, CheckTask< storm::logic::ProbabilityOperatorFormula, SolutionType > const &checkTask)
typename std::conditional< std::is_same_v< ValueType, storm::Interval >, double, ValueType >::type SolutionType
virtual std::unique_ptr< CheckResult > computeTimes(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeConditionalRewards(Environment const &env, CheckTask< storm::logic::ConditionalFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkGameFormula(Environment const &env, CheckTask< storm::logic::GameFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkTimeOperatorFormula(Environment const &env, CheckTask< storm::logic::TimeOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkStateFormula(Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeReachabilityRewards(Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkBinaryBooleanStateFormula(Environment const &env, CheckTask< storm::logic::BinaryBooleanStateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeLongRunAverageProbabilities(Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeUntilProbabilities(Environment const &env, CheckTask< storm::logic::UntilFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkLexObjectiveFormula(Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeLongRunAverageRewards(Environment const &env, CheckTask< storm::logic::LongRunAverageRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeHOAPathProbabilities(Environment const &env, CheckTask< storm::logic::HOAPathFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkMultiObjectiveFormula(Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeReachabilityProbabilities(Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeConditionalProbabilities(Environment const &env, CheckTask< storm::logic::ConditionalFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkBooleanLiteralFormula(Environment const &env, CheckTask< storm::logic::BooleanLiteralFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeRewards(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeInstantaneousRewards(Environment const &env, CheckTask< storm::logic::InstantaneousRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeNextProbabilities(Environment const &env, CheckTask< storm::logic::NextFormula, SolutionType > const &checkTask)
virtual std::string getClassName() const
Returns the name of the model checker class (e.g., for display in error messages).
virtual std::unique_ptr< CheckResult > computeReachabilityTimes(Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > checkAtomicExpressionFormula(Environment const &env, CheckTask< storm::logic::AtomicExpressionFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeTotalRewards(Environment const &env, CheckTask< storm::logic::TotalRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeBoundedUntilProbabilities(Environment const &env, CheckTask< storm::logic::BoundedUntilFormula, SolutionType > const &checkTask)
bool isBoundSet() const
Retrieves whether there is a bound with which the values for the states will be compared.
Definition CheckTask.h:219
ValueType getBoundThreshold() const
Retrieves the value of the bound (if set).
Definition CheckTask.h:226
storm::logic::ComparisonType const & getBoundComparisonType() const
Retrieves the comparison type of the bound (if set).
Definition CheckTask.h:235
CheckTask< NewFormulaType, ValueType > substituteFormula(NewFormulaType const &newFormula) const
Copies the check task from the source while replacing the formula with the new one.
Definition CheckTask.h:52
FormulaType const & getFormula() const
Retrieves the formula from this task.
Definition CheckTask.h:140
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
LabParser.cpp.
Definition cli.cpp:18