I just gotta say, it's _incredibly_ surreal seeing one of the people who inspired me to start studying formal methods link an article I wrote on formal methods.
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/. 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.
Would you mind emailing me the screenshots at h@learntla? My immediate guess would be that "temporal properties" is unchecked, but I'd have to take a look.
