build_model

build_model[ValueType](
model: stormpy.io.PrismProgram | stormpy.io.JaniModel | stormpy.io.SymbolicModelDescription,
properties: stormpy.logic.Property | collections.abc.Iterable[stormpy.logic.Property] | None = None,
*,
options: stormpy.BuilderOptions | None = None,
engine: stormpy.Engine = stormpy.Engine.SPARSE,
environment: stormpy.environments.Environment | None = None,
)

Select a specialization with build_model[ValueType](...).

The default specialization is build_model[float].

Template arguments:

  • ValueType (type)

Supported specializations: build_model[float], build_model[stormpy.numbers.Rational], build_model[stormpy.numbers.RationalFunction], build_model[stormpy.numbers.Interval], build_model[stormpy.numbers.RationalInterval].

Build a model from a symbolic model description.

The engine determines the representation of the model and should match the engine later used for model_checking(): Engine.SPARSE (default) builds a sparse (explicit) model, Engine.DD and Engine.HYBRID build a symbolic model (using decision diagrams, see also build_symbolic_model()).

The value type of the model is selected via subscript, e.g. build_model[stormpy.Rational](program): float (default), Rational (exact), RationalFunction (parametric), Interval or RationalInterval (exact interval). Symbolic models do not support the interval value types.

Parameters:

  • model – Symbolic model (Prism program, Jani model or symbolic model description).

  • properties – (optional) Property or properties which should be checkable on the built model. Only the labels and reward models required by the properties are built. If None or empty (and no options are given), all labels and reward models are built.

  • options – (optional) Builder options for full control of the building process. Cannot be combined with properties. Only supported for Engine.SPARSE.

  • engine – Engine for which the model is built.

  • environment – (optional) Environment configuring the decision diagram libraries. Only supported for Engine.DD and Engine.HYBRID.

Returns:

The model in sparse representation (e.g. a sparse DTMC) or in symbolic representation (e.g. a symbolic DTMC).

Raises:

TypeError – If the value type is not supported.