Template Class StatisticalModelCheckingEngine

Inheritance Relationships

Base Type

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

Class Documentation

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

  • Whether – we are caching the previously expanded data, to re-use them and speed-up evaluation

Public Types

using ValueType = typename ModelType::ValueType
using StateType = uint32_t
using StateGeneratorType = std::conditional_t<CacheData, state_generation::StateGeneration<StateType, ValueType>, state_generation::StateGenerationCacheless<ValueType>>
using TraceExportType = std::conditional_t<CacheData, samples::CompressedStateTraceExporter, samples::UncompressedStateTraceExporter>

Public Functions

StatisticalModelCheckingEngine(const storm::storage::SymbolicModelDescription &in_model, const settings::SmcSettings &settings, const std::vector<SmcPluginInstance> &loaded_plugins = {})

Constructor for the StatisticalModelCheckingEngine.

Parameters:

  • in_model – the model to perform the evaluation on

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

  • loaded_plugins – All the plugins loaded from the model definition.

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(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(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