stormpy.transformations

Model transformations and their options, policies and mapping results.

Includes bisimulation minimization, submodel construction, representation changes and the addition of uncertainty.

Functions

add_uncertainty(model, additive_uncertainty, *)	Transform a model into an interval model by adding uncertainty to all transition probabilities.
build_submodel(model, states, actions, *[, ...])	Build the submodel restricted to the given states and actions.
eliminate_non_markovian_chains(model, ...)	Eliminate chains of non-Markovian states in a Markov automaton if possible.
perform_bisimulation(model, properties, *[, ...])	Minimize a model via bisimulation while preserving the given properties.
set_state_valuations(model, valuations)	Create a copy of the model with the given state valuations.
transform_to_discrete_time_model(model, ...)	Transform a continuous-time model (CTMC or MA) into a discrete-time model (DTMC or MDP).
transform_to_sparse_model(model[, properties])	Transform a model in symbolic representation into a model in sparse representation.

Classes

BisimulationOptions(self)	Options for bisimulation on sparse models
BisimulationType(*values)	Type of bisimulation
EliminationLabelBehavior(*values)	Behavior of labels while eliminating non-Markovian chains
QuotientFormat(*values)	Format of the quotient of symbolic bisimulation
StateLabelPreservation(*values)	Which state labels to preserve during bisimulation
SubsystemBuilderOptions(self)	Options for constructing a subsystem
SubsystemBuilderReturnType	Result of the construction of a subsystem