Crate modelator[−][src]

modelator is a framework for model-based testing.

Re-exports

pub use datachef::Recipe;

pub use event::ActionHandler;

pub use event::Event;

pub use event::EventStream;

pub use event::Runner;

pub use event::StateHandler;

artifact	List of artifacts.
datachef	Datastructure converter. Allows to define conversion rules to make (cook) concrete data-structures from the abstract ones for testing purposes.
event	A framework for event-based testing of message-passing systems with possibly partitioned system state.
module	List of modules.
runner	Test runner.
tester	Provides the way to run sets of test functions on several kinds of test inputs.

CliOptions	A struct that generates a CLI for `modelator` using `clap`.
CliOutput	Struct representing the output of `modelator` CLI. See super::CliOptions.
ModelCheckerOptions	Set of options to select the model checker to be used and configure them.
Options	Set of options to configure `modelator`.

CliStatus	Represents the exit status of any CLI command
Error	Set of possible errors that can occur when running `modelator`.
ModelChecker	Configuration option to select the model checker to be used.
ModelCheckerWorkers	Configuration option to select the number of model checker workers.
TestError	Set of possible errors that can occur when running a test using `modelator`.

run	Generate TLA+ traces using `traces` and executes them against the Rust implementation of the modeled system using a test `runner`. This `runner` implements the crate::runner::TestRunner trait.
traces	Generate TLA+ traces (encoded as JSON) given a crate::artifact::TlaFile containing TLA+ assertions and a crate::artifact::TlaConfigFile.