stormpy.models

Probabilistic models, their states, actions, rewards, labels and schedulers.

Sparse model states and actions are views obtained through model.states and state.actions. They expose identifiers, labels and outgoing transitions.

Classes

ChoiceLabeling(self, choice_count)	Labeling for choices
ChoiceOrigins	This class represents the origin of choices of a model in terms of the input model spec.
DdType(*values)
JaniChoiceOrigins(self, jani_model, ...)	This class represents for each choice the origin in the jani spec.
MemoryStructure	Finite memory states, labels and transitions used by a scheduler
MemoryStructureBuilder	Memory structure builder
ModelType(*values)	Type of the model
PrismChoiceOrigins(self, prism_program, ...)	This class represents for each choice the set of prism commands that induced the choice.
Scheduler	A Finite Memory Scheduler
SchedulerChoice	A choice of a finite memory scheduler
SimpleValuation	Values of the variables in a symbolic program state
SparseCtmc	CTMC in sparse representation
SparseDtmc	DTMC in sparse representation
SparseMA	MA in sparse representation
SparseMdp	MDP in sparse representation
SparseModel	A probabilistic model in a sparse matrix representation
SparseModelAction	Action for state in sparse model
SparseModelActions	Actions for state in sparse model
SparseModelComponents	Components required for building a sparse model
SparseModelState	State in sparse model
SparseModelStates	States in sparse model
SparsePomdp	POMDP in sparse representation
SparseRewardModel	Reward structure for sparse models
SparseSmg	SMG in sparse representation
StateLabeling(self, state_count)	Labeling for states
SymbolicCtmc	CTMC in symbolic representation
SymbolicDtmc	DTMC in symbolic representation
SymbolicMA	MA in symbolic representation
SymbolicMdp	MDP in symbolic representation
SymbolicModel	A probabilistic model in a symbolic representation
SymbolicRewardModel	Reward structure for symbolic models
ValuationClassDescription	Schema describing the variables of a valuation class
ValuationDescriptionBuilder(self, manager)	Incrementally builds a ValuationClassDescription
Valuations(self, class_description[, ...])	Valuations for explicit entities (states/observations)
ValuationTransformer(self, old_valuations)	Transforms the given valuations to a new valuations over a new variable set.