Modelator is a tool that facilitates generation and execution of tests. Besides other features, it provides:

• easy selection of a model checker to execute (Apalache or TLC)
• automatic enumeration of tests in TLA+ files
• generation of multiple test executions from the same test assertion
• interfaces for execution of generated tests in target languages (currently Rust and Go)