Template Class StatisticalModelCheckingEngine

Inheritance Relationships

Base Type

  • public storm::modelchecker::AbstractModelChecker< ModelType >

Class Documentation

template<typename ModelType, typename StateType = uint32_t>
class StatisticalModelCheckingEngine : public storm::modelchecker::AbstractModelChecker<ModelType>

The implementation of the ModelChecking engine.

Template Parameters:

  • ModelType – Definition of the kind of model to evaluate (e.g. DTMC, MDP, …)

  • StateType – Variable type used to identify the states in the model

Public Types

typedef ModelType::ValueType ValueType
typedef StateType ActionType

Public Functions

StatisticalModelCheckingEngine(const storm::storage::SymbolicModelDescription &in_model, const settings::SmcSettings &settings)

Constructor for the StatisticalModelCheckingEngine.

Parameters:

  • in_model – the model to perform the evaluation on

  • settings – A collection of settings, used to configure the engine

virtual bool canHandle(const storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> &check_task) const override

Check if the provided property is supported by the engine.

Parameters:

check_task – The property to verify

Returns:

true if the property can be handled, false otherwise

virtual std::unique_ptr<storm::modelchecker::CheckResult> computeProbabilities([[maybe_unused]] const storm::Environment &env, const storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> &check_task) override

Evaluate the loaded model on a P property.

Parameters:

  • env – Variable carrying information for other Model Checkers in STORM. Unused here.

  • check_task – The property to verify

Returns:

The result of the evaluation

virtual std::unique_ptr<storm::modelchecker::CheckResult> computeReachabilityRewards([[maybe_unused]] const storm::Environment &env, const storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, ValueType> &check_task) override

Evaluate the loaded model on a R property.

Parameters:

  • env – Variable carrying information for other Model Checkers in STORM. Unused here.

  • check_task – The property to verify

Returns:

The result of the evaluation

Public Static Functions

static bool canHandleStatic(const storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> &check_task)

Static version of the engine’s compatibility check for the provided property.

Parameters:

check_task – The property to verify

Returns:

true if the property can be handled, false otherwise