SymbolicCtmc

class SymbolicCtmc[DdType, ValueType]

CTMC in symbolic representation

Template arguments:

• DdType (value)

• ValueType (type)

Available specializations:

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

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

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

Members

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

dd manager

SymbolicCtmc.get_parameters(

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

) → set[stormpy.numbers.Variable]

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

Get parameters

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

Flag whether model has parameters

property SymbolicCtmc.initial_states

initial states as DD

property SymbolicCtmc.is_discrete_time_model

Flag whether the model is a discrete time model

property SymbolicCtmc.is_exact

Flag whether model is exact

property SymbolicCtmc.is_nondeterministic_model

Flag whether the model contains nondeterminism

property SymbolicCtmc.is_partially_observable

Flag whether the model has observation labels

property SymbolicCtmc.is_sparse_model

Flag whether the model is stored as a sparse model

property SymbolicCtmc.is_symbolic_model

Flag whether the model is stored using decision diagrams

property SymbolicCtmc.model_type

Model type

property SymbolicCtmc.nr_choices

Number of choices

property SymbolicCtmc.nr_states

Number of states

property SymbolicCtmc.nr_transitions

Number of transitions

property SymbolicCtmc.reachable_states

reachable states as DD

SymbolicCtmc.reduce_to_state_based_rewards(

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

) → None

property SymbolicCtmc.reward_models

Reward models

property SymbolicCtmc.supports_parameters

Flag whether model supports parameters