stormpy.developer.storage

Warning

The stormpy developer API is internal and can be subject to change.

Raw bindings for Storm storage, model descriptions, models and expressions.

This module is intended for developers. Use stormpy.models, stormpy.datastructures, stormpy.expressions and stormpy.io for the documented public API.

Functions

collect_model_information(model)	Collect structural model information
get_topological_sort(...)	get topological sort w.r.t.
import_umb(path, options)	Import a UMB model from the given archive path
parameters_of_model(model)	Return the value-type parameter of a sparse model or model components.
sparse_model_from_umb(umb_model, options)	Build a sparse model from the given UMB model
sparse_model_to_umb(...)	Convert a sparse model to UMB
to_archive(umb_model, path, options)	Export a UMB model to the given archive path
to_value_type	Convert a scheduler to another value type

Classes

Add	Add
AddIterator	AddIterator
Bdd	Bdd
Dd	Dd
DdManager	DD manager
DdMetaVariable	DD meta variable
DdMetaVariableType(*values)
DiceStringVisitor(self, nr_bits)	Translate expressions to dice
Halfspace	Halfspace given by normal_vector * x <= offset
ItemLabeling	Labeling
JaniInformationObject	An object holding information about a JANI model
JaniLocationExpander(self, model)	A transformer for Jani expanding variables into locations
JaniScopeChanger(self)	A transformer for Jani changing variables from local to global and vice versa
JsonExporter	Export JANI models to JSON
MemoryStructureProduct	Memory structure product
ModelBase	Base class for all models
OverlappingGuardAnalyser(self, program, ...)	An SMT driven analysis for overlapping guards
Polytope	Polytope
RewardAccumulationEliminationVisitor(self, model)	Eliminate reward accumulations from formulas and properties
SparseModelMemoryProductReverseData	Maps schedulers on a memory product back to the original model
Valuation	Base class for valuations of expression variables