[tlaplus] Few questions encountered when trying to implementing my spec in TLA+

External link below since it's a little bit long:

https://stackoverflow.com/questions/74912408/few-questions-encountered-when-trying-to-implementing-a-state-machine-in-tla

I hope my silly problems won't bother you .Thank you.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/614f2f23-9439-47ec-ac32-3e75dfd02d55n%40googlegroups.com.