Modelator v0.2.0
Pre-release
Pre-release
- provide two top-level functions to test a system using execution traces coming from TLA+ (see #44)
run_tla_steps
will run anything that implements aStepRunner
trait: this is suitable for small specs and simple casesrun_tla_events
will run an implementation ofEventRunner
, which expects that a TLA+ state is structured, and contains besides state, also theaction
to execute, as well as theactionOutcome
to expect.
- make Apalache the default model checker
- execute model checkers in a temporary directory (see #48)