TLA+ Specification for Ambry (https://github.com/linkedin/ambry)
- Install Visual Studio Code.
- Install the extensions "TLA+" and "TLA+ Nightly".
- Open the directory containing the tla+ and cfg files.
- Right-click, select "Check Model with TCL" and specify the below arguments
-deadlock -noTE -dump dot,actionlabels,colorize ATD -coverage 1
java -cp tla2tools.jar tlc2.TLC -deadlock -noTE -dump dot,actionlabels,colorize AR -coverage 1 <filename>