#include <AbstractModelChecker.h>

Inheritance diagram for storm::modelchecker::AbstractModelChecker< ModelType >:

[legend]

Public Types
typedef ModelType::ValueType	ValueType
using	SolutionType = typename GetSolutionType<ValueType, void>::type

Public Member Functions
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 >	computeDiscountedCumulativeRewards (Environment const &env, CheckTask< storm::logic::DiscountedCumulativeRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeDiscountedTotalRewards (Environment const &env, CheckTask< storm::logic::DiscountedTotalRewardFormula, 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)

Detailed Description

template<typename ModelType>
class storm::modelchecker::AbstractModelChecker< ModelType >

Definition at line 17 of file AbstractModelChecker.h.

Member Typedef Documentation

◆ SolutionType

template<typename ModelType>

using storm::modelchecker::AbstractModelChecker< ModelType >::SolutionType = typename GetSolutionType<ValueType, void>::type

Definition at line 42 of file AbstractModelChecker.h.

◆ ValueType

template<typename ModelType>

typedef ModelType::ValueType storm::modelchecker::AbstractModelChecker< ModelType >::ValueType

Definition at line 41 of file AbstractModelChecker.h.

Constructor & Destructor Documentation

◆ ~AbstractModelChecker()

template<typename ModelType>

virtual storm::modelchecker::AbstractModelChecker< ModelType >::~AbstractModelChecker ( )

inlinevirtual

Definition at line 37 of file AbstractModelChecker.h.

Member Function Documentation

◆ canHandle()

template<typename ModelType>

virtual bool storm::modelchecker::AbstractModelChecker< ModelType >::canHandle ( CheckTask< storm::logic::Formula, SolutionType > const & checkTask ) const

pure virtual

Determines whether the model checker can handle the given verification task.

If this method returns false, the task must not be checked using this model checker.

Parameters

checkTask The task for which to check whether the model checker can handle it.

Returns: True iff the model checker can check the given task.

◆ check() [1/2]

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::check ( CheckTask< storm::logic::Formula, SolutionType > const & checkTask )

Checks the provided formula with the default environment.

TODO This function is obsolete as soon as the Environment is fully integrated.

Definition at line 43 of file AbstractModelChecker.cpp.

◆ check() [2/2]

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::check	(	Environment const &	env,
		CheckTask< storm::logic::Formula, SolutionType > const &	checkTask )

virtual

Checks the provided formula.

Parameters

checkTask The verification task to pursue.

Returns: The verification result.

Definition at line 49 of file AbstractModelChecker.cpp.

◆ checkAtomicExpressionFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkAtomicExpressionFormula	(	Environment const &	env,
		CheckTask< storm::logic::AtomicExpressionFormula, SolutionType > const &	checkTask )

virtual

Definition at line 306 of file AbstractModelChecker.cpp.

◆ checkAtomicLabelFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkAtomicLabelFormula	(	Environment const &	env,
		CheckTask< storm::logic::AtomicLabelFormula, SolutionType > const &	checkTask )

virtual

Definition at line 315 of file AbstractModelChecker.cpp.

◆ checkBinaryBooleanStateFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkBinaryBooleanStateFormula	(	Environment const &	env,
		CheckTask< storm::logic::BinaryBooleanStateFormula, SolutionType > const &	checkTask )

virtual

Definition at line 322 of file AbstractModelChecker.cpp.

◆ checkBooleanLiteralFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkBooleanLiteralFormula	(	Environment const &	env,
		CheckTask< storm::logic::BooleanLiteralFormula, SolutionType > const &	checkTask )

virtual

Definition at line 348 of file AbstractModelChecker.cpp.

◆ checkGameFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkGameFormula	(	Environment const &	env,
		CheckTask< storm::logic::GameFormula, SolutionType > const &	checkTask )

virtual

Definition at line 455 of file AbstractModelChecker.cpp.

◆ checkLexObjectiveFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkLexObjectiveFormula	(	Environment const &	env,
		CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &	checkTask )

virtual

Definition at line 434 of file AbstractModelChecker.cpp.

◆ checkLongRunAverageOperatorFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkLongRunAverageOperatorFormula	(	Environment const &	env,
		CheckTask< storm::logic::LongRunAverageOperatorFormula, SolutionType > const &	checkTask )

virtual

Definition at line 402 of file AbstractModelChecker.cpp.

◆ checkMultiObjectiveFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkMultiObjectiveFormula	(	Environment const &	env,
		CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &	checkTask )

virtual

Definition at line 441 of file AbstractModelChecker.cpp.

◆ checkProbabilityOperatorFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkProbabilityOperatorFormula	(	Environment const &	env,
		CheckTask< storm::logic::ProbabilityOperatorFormula, SolutionType > const &	checkTask )

virtual

Definition at line 355 of file AbstractModelChecker.cpp.

◆ checkQuantileFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkQuantileFormula	(	Environment const &	env,
		CheckTask< storm::logic::QuantileFormula, SolutionType > const &	checkTask )

virtual

Definition at line 448 of file AbstractModelChecker.cpp.

◆ checkRewardOperatorFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkRewardOperatorFormula	(	Environment const &	env,
		CheckTask< storm::logic::RewardOperatorFormula, SolutionType > const &	checkTask )

virtual

Definition at line 370 of file AbstractModelChecker.cpp.

◆ checkStateFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkStateFormula	(	Environment const &	env,
		CheckTask< storm::logic::StateFormula, SolutionType > const &	checkTask )

virtual

Definition at line 266 of file AbstractModelChecker.cpp.

◆ checkTimeOperatorFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkTimeOperatorFormula	(	Environment const &	env,
		CheckTask< storm::logic::TimeOperatorFormula, SolutionType > const &	checkTask )

virtual

Definition at line 385 of file AbstractModelChecker.cpp.

◆ checkUnaryBooleanStateFormula()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::checkUnaryBooleanStateFormula	(	Environment const &	env,
		CheckTask< storm::logic::UnaryBooleanStateFormula, SolutionType > const &	checkTask )

virtual

Definition at line 420 of file AbstractModelChecker.cpp.

◆ computeBoundedUntilProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeBoundedUntilProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::BoundedUntilFormula, SolutionType > const &	checkTask )

virtual

Definition at line 90 of file AbstractModelChecker.cpp.

◆ computeConditionalProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeConditionalProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::ConditionalFormula, SolutionType > const &	checkTask )

virtual

Definition at line 97 of file AbstractModelChecker.cpp.

◆ computeConditionalRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeConditionalRewards	(	Environment const &	env,
		CheckTask< storm::logic::ConditionalFormula, SolutionType > const &	checkTask )

virtual

Definition at line 185 of file AbstractModelChecker.cpp.

◆ computeCumulativeRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeCumulativeRewards	(	Environment const &	env,
		CheckTask< storm::logic::CumulativeRewardFormula, SolutionType > const &	checkTask )

virtual

Definition at line 192 of file AbstractModelChecker.cpp.

◆ computeDiscountedCumulativeRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeDiscountedCumulativeRewards	(	Environment const &	env,
		CheckTask< storm::logic::DiscountedCumulativeRewardFormula, SolutionType > const &	checkTask )

virtual

Definition at line 234 of file AbstractModelChecker.cpp.

◆ computeDiscountedTotalRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeDiscountedTotalRewards	(	Environment const &	env,
		CheckTask< storm::logic::DiscountedTotalRewardFormula, SolutionType > const &	checkTask )

virtual

Definition at line 241 of file AbstractModelChecker.cpp.

◆ computeGloballyProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeGloballyProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::GloballyFormula, SolutionType > const &	checkTask )

virtual

Definition at line 112 of file AbstractModelChecker.cpp.

◆ computeHOAPathProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeHOAPathProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::HOAPathFormula, SolutionType > const &	checkTask )

virtual

Definition at line 133 of file AbstractModelChecker.cpp.

◆ computeInstantaneousRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeInstantaneousRewards	(	Environment const &	env,
		CheckTask< storm::logic::InstantaneousRewardFormula, SolutionType > const &	checkTask )

virtual

Definition at line 199 of file AbstractModelChecker.cpp.

◆ computeLongRunAverageProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeLongRunAverageProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::StateFormula, SolutionType > const &	checkTask )

virtual

Definition at line 227 of file AbstractModelChecker.cpp.

◆ computeLongRunAverageRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeLongRunAverageRewards	(	Environment const &	env,
		CheckTask< storm::logic::LongRunAverageRewardFormula, SolutionType > const &	checkTask )

virtual

Definition at line 220 of file AbstractModelChecker.cpp.

◆ computeLTLProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeLTLProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::PathFormula, SolutionType > const &	checkTask )

virtual

