build_symbolic_model

build_symbolic_model[ValueType](
model: stormpy.io.PrismProgram | stormpy.io.JaniModel | stormpy.io.SymbolicModelDescription,
properties: stormpy.logic.Property | collections.abc.Iterable[stormpy.logic.Property] | None = None,
*,
environment: stormpy.environments.Environment | None = None,
)

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

The default specialization is build_symbolic_model[float].

Template arguments:

  • ValueType (type)

Supported specializations: build_symbolic_model[float], build_symbolic_model[stormpy.numbers.Rational], build_symbolic_model[stormpy.numbers.RationalFunction].

Build a model in symbolic representation (using decision diagrams) from a symbolic model.

The value type of the model is selected via subscript, e.g. build_symbolic_model[stormpy.Rational](program): float (default), Rational (exact) or RationalFunction (parametric). Interval value types are not supported.

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. If None, the full model is built.

  • environment – (optional) Environment configuring the decision diagram libraries. Defaults to stormpy.environments.default().

Returns:

The model in symbolic representation, e.g. a symbolic DTMC.

Raises:

TypeError – If the value type is not supported.