model_checking

model_checking(
model,
property: Property,
*,
only_initial_states: bool = False,
extract_scheduler: bool = False,
force_fully_observable: bool = False,
hint: ModelCheckerHint | None = None,
uncertainty_resolution_mode: UncertaintyResolutionMode | None = None,
engine: Engine | None = None,
environment: Environment | None = None,
) → CheckResult

Model check a property on a model.

Supports sparse and symbolic models, parametric models, interval models and multi-objective properties.

Parameters:

  • model – The model (sparse or symbolic).

  • property – The property (or formula) to check.

  • only_initial_states – If True, only the results for the initial states are computed. Otherwise, the results for all states are computed.

  • extract_scheduler – If True, an optimal scheduler is extracted (if supported). Only supported by the sparse engine.

  • force_fully_observable – If True, a POMDP is treated as a fully observable MDP. Must be set for POMDPs.

  • hint – (optional) Hint that may speed up the computation. Only supported by the sparse engine.

  • uncertainty_resolution_mode – How uncertainty is resolved. Required for interval models, not allowed otherwise.

  • engine – (optional) Engine to use. Defaults to the sparse engine for sparse models and the DD engine for symbolic models.

  • environment – (optional) Environment configuring the solvers. Defaults to stormpy.environments.default().

Returns:

The model checking result, e.g. an stormpy.results.ExplicitQuantitativeCheckResult. Use result[state] to get the value for a state together with its sound bounds as a stormpy.results.BoundedValue, or result.get_value(state) to get the value only.