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
|
Create a new environment suitable for the given model. |
|
Create a new environment which enforces exact computations. |
|
Create a new environment which enforces sound computations. |
Classes
|
Algorithm used for conditional model checking |
Environment for conditional model checking |
|
Environment for CUDD DD manager |
|
|
Reordering technique used in CUDD library |
Environment for DD libraries |
|
|
Environment configuring the algorithms of Storm |
|
Solver type for equation systems |
Environment for exploration-based model checking |
|
|
Method for min-max equation systems |
Environment for min-max solvers |
|
Environment for the model checker |
|
|
Encoding type for multi-objective model checking |
|
Multi-objective model checking method |
Environment for multi-objective model checking |
|
|
Type of precision for multi-objective model checking |
|
Method for linear equation systems with the native solver |
Environment for native solvers |
|
|
Heuristic to choose the next state during exploration |
|
Type of precomputation for exploration-based model checking |
Environment for solvers |
|
|
Algorithm for steady state distribution computation |
Environment for Sylvan DD manager |