SymbolicDtmc

class SymbolicDtmc[DdType, ValueType]

DTMC in symbolic representation

Template arguments:

• DdType (value)

• ValueType (type)

Available specializations:

• SymbolicDtmc[stormpy.models.DdType.Sylvan, float]

• SymbolicDtmc[stormpy.models.DdType.Sylvan, stormpy.numbers.Rational]

• SymbolicDtmc[stormpy.models.DdType.Sylvan, stormpy.numbers.RationalFunction]

Members

SymbolicDtmc.compute_depth(self: stormpy.models.SymbolicModel[DdType, ValueType]) → int

Computes the depth of the model, i.e., the distance to the node with the largest minimal distance from the initial states

property SymbolicDtmc.dd_manager

dd manager

SymbolicDtmc.get_parameters(

self: stormpy.models.SymbolicModel[stormpy.models.DdType.Sylvan, stormpy.numbers.RationalFunction],

) → set[stormpy.numbers.Variable]

Available only for: SymbolicDtmc[stormpy.models.DdType.Sylvan, stormpy.numbers.RationalFunction].

Get parameters

SymbolicDtmc.get_states(

self: stormpy.models.SymbolicModel[DdType, ValueType],

expression,

) → stormpy.developer.storage.Bdd[stormpy.models.DdType.Sylvan]

Get states that are described by the expression

property SymbolicDtmc.has_parameters

Flag whether model has parameters

property SymbolicDtmc.initial_states

initial states as DD

property SymbolicDtmc.is_discrete_time_model

Flag whether the model is a discrete time model

property SymbolicDtmc.is_exact

Flag whether model is exact

property SymbolicDtmc.is_nondeterministic_model

Flag whether the model contains nondeterminism

property SymbolicDtmc.is_partially_observable

Flag whether the model has observation labels

property SymbolicDtmc.is_sparse_model

Flag whether the model is stored as a sparse model

property SymbolicDtmc.is_symbolic_model

Flag whether the model is stored using decision diagrams

property SymbolicDtmc.model_type

Model type

property SymbolicDtmc.nr_choices

Number of choices

property SymbolicDtmc.nr_states

Number of states

property SymbolicDtmc.nr_transitions

Number of transitions

property SymbolicDtmc.reachable_states

reachable states as DD

SymbolicDtmc.reduce_to_state_based_rewards(

self: stormpy.models.SymbolicModel[DdType, ValueType],

) → None

property SymbolicDtmc.reward_models

Reward models

property SymbolicDtmc.supports_parameters

Flag whether model supports parameters