stormvogel.stormpy_utils.model_checking

Functions

model_checking(...)

Perform model checking on a stormvogel model using stormpy.

Module Contents

stormvogel.stormpy_utils.model_checking.model_checking(model: stormvogel.model.Model, prop: str | None = None, scheduler: bool = True) → stormvogel.result.Result | stormvogel.result.ParetoResult | None

Perform model checking on a stormvogel model using stormpy.

Convert the model to stormpy, run model checking, and convert the result back. If no property string is provided, a widget for building one is displayed.

For multiobjective properties of the form multi(Pmax=? [...], ...) a ParetoResult is returned instead of a Result.

Parameters:

  • model – The stormvogel model to check.

  • prop – A property string to check, or None to display a property builder widget.

  • scheduler – Whether to extract a scheduler from the result (ignored for multiobjective).

Returns:

The model checking result, or None if no property was provided.

Raises:

RuntimeError – If the model is not stochastic.