stormpy.environmentsΒΆ

Environments configuring the algorithms of Storm, e.g., the solvers and their precision.

Model checking uses default() unless an environment is given explicitly. It enforces sound computations, and exact computations for exact and parametric models.

Functions

default(model)

Create a new environment suitable for the given model.

exact()

Create a new environment which enforces exact computations.

sound()

Create a new environment which enforces sound computations.

Classes

ConditionalAlgorithmSetting(*values)

Algorithm used for conditional model checking

ConditionalModelCheckerEnvironment

Environment for conditional model checking

CuddDdManagerEnvironment

Environment for CUDD DD manager

CuddReorderingTechnique(*values)

Reordering technique used in CUDD library

DdEnvironment

Environment for DD libraries

Environment(self)

Environment configuring the algorithms of Storm

EquationSolverType(*values)

Solver type for equation systems

ExplorationEnvironment

Environment for exploration-based model checking

MinMaxMethod(*values)

Method for min-max equation systems

MinMaxSolverEnvironment

Environment for min-max solvers

ModelCheckerEnvironment

Environment for the model checker

MultiObjectiveEncodingType(*values)

Encoding type for multi-objective model checking

MultiObjectiveMethod(*values)

Multi-objective model checking method

MultiObjectiveModelCheckerEnvironment

Environment for multi-objective model checking

MultiObjectivePrecisionType(*values)

Type of precision for multi-objective model checking

NativeLinearEquationSolverMethod(*values)

Method for linear equation systems with the native solver

NativeSolverEnvironment

Environment for native solvers

NextStateHeuristic(*values)

Heuristic to choose the next state during exploration

PrecomputationType(*values)

Type of precomputation for exploration-based model checking

SolverEnvironment

Environment for solvers

SteadyStateDistributionAlgorithm(*values)

Algorithm for steady state distribution computation

SylvanDdManagerEnvironment

Environment for Sylvan DD manager