|
| virtual | ~AbstractModelChecker () |
| |
| virtual std::string | getClassName () const |
| | Returns the name of the model checker class (e.g., for display in error messages).
|
| |
| virtual bool | canHandle (CheckTask< storm::logic::Formula, SolutionType > const &checkTask) const =0 |
| | Determines whether the model checker can handle the given verification task.
|
| |
| virtual std::unique_ptr< CheckResult > | check (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask) |
| | Checks the provided formula.
|
| |
| std::unique_ptr< CheckResult > | check (CheckTask< storm::logic::Formula, SolutionType > const &checkTask) |
| | Checks the provided formula with the default environment.
|
| |
| virtual std::unique_ptr< CheckResult > | computeProbabilities (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeConditionalProbabilities (Environment const &env, CheckTask< storm::logic::ConditionalFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeBoundedUntilProbabilities (Environment const &env, CheckTask< storm::logic::BoundedUntilFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeReachabilityProbabilities (Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeGloballyProbabilities (Environment const &env, CheckTask< storm::logic::GloballyFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeNextProbabilities (Environment const &env, CheckTask< storm::logic::NextFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeUntilProbabilities (Environment const &env, CheckTask< storm::logic::UntilFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeHOAPathProbabilities (Environment const &env, CheckTask< storm::logic::HOAPathFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeLTLProbabilities (Environment const &env, CheckTask< storm::logic::PathFormula, SolutionType > const &checkTask) |
| |
| std::unique_ptr< CheckResult > | computeStateFormulaProbabilities (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeRewards (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 > | computeCumulativeRewards (Environment const &env, CheckTask< storm::logic::CumulativeRewardFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeInstantaneousRewards (Environment const &env, CheckTask< storm::logic::InstantaneousRewardFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeReachabilityRewards (Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeTotalRewards (Environment const &env, CheckTask< storm::logic::TotalRewardFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeLongRunAverageRewards (Environment const &env, CheckTask< storm::logic::LongRunAverageRewardFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeLongRunAverageProbabilities (Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeTimes (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | computeReachabilityTimes (Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkStateFormula (Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkAtomicExpressionFormula (Environment const &env, CheckTask< storm::logic::AtomicExpressionFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkAtomicLabelFormula (Environment const &env, CheckTask< storm::logic::AtomicLabelFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkBinaryBooleanStateFormula (Environment const &env, CheckTask< storm::logic::BinaryBooleanStateFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkBooleanLiteralFormula (Environment const &env, CheckTask< storm::logic::BooleanLiteralFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkProbabilityOperatorFormula (Environment const &env, CheckTask< storm::logic::ProbabilityOperatorFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkRewardOperatorFormula (Environment const &env, CheckTask< storm::logic::RewardOperatorFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkTimeOperatorFormula (Environment const &env, CheckTask< storm::logic::TimeOperatorFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkLongRunAverageOperatorFormula (Environment const &env, CheckTask< storm::logic::LongRunAverageOperatorFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkUnaryBooleanStateFormula (Environment const &env, CheckTask< storm::logic::UnaryBooleanStateFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkMultiObjectiveFormula (Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkQuantileFormula (Environment const &env, CheckTask< storm::logic::QuantileFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkLexObjectiveFormula (Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask) |
| |
| virtual std::unique_ptr< CheckResult > | checkGameFormula (Environment const &env, CheckTask< storm::logic::GameFormula, SolutionType > const &checkTask) |
| |
template<typename ModelType>
class storm::modelchecker::AbstractModelChecker< ModelType >
Definition at line 17 of file AbstractModelChecker.h.