Definition at line 139 of file AbstractModelChecker.cpp.

◆ computeNextProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeNextProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::NextFormula, SolutionType > const &	checkTask )

virtual

Definition at line 119 of file AbstractModelChecker.cpp.

◆ computeProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::Formula, SolutionType > const &	checkTask )

virtual

Definition at line 60 of file AbstractModelChecker.cpp.

◆ computeReachabilityProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeReachabilityProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::EventuallyFormula, SolutionType > const &	checkTask )

virtual

Definition at line 104 of file AbstractModelChecker.cpp.

◆ computeReachabilityRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeReachabilityRewards	(	Environment const &	env,
		CheckTask< storm::logic::EventuallyFormula, SolutionType > const &	checkTask )

virtual

Definition at line 206 of file AbstractModelChecker.cpp.

◆ computeReachabilityTimes()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeReachabilityTimes	(	Environment const &	env,
		CheckTask< storm::logic::EventuallyFormula, SolutionType > const &	checkTask )

virtual

Definition at line 259 of file AbstractModelChecker.cpp.

◆ computeRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeRewards	(	Environment const &	env,
		CheckTask< storm::logic::Formula, SolutionType > const &	checkTask )

virtual

Definition at line 161 of file AbstractModelChecker.cpp.

◆ computeStateFormulaProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeStateFormulaProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::Formula, SolutionType > const &	checkTask )

Definition at line 145 of file AbstractModelChecker.cpp.

◆ computeTimes()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeTimes	(	Environment const &	env,
		CheckTask< storm::logic::Formula, SolutionType > const &	checkTask )

virtual

Definition at line 248 of file AbstractModelChecker.cpp.

◆ computeTotalRewards()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeTotalRewards	(	Environment const &	env,
		CheckTask< storm::logic::TotalRewardFormula, SolutionType > const &	checkTask )

virtual

Definition at line 213 of file AbstractModelChecker.cpp.

◆ computeUntilProbabilities()

template<typename ModelType>

std::unique_ptr< CheckResult > storm::modelchecker::AbstractModelChecker< ModelType >::computeUntilProbabilities	(	Environment const &	env,
		CheckTask< storm::logic::UntilFormula, SolutionType > const &	checkTask )

virtual

Definition at line 126 of file AbstractModelChecker.cpp.

◆ getClassName()

template<typename ModelType>

std::string storm::modelchecker::AbstractModelChecker< ModelType >::getClassName ( ) const

virtual

Returns the name of the model checker class (e.g., for display in error messages).

Definition at line 38 of file AbstractModelChecker.cpp.

The documentation for this class was generated from the following files:

src/storm/modelchecker/AbstractModelChecker.h
src/storm/modelchecker/AbstractModelChecker.cpp

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ SolutionType

◆ ValueType

Constructor & Destructor Documentation

◆ ~AbstractModelChecker()

Member Function Documentation

◆ canHandle()

◆ check() [1/2]

◆ check() [2/2]

◆ checkAtomicExpressionFormula()

◆ checkAtomicLabelFormula()

◆ checkBinaryBooleanStateFormula()

◆ checkBooleanLiteralFormula()

◆ checkGameFormula()

◆ checkLexObjectiveFormula()

◆ checkLongRunAverageOperatorFormula()

◆ checkMultiObjectiveFormula()

◆ checkProbabilityOperatorFormula()

◆ checkQuantileFormula()

◆ checkRewardOperatorFormula()

◆ checkStateFormula()

◆ checkTimeOperatorFormula()

◆ checkUnaryBooleanStateFormula()

◆ computeBoundedUntilProbabilities()

◆ computeConditionalProbabilities()

◆ computeConditionalRewards()

◆ computeCumulativeRewards()

◆ computeDiscountedCumulativeRewards()

◆ computeDiscountedTotalRewards()

◆ computeGloballyProbabilities()

◆ computeHOAPathProbabilities()

◆ computeInstantaneousRewards()

◆ computeLongRunAverageProbabilities()

◆ computeLongRunAverageRewards()

◆ computeLTLProbabilities()

◆ computeNextProbabilities()

◆ computeProbabilities()

◆ computeReachabilityProbabilities()

◆ computeReachabilityRewards()

◆ computeReachabilityTimes()

◆ computeRewards()

◆ computeStateFormulaProbabilities()

◆ computeTimes()

◆ computeTotalRewards()

◆ computeUntilProbabilities()

◆ getClassName()