build_model

build_model(
dft: DFT,
*,
symmetries: DftSymmetries | None = None,
relevant_events: RelevantEvents | None = None,
environment: DftEnvironment | None = None,
) → SparseCtmc[float] | SparseCtmc[stormpy.numbers.RationalFunction] | SparseMA[float] | SparseMA[stormpy.numbers.RationalFunction]

Build state-space model (CTMC or MA) for the given DFT.

Parameters:

  • dft – DFT.

  • symmetries – (optional) symmetries in the DFT to exploit.

  • relevant_events – (optional) relevant events which should be observed.

  • environment – (optional) Environment configuring the build.

Returns:

The built model as either a CTMC or an MA.