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>
179 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << rewardFormula <<
"' is invalid.");
182template<
typename ModelType>
186 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
189template<
typename ModelType>
193 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
196template<
typename ModelType>
200 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
203template<
typename ModelType>
207 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
210template<
typename ModelType>
214 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
217template<
typename ModelType>
221 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
224template<
typename ModelType>
228 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
231template<
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>
284 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << stateFormula <<
"' is invalid.");
287template<
typename ModelType>
291 std::stringstream stream;
296template<
typename ModelType>
300 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
303template<
typename ModelType>
308 storm::exceptions::InvalidArgumentException,
"The given formula is invalid.");
310 std::unique_ptr<CheckResult> leftResult =
312 std::unique_ptr<CheckResult> rightResult =
315 STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException,
316 "Expected qualitative results.");
318 if (stateFormula.
isAnd()) {
319 leftResult->asQualitativeCheckResult() &= rightResult->asQualitativeCheckResult();
320 }
else if (stateFormula.
isOr()) {
321 leftResult->asQualitativeCheckResult() |= rightResult->asQualitativeCheckResult();
323 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << stateFormula <<
"' is invalid.");
329template<
typename ModelType>
333 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
336template<
typename ModelType>
343 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
344 "Unable to perform comparison operation on non-quantitative result.");
351template<
typename ModelType>
358 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
359 "Unable to perform comparison operation on non-quantitative result.");
366template<
typename ModelType>
375 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
376 "Unable to perform comparison operation on non-quantitative result.");
383template<
typename ModelType>
389 std::unique_ptr<CheckResult> result =
393 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException,
394 "Unable to perform comparison operation on non-quantitative result.");
401template<
typename ModelType>
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();
410 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << stateFormula <<
"' is invalid.");
415template<
typename ModelType>
419 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
422template<
typename ModelType>
426 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
429template<
typename ModelType>
433 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
436template<
typename ModelType>
440 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
".");
127template<
typename ModelType> {
…}
120template<
typename ModelType> {
…}
102 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
"."); {
…}
98template<
typename ModelType> {
…}
95 "This model checker (" << getClassName() <<
") does not support the formula: " << checkTask.
getFormula() <<
"."); {
…}
91template<
typename ModelType> {
…}
88 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << formula <<
"' is invalid."); {
…}
58 STORM_LOG_THROW(
false, storm::exceptions::InvalidArgumentException,
"The given formula '" << formula <<
"' is invalid."); {
…}
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 > 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.
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)