SymbolicMA

class SymbolicMA[DdType, ValueType]

MA in symbolic representation

Template arguments:

• DdType (value)

• ValueType (type)

Available specializations:

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

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

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

Members

SymbolicMA.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 SymbolicMA.dd_manager

dd manager

SymbolicMA.get_parameters(

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

) → set[stormpy.numbers.Variable]

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

Get parameters

SymbolicMA.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 SymbolicMA.has_parameters

Flag whether model has parameters

property SymbolicMA.initial_states

initial states as DD

property SymbolicMA.is_discrete_time_model

Flag whether the model is a discrete time model

property SymbolicMA.is_exact

Flag whether model is exact

property SymbolicMA.is_nondeterministic_model

Flag whether the model contains nondeterminism

property SymbolicMA.is_partially_observable

Flag whether the model has observation labels

property SymbolicMA.is_sparse_model

Flag whether the model is stored as a sparse model

property SymbolicMA.is_symbolic_model

Flag whether the model is stored using decision diagrams

property SymbolicMA.model_type

Model type

property SymbolicMA.nr_choices

Number of choices

property SymbolicMA.nr_states

Number of states

property SymbolicMA.nr_transitions

Number of transitions

property SymbolicMA.reachable_states

reachable states as DD

SymbolicMA.reduce_to_state_based_rewards(

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

) → None

property SymbolicMA.reward_models

Reward models

property SymbolicMA.supports_parameters

Flag whether model supports parameters