(TLA+ newbie here) I am trying to PlusCal model the double-switch lamp state machine that you can see here: https://learntla.com/topics/state-machines.html. The model works but then I knocked off one of the state transitions on purpose, to simulate a faulty model. It still passes 🙂 How can I elicit a diagnostic about that dysfunction? Thanks!