3#include <boost/core/typeinfo.hpp>
37namespace modelchecker {
39template<
typename ModelType>
41 return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*
this)));
44template<
typename ModelType>
47 return this->check(env, checkTask);
50template<
typename ModelType>
53 STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException,
54 "The model checker (" << getClassName() <<
") is not able to check the formula '" << formula <<
"'.");
58 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << formula <<
"' is invalid.");
61template<
typename ModelType>
88 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << formula <<
"' is invalid.");
91template<
typename ModelType>
95 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
98template<
typename ModelType>
102 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
105template<
typename ModelType>
113template<
typename ModelType>
117 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
120template<
typename ModelType>
124 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
127template<
typename ModelType>
131 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
134template<
typename ModelType>
137 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"This model checker does not support the formula: " << checkTask.
getFormula() <<
".");
140template<
typename ModelType>
143 STORM_LOG_THROW(
false, storm::exceptions::NotImplementedException,
"This model checker does not support the formula: " << checkTask.
getFormula() <<
".");
146template<
typename ModelType>
150 std::unique_ptr<CheckResult> resultPointer = this->check(env, checkTask.
getFormula());
151 if (resultPointer->isExplicitQualitativeCheckResult()) {
153 return std::make_unique<ExplicitQuantitativeCheckResult<SolutionType>>(resultPointer->asExplicitQualitativeCheckResult());
155 STORM_LOG_ASSERT(resultPointer->isSymbolicQualitativeCheckResult(),
"Unexpected result type.");
158 return std::make_unique<SymbolicQuantitativeCheckResult<storm::models::GetDdType<ModelType::Representation>::ddType,
SolutionType>>(qualRes);
162template<
typename ModelType>
183 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << rewardFormula <<
"' is invalid.");
186template<
typename ModelType>
190 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
193template<
typename ModelType>
197 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
200template<
typename ModelType>
204 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
207template<
typename ModelType>
211 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
214template<
typename ModelType>
218 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
221template<
typename ModelType>
225 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
228template<
typename ModelType>
232 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
235template<
typename ModelType>
239 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
242template<
typename ModelType>
246 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
249template<
typename ModelType>
257 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
260template<
typename ModelType>
264 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
267template<
typename ModelType>
302 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << stateFormula <<
"' is invalid.");
305template<
typename ModelType>
309 std::stringstream stream;
314template<
typename ModelType>
318 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
321template<
typename ModelType>
326 storm::exceptions::InvalidArgumentException,
"The given formula is invalid.");
328 std::unique_ptr<CheckResult> leftResult =
330 std::unique_ptr<CheckResult> rightResult =
333 STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException,
334 "Expected qualitative results.");
336 if (stateFormula.
isAnd()) {
337 leftResult->asQualitativeCheckResult() &= rightResult->asQualitativeCheckResult();
338 }
else if (stateFormula.
isOr()) {
339 leftResult->asQualitativeCheckResult() |= rightResult->asQualitativeCheckResult();
341 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << stateFormula <<
"' is invalid.");
347template<
typename ModelType>
351 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
354template<
typename ModelType>
361 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
362 "Unable to perform comparison operation on non-quantitative result.");
369template<
typename ModelType>
376 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
377 "Unable to perform comparison operation on non-quantitative result.");
384template<
typename ModelType>
393 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
394 "Unable to perform comparison operation on non-quantitative result.");
401template<
typename ModelType>
407 std::unique_ptr<CheckResult> result =
411 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
412 "Unable to perform comparison operation on non-quantitative result.");
419template<
typename ModelType>
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();
428 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << stateFormula <<
"' is invalid.");
433template<
typename ModelType>
437 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
440template<
typename ModelType>
444 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
447template<
typename ModelType>
451 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
454template<
typename ModelType>
458 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
ModelCheckerEnvironment & modelchecker()
MultiObjectiveModelCheckerEnvironment & multi()
bool isLexicographicModelCheckingSet() 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.
ValueType getBoundThreshold() const
Retrieves the value of the bound (if set).
storm::logic::ComparisonType const & getBoundComparisonType() const
Retrieves the comparison type of the bound (if set).
CheckTask< NewFormulaType, ValueType > substituteFormula(NewFormulaType const &newFormula) const
Copies the check task from the source while replacing the formula with the new one.
FormulaType const & getFormula() const
Retrieves the formula from this task.
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
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)