Checking the model in VS Code

Before running model check disable deadlock detection and set number of workers to 8 in settings.json:

{
    "tlaplus.tlc.modelChecker.options": "-deadlock -workers 8"
}