Hi Hillel, Not sure if you can help but I am interested in TLA and was following your tla intro website, particularly this part: https://learntla.com/pluscal/to

Hi Hillel, Not sure if you can help but I am interested in TLA and was following your tla intro website, particularly this part: https://learntla.com/pluscal/toolbox/ https://learntla.com/pluscal/toolbox/. I installed TLA+ Toolbox, added the example spec, translated and then tried to "run the model" however nothing happens. No output, the start and end time are still blank, no statistics etc. It is as if I never hit the run button. I don't see any errors in the console and I'm not exactly sure what I am doing so I may have missed something. FWIW the Model Overview view looks identical to the screenshot in the webpage.