[−][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.
The actor
and semantics
submodules will be of particular interest
to most individuals.
Modules
actor | This module provides an actor abstraction. See the |
checker | A |
explorer | A web service for interactively exploring a model. Remember to import the |
semantics | This module provides code to define and verify the correctness of an object or system based on how it responds to a collection of potentially concurrent (i.e. partially ordered) operations. |
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 |
Type Definitions
Fingerprint | A state identifier. See |