Template Class StatisticalModelCheckingEngine

Inheritance Relationships

Base Type

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

Class Documentation

template<typename ModelType, bool StoreExploredStates>
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, …)

  • StoreExploredStates – Boolean flag to enable the storage of the generated traces

Public Types

typedef ModelType::ValueType ValueType
typedef std::conditional_t<StoreExploredStates, uint32_t, storm::generator::CompressedState> StateType

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