SparseModelComponents

class SparseModelComponents[ValueType](

transition_matrix: stormpy.datastructures.SparseMatrix[ValueType] = ...,

state_labeling: stormpy.models.StateLabeling = ...,

reward_models: collections.abc.Mapping[str, stormpy.models.SparseRewardModel[ValueType]] = {},

rate_transitions: bool = False,

markovian_states: stormpy.datastructures.BitVector | None = None,

player1_matrix=None,

)

Components required for building a sparse model

Template arguments:

• ValueType (type)

Available specializations:

• SparseModelComponents[float]

• SparseModelComponents[stormpy.numbers.Rational]

• SparseModelComponents[stormpy.numbers.Interval]

• SparseModelComponents[stormpy.numbers.RationalInterval]

• SparseModelComponents[stormpy.numbers.RationalFunction]

Construction

The specialization can be inferred from the first positional constructor argument (alternatively, the transition_matrix keyword argument). If none is supplied, SparseModelComponents[float] is selected.

Members

property SparseModelComponents.choice_labeling

A list that stores a labeling for each choice

property SparseModelComponents.choice_origins

Stores for each choice from which parts of the input model description it originates

property SparseModelComponents.exit_rates

The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.

property SparseModelComponents.markovian_states

A list that stores which states are Markovian (only for Markov Automata)

property SparseModelComponents.observability_classes

The POMDP observations

property SparseModelComponents.observation_valuations

The POMDP observation valuations

property SparseModelComponents.player1_matrix

Matrix of player 1 choices (needed for stochastic two player games

property SparseModelComponents.rate_transitions

True iff the transition values (for Markovian choices) are interpreted as rates

property SparseModelComponents.reward_models

Reward models associated with the model

property SparseModelComponents.state_labeling

The state labeling

property SparseModelComponents.state_player_indications

The vector mapping states to player indices

property SparseModelComponents.state_valuations

A list that stores for each state to which variable valuation it belongs

property SparseModelComponents.transition_matrix

The transition matrix