stormpy.io

Format-specific model descriptions, parsing, exporting and their options.

Functions

export_jani_to_file(filename, model[, ...])	Write a JANI model and its properties as JSON.
export_to_drn(model, path, *[, options])	Export a sparse model in the explicit DRN format.
export_to_umb(model, path, *[, options])	Export a sparse model as UMB archive.
import_umb(path, *[, options])	Read a UMB archive into an intermediate UMB model.
instantiate_constants(model, constants[, ...])	Instantiate undefined constants in a symbolic model and the corresponding properties.
parse_jani_model(path, *[, property_filter])	Parse a Jani model and the properties contained in it from file.
parse_jani_model_from_string(json_string, *)	Parse a Jani model and the properties contained in it from a string.
parse_prism_program(path, *[, ...])	Parse a Prism program from file.
sparse_model_to_umb(model, *[, options])	Convert a sparse model to the intermediate UMB representation.
umb_to_archive(umb_model, path[, options])	Write an intermediate UMB model to an archive.

Classes

ArrayType	An array type in JANI
BasicType	A basic type in JANI
BoundedType	A bounded type in JANI
ClockType	A clock type in JANI
CompressionMode(*values)	Compression mode for UMB archives
ContinuousType	A continuous type in JANI
DirectEncodingExporterOptions(self)	Options for the DRN exporter
DirectEncodingParserOptions(self)	Options for the DRN parser
ExplicitModelParserOptions(self)	Options for the explicit model parser
JaniAssignment(self, lhs, rhs[, lvl])	Jani Assignment
JaniAutomaton(self, arg0, arg1)	A Jani Automation
JaniConstant(self, arg0, arg1)	A Constant in JANI
JaniEdge(self, source_location_index, ...)	A Jani Edge
JaniEdgeDestination	Destination in Jani
JaniLocation(self, name, assignments)	A Location in JANI
JaniModel(self, other_model)	A Jani Model
JaniModelType(*values)	Type of the Jani model
JaniOrderedAssignments(self, arg0)	Set of assignments
JaniTemplateEdge(self, arg0)	Template edge, internal data structure for edges
JaniTemplateEdgeDestination(self, ...)	Template edge destination, internal data structure for edge destinations
JaniType	A Variable Type in JANI
JaniVariable	A Variable in JANI
JaniVariableSet(self)	Jani Set of Variables
PrismAssignment(self, arg0, arg1)	An assignment in prism
PrismBooleanVariable	A program boolean variable in a Prism program
PrismCommand	A command in a Prism program
PrismConstant	A constant in a Prism program
PrismIntegerVariable	A program integer variable in a Prism program
PrismLabel	A label in prism
PrismModelType(*values)	Type of the prism model
PrismModule	A module in a Prism program
PrismProgram	A Prism Program
PrismRewardModel	Reward declaration in prism
PrismUpdate(self, arg0, arg1, arg2)	An update in a Prism command
PrismVariable	A program variable in a Prism program
SymbolicModelDescription(...)	Symbolic description of a model (Prism program or Jani model)
UmbExportOptions(self)	Options for exporting UMB models
UmbExportValueType(*values)	Value type for UMB export
UmbImportOptions(self)	Options for importing UMB models
UmbImportValueType(*values)	Value type for UMB import
UmbModel	Model in the UMB format