[−][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 `system` submodule for model checking. See the `spawn` submodule for a runtime that can run your actor over a real network. See the `register` submodule for an example wrapper.
checker	A `Model` checker.
explorer	A web service for interactively exploring a model.

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 Checker.

Functions

fingerprint

Converts a state to a fingerprint.

Type Definitions

Fingerprint