Link Search Menu Expand Document

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)

MBT Architecture