Experiments on Concurrency using TLA+
To run this you need to open the folder in VSCode. Make sure you install the TLA+ Language support extension for VSCode.
At this point you can open any .tla file and run it.
The code is using PLUSCAL which is an imperative language specifying a TLA specification. You can interpret the program by right-click and saying "Source Action | Parse Module"
After this you can use TLC to check the model by right click and selecting "Check model with TLC"
QED.