SymbolicMdp

class SymbolicMdp[DdType, ValueType]

MDP in symbolic representation

Template arguments:

• DdType (value)

• ValueType (type)

Available specializations:

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

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

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

Members

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

dd manager

SymbolicMdp.get_parameters(

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

) → set[stormpy.numbers.Variable]

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

Get parameters

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

Flag whether model has parameters

property SymbolicMdp.initial_states

initial states as DD

property SymbolicMdp.is_discrete_time_model

Flag whether the model is a discrete time model

property SymbolicMdp.is_exact

Flag whether model is exact

property SymbolicMdp.is_nondeterministic_model

Flag whether the model contains nondeterminism

property SymbolicMdp.is_partially_observable

Flag whether the model has observation labels

property SymbolicMdp.is_sparse_model

Flag whether the model is stored as a sparse model

property SymbolicMdp.is_symbolic_model

Flag whether the model is stored using decision diagrams

property SymbolicMdp.model_type

Model type

property SymbolicMdp.nr_choices

Number of choices

property SymbolicMdp.nr_states

Number of states

property SymbolicMdp.nr_transitions

Number of transitions

property SymbolicMdp.reachable_states

reachable states as DD

SymbolicMdp.reduce_to_state_based_rewards(

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

) → None

property SymbolicMdp.reward_models

Reward models

property SymbolicMdp.supports_parameters

Flag whether model supports parameters