Crate modelator[−][src]
Expand description
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::EventRunner;pub use event::EventStream;pub use event::StateHandler;pub use step_runner::StepRunner;Modules
List of artifacts.
Datastructure converter. Allows to define conversion rules to make (cook) concrete data-structures from the abstract ones for testing purposes.
A framework for event-based testing of message-passing systems with possibly partitioned system state.
List of modules.
A runner for steps obtained from Json traces
Testing utilities
Provides the way to run sets of test functions on several kinds of test inputs.
Structs
A struct that generates a CLI for modelator using clap.
Struct representing the output of modelator CLI.
See super::CliOptions.
Set of options to select the model checker to be used and configure them.
Set of options to configure modelator.
Enums
Represents the exit status of any CLI command
Set of possible errors that can occur when running modelator.
Configuration option to select the model checker to be used.
Configuration option to select the number of model checker workers.
Set of possible errors that can occur when running a test using modelator.
Functions
Run the system under test (SUT) using the abstract events obtained
from TLA+ traces. Traces are generated using traces,
To interpret abstract events an EventRunner needs to be created,
as well as StateHandler and ActionHandler to be implemented
for abstract states and actions you want to handle.
This is the most simple interface to run your system under test (SUT)
against traces obtained from TLA+ tests.
The function generates TLA+ traces using crate::traces and execute them against
the SUT that implements StepRunner.
Given a crate::artifact::TlaFile with TLA+ test assertions, as well as a crate::artifact::TlaConfigFile with TLA+ configuration, generate all traces resulting from the test assertions.