TLA+ language support for Visual Studio Code
Run last model check again
command which allows you to quickly run TLC again without switching to the spec or model file. The Check again
button on the check visualization panel does the same.Check model
command from the Explorer context menu on .tla and .cfg files.Go to Definition
action implementation.Java Options
setting.-continue
option is used.TLC: Model Checker Options
setting now supports variables ${specName}
and ${modelName}
.TLC: Statistics Sharing
setting that allows to opt-in / opt-out sharing of TLC usage statistics (more information). Please, consider sharing.