TLA+ Wiki

Generating tests from models

You can use modelator: https://github.com/informalsystems/modelator

It can be installed through pip (python's package manager):

pip install modelator