stormpy

Python bindings for the probabilistic model checker Storm.

This module provides convenience entry points for the core functionality of Storm: parsing symbolic models and properties, building models and model checking.

Functions

build_model	Build a model from a symbolic model description.
build_model_from_drn	Build a model in sparse representation from a file in the explicit DRN format.
build_model_from_explicit(transitions, ...)	Build a model in sparse representation from files in the explicit format (.tra, .lab, ...).
build_model_from_umb(path, *[, options])	Build a model in sparse representation from a UMB archive.
build_symbolic_model	Build a model in symbolic representation (using decision diagrams) from a symbolic model.
create_filter(model, expression)	Create a filter selecting the states of a symbolic model satisfying the given expression.
create_filter_initial_states(model)	Create a filter selecting the initial states of the model.
filter_initial_states(result, model)	Restrict the model checking result to the initial states of the model.
instantiate_constants(model, constants[, ...])	Instantiate undefined constants in a symbolic model and the corresponding properties.
model_checking(model, property, *[, ...])	Model check a property on a model.
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.
parse_properties(properties[, context, ...])	Parse properties given in the Prism property format.
parse_property(property[, context])	Parse a single property given in the Prism property format.

Classes

BuilderOptions(BuilderOptions)	Options for building a model from a symbolic description.
CheckResult	Base class for all model checking results
Engine(*values)	Engine used for building models and model checking.
Environment(self)	Environment configuring the algorithms of Storm
ExplicitModelCheckerHint	Information that may accelerate an explicit state model checker
Interval(Interval Interval)
ModelCheckerHint	Information that may accelerate the model checking process
Polynomial
Rational(...)	Class wrapping gmp-rational numbers
RationalFunction
RationalFunctionCoefficient
RationalInterval
RawPolynomial
UncertaintyResolutionMode(*values)	How uncertainty in interval models is resolved