Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
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()) {
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}
90
91template<typename ModelType>
94 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
95 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
96}
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.isDiscountedCumulativeRewardFormula()) {
169 return this->computeDiscountedCumulativeRewards(env, checkTask.substituteFormula(rewardFormula.asDiscountedCumulativeRewardFormula()));
170 } else if (rewardFormula.isInstantaneousRewardFormula()) {
171 return this->computeInstantaneousRewards(env, checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
172 } else if (rewardFormula.isReachabilityRewardFormula()) {
173 return this->computeReachabilityRewards(env, checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula()));
174 } else if (rewardFormula.isTotalRewardFormula()) {
175 return this->computeTotalRewards(env, checkTask.substituteFormula(rewardFormula.asTotalRewardFormula()));
176 } else if (rewardFormula.isDiscountedTotalRewardFormula()) {
177 return this->computeDiscountedTotalRewards(env, checkTask.substituteFormula(rewardFormula.asDiscountedTotalRewardFormula()));
178 } else if (rewardFormula.isLongRunAverageRewardFormula()) {
179 return this->computeLongRunAverageRewards(env, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
180 } else if (rewardFormula.isConditionalRewardFormula()) {
181 return this->computeConditionalRewards(env, checkTask.substituteFormula(rewardFormula.asConditionalFormula()));
182 }
183 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid.");
184}
185
186template<typename ModelType>
189 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
190 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
191}
192
193template<typename ModelType>
196 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
197 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
198}
199
200template<typename ModelType>
203 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
204 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
205}
206
207template<typename ModelType>
210 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
211 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
212}
213
214template<typename ModelType>
217 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
218 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
219}
220
221template<typename ModelType>
224 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
225 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
226}
227
228template<typename ModelType>
231 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
232 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
233}
234
235template<typename ModelType>
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>
250std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeTimes(Environment const& env,
252 storm::logic::Formula const& timeFormula = checkTask.getFormula();
253 if (timeFormula.isReachabilityTimeFormula()) {
254 return this->computeReachabilityTimes(env, checkTask.substituteFormula(timeFormula.asReachabilityTimeFormula()));
255 }
256 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
257 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
258}
259
260template<typename ModelType>
263 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
264 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
265}
266
267template<typename ModelType>
270 storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
271 if (stateFormula.isBinaryBooleanStateFormula()) {
272 return this->checkBinaryBooleanStateFormula(env, checkTask.substituteFormula(stateFormula.asBinaryBooleanStateFormula()));
273 } else if (stateFormula.isUnaryBooleanStateFormula()) {
274 return this->checkUnaryBooleanStateFormula(env, checkTask.substituteFormula(stateFormula.asUnaryBooleanStateFormula()));
275 } else if (stateFormula.isBooleanLiteralFormula()) {
276 return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
277 } else if (stateFormula.isProbabilityOperatorFormula()) {
278 return this->checkProbabilityOperatorFormula(env, checkTask.substituteFormula(stateFormula.asProbabilityOperatorFormula()));
279 } else if (stateFormula.isRewardOperatorFormula()) {
280 return this->checkRewardOperatorFormula(env, checkTask.substituteFormula(stateFormula.asRewardOperatorFormula()));
281 } else if (stateFormula.isTimeOperatorFormula()) {
282 return this->checkTimeOperatorFormula(env, checkTask.substituteFormula(stateFormula.asTimeOperatorFormula()));
283 } else if (stateFormula.isLongRunAverageOperatorFormula()) {
284 return this->checkLongRunAverageOperatorFormula(env, checkTask.substituteFormula(stateFormula.asLongRunAverageOperatorFormula()));
285 } else if (stateFormula.isAtomicExpressionFormula()) {
286 return this->checkAtomicExpressionFormula(env, checkTask.substituteFormula(stateFormula.asAtomicExpressionFormula()));
287 } else if (stateFormula.isAtomicLabelFormula()) {
288 return this->checkAtomicLabelFormula(env, checkTask.substituteFormula(stateFormula.asAtomicLabelFormula()));
289 } else if (stateFormula.isBooleanLiteralFormula()) {
290 return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
291 } else if (stateFormula.isGameFormula()) {
292 return this->checkGameFormula(env, checkTask.substituteFormula(stateFormula.asGameFormula()));
293 } else if (stateFormula.isMultiObjectiveFormula()) {
295 return this->checkLexObjectiveFormula(env, checkTask.substituteFormula(stateFormula.asMultiObjectiveFormula()));
296 } else {
297 return this->checkMultiObjectiveFormula(env, checkTask.substituteFormula(stateFormula.asMultiObjectiveFormula()));
298 }
299 } else if (stateFormula.isQuantileFormula()) {
300 return this->checkQuantileFormula(env, checkTask.substituteFormula(stateFormula.asQuantileFormula()));
301 }
302 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
303}
304
305template<typename ModelType>
308 storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula();
309 std::stringstream stream;
310 stream << stateFormula.getExpression();
311 return this->checkAtomicLabelFormula(env, checkTask.substituteFormula(storm::logic::AtomicLabelFormula(stream.str())));
312}
313
314template<typename ModelType>
317 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
318 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
319}
320
321template<typename ModelType>
324 storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
326 storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
327
328 std::unique_ptr<CheckResult> leftResult =
329 this->check(env, checkTask.template substituteFormula<storm::logic::Formula>(stateFormula.getLeftSubformula().asStateFormula()));
330 std::unique_ptr<CheckResult> rightResult =
331 this->check(env, checkTask.template substituteFormula<storm::logic::Formula>(stateFormula.getRightSubformula().asStateFormula()));
332
333 STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException,
334 "Expected qualitative results.");
335
336 if (stateFormula.isAnd()) {
337 leftResult->asQualitativeCheckResult() &= rightResult->asQualitativeCheckResult();
338 } else if (stateFormula.isOr()) {
339 leftResult->asQualitativeCheckResult() |= rightResult->asQualitativeCheckResult();
340 } else {
341 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
342 }
343
344 return leftResult;
345}
346
347template<typename ModelType>
350 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
351 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
352}
353
354template<typename ModelType>
357 storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
358 std::unique_ptr<CheckResult> result = this->computeProbabilities(env, checkTask.substituteFormula(stateFormula.getSubformula()));
359
360 if (checkTask.isBoundSet()) {
361 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
362 "Unable to perform comparison operation on non-quantitative result.");
363 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
364 } else {
365 return result;
366 }
367}
368
369template<typename ModelType>
372 storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
373 std::unique_ptr<CheckResult> result = this->computeRewards(env, checkTask.substituteFormula(stateFormula.getSubformula()));
374
375 if (checkTask.isBoundSet()) {
376 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
377 "Unable to perform comparison operation on non-quantitative result.");
378 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
379 } else {
380 return result;
381 }
382}
383
384template<typename ModelType>
387 storm::logic::TimeOperatorFormula const& stateFormula = checkTask.getFormula();
388 STORM_LOG_THROW(stateFormula.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
389
390 std::unique_ptr<CheckResult> result = this->computeTimes(env, checkTask.substituteFormula(stateFormula.getSubformula()));
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::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula();
405 STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
406
407 std::unique_ptr<CheckResult> result =
408 this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(stateFormula.getSubformula().asStateFormula()));
409
410 if (checkTask.isBoundSet()) {
411 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
412 "Unable to perform comparison operation on non-quantitative result.");
413 return result->asQuantitativeCheckResult<SolutionType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
414 } else {
415 return result;
416 }
417}
418
419template<typename ModelType>
422 storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
423 std::unique_ptr<CheckResult> subResult = this->check(env, checkTask.template substituteFormula<storm::logic::Formula>(stateFormula.getSubformula()));
424 STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result.");
425 if (stateFormula.isNot()) {
426 subResult->asQualitativeCheckResult().complement();
427 } else {
428 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
429 }
430 return subResult;
431}
432
433template<typename ModelType>
436 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
437 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
438}
439
440template<typename ModelType>
443 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
444 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
445}
446
447template<typename ModelType>
450 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
451 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
452}
453
454template<typename ModelType>
457 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
458 "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
459}
460
462// Explicitly instantiate the template class.
464// Sparse
472
475
483
490
492
493// DD
518} // namespace modelchecker
519} // 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:437
HOAPathFormula & asHOAPathFormula()
Definition Formula.cpp:317
virtual bool isUnaryBooleanStateFormula() const
Definition Formula.cpp:48
RewardOperatorFormula & asRewardOperatorFormula()
Definition Formula.cpp:484
virtual bool isDiscountedCumulativeRewardFormula() const
Definition Formula.cpp:148
virtual bool isReachabilityRewardFormula() const
Definition Formula.cpp:156
virtual bool isGloballyFormula() const
Definition Formula.cpp:96
GameFormula & asGameFormula()
Definition Formula.cpp:373
virtual bool isBooleanLiteralFormula() const
Definition Formula.cpp:60
virtual bool isMultiObjectiveFormula() const
Definition Formula.cpp:28
UntilFormula & asUntilFormula()
Definition Formula.cpp:325
virtual bool isBinaryBooleanStateFormula() const
Definition Formula.cpp:44
virtual bool isNextFormula() const
Definition Formula.cpp:132
BoundedUntilFormula & asBoundedUntilFormula()
Definition Formula.cpp:333
virtual bool isInstantaneousRewardFormula() const
Definition Formula.cpp:152
static std::shared_ptr< Formula const > getTrueFormula()
Definition Formula.cpp:213
virtual bool isReachabilityTimeFormula() const
Definition Formula.cpp:172
LongRunAverageOperatorFormula & asLongRunAverageOperatorFormula()
Definition Formula.cpp:413
virtual bool isQuantileFormula() const
Definition Formula.cpp:32
virtual bool isReachabilityProbabilityFormula() const
Definition Formula.cpp:92
LongRunAverageRewardFormula & asLongRunAverageRewardFormula()
Definition Formula.cpp:468
BinaryBooleanStateFormula & asBinaryBooleanStateFormula()
Definition Formula.cpp:277
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:180
virtual bool isCumulativeRewardFormula() const
Definition Formula.cpp:144
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:476
DiscountedCumulativeRewardFormula & asDiscountedCumulativeRewardFormula()
Definition Formula.cpp:445
BooleanLiteralFormula & asBooleanLiteralFormula()
Definition Formula.cpp:293
ConditionalFormula & asConditionalFormula()
Definition Formula.cpp:269
EventuallyFormula & asReachabilityTimeFormula()
Definition Formula.cpp:365
GloballyFormula & asGloballyFormula()
Definition Formula.cpp:381
AtomicExpressionFormula & asAtomicExpressionFormula()
Definition Formula.cpp:301
DiscountedTotalRewardFormula & asDiscountedTotalRewardFormula()
Definition Formula.cpp:453
UnaryBooleanStateFormula & asUnaryBooleanStateFormula()
Definition Formula.cpp:285
StateFormula & asStateFormula()
Definition Formula.cpp:229
virtual bool isGameFormula() const
Definition Formula.cpp:176
virtual bool isUntilFormula() const
Definition Formula.cpp:80
QuantileFormula & asQuantileFormula()
Definition Formula.cpp:245
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:184
virtual bool isLongRunAverageRewardFormula() const
Definition Formula.cpp:160
PathFormula & asPathFormula()
Definition Formula.cpp:221
TimeOperatorFormula & asTimeOperatorFormula()
Definition Formula.cpp:421
InstantaneousRewardFormula & asInstantaneousRewardFormula()
Definition Formula.cpp:460
virtual bool isLongRunAverageOperatorFormula() const
Definition Formula.cpp:136
virtual bool isBoundedUntilFormula() const
Definition Formula.cpp:84
NextFormula & asNextFormula()
Definition Formula.cpp:405
EventuallyFormula & asReachabilityRewardFormula()
Definition Formula.cpp:349
virtual bool isHOAPathFormula() const
Definition Formula.cpp:100
virtual bool isDiscountedTotalRewardFormula() const
Definition Formula.cpp:168
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:237
virtual bool isTotalRewardFormula() const
Definition Formula.cpp:164
AtomicLabelFormula & asAtomicLabelFormula()
Definition Formula.cpp:309
CumulativeRewardFormula & asCumulativeRewardFormula()
Definition Formula.cpp:429
EventuallyFormula & asReachabilityProbabilityFormula()
Definition Formula.cpp:357
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:571
virtual bool isAtomicExpressionFormula() const
Definition Formula.cpp:72
virtual bool hasQualitativeResult() const
Definition Formula.cpp:196
FormulaInformation info(bool recurseIntoOperators=true) const
Definition Formula.cpp:209
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 > computeDiscountedCumulativeRewards(Environment const &env, CheckTask< storm::logic::DiscountedCumulativeRewardFormula, 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)
virtual std::unique_ptr< CheckResult > computeDiscountedTotalRewards(Environment const &env, CheckTask< storm::logic::DiscountedTotalRewardFormula, 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
std::unique_ptr< CheckResult > computeConditionalProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
LabParser.cpp.