Wolf480pl on Nostr: So yesterday TLA+ made me realize that the property of my protocol that I'm trying to ...

So yesterday TLA+ made me realize that the property of my protocol that I'm trying to verify makes no sense (the incorrect behaviour is indistinguishable from a client's PoV from a correct behaviour).

So I was thinking how I could make it distinguishable in a way that will work not only in TLA+ but also in real life, and it turns out I could really use pings in the protocol.

Then I looked into my WIP testsuite for this protocol from 2 years ago, and guess what I found?