[−][src]Crate stateright
A library for model checking systems, with an emphasis on distributed systems.
Please see the examples, README, and submodules for additional details.
Modules
actor | This module provides an actor abstraction. See the |
checker | A |
explorer | A web service for interactively exploring a model. |
util | Utilities such as |
Structs
Property | A named predicate, such as "an epoch sometimes has no leader" (for which the the model checker would find an example) or "an epoch always has at most one leader" (for which the model checker would find a counterexample) or "a proposal is eventually accepted" (for which the model checker would find a counterexample path leading from the initial state through to a terminal state). |
Enums
Expectation | Indicates whether a property is always, eventually, or sometimes true. |
Traits
Model | Models a possibly nondeterministic system's evolution. See |
Functions
fingerprint | Converts a state to a fingerprint. |
Type Definitions
Fingerprint | A state identifier. See |