SymbolicModel

class SymbolicModel[DdType, ValueType]

A probabilistic model in a symbolic representation

Template arguments:

• DdType (value)

• ValueType (type)

Available specializations:

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

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

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

Members

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

dd manager

SymbolicModel.get_parameters(

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

) → set[stormpy.numbers.Variable]

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

Get parameters

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

Flag whether model has parameters

property SymbolicModel.initial_states

initial states as DD

property SymbolicModel.is_discrete_time_model

Flag whether the model is a discrete time model

property SymbolicModel.is_exact

Flag whether model is exact

property SymbolicModel.is_nondeterministic_model

Flag whether the model contains nondeterminism

property SymbolicModel.is_partially_observable

Flag whether the model has observation labels

property SymbolicModel.is_sparse_model

Flag whether the model is stored as a sparse model

property SymbolicModel.is_symbolic_model

Flag whether the model is stored using decision diagrams

property SymbolicModel.model_type

Model type

property SymbolicModel.nr_choices

Number of choices

property SymbolicModel.nr_states

Number of states

property SymbolicModel.nr_transitions

Number of transitions

property SymbolicModel.reachable_states

reachable states as DD

SymbolicModel.reduce_to_state_based_rewards(

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

) → None

property SymbolicModel.reward_models

Reward models

property SymbolicModel.supports_parameters

Flag whether model supports parameters