Embed Notice

Of course the problem with pings with nonces in TLA+ is that the set of possible nonces must be larger than the worst-case-scenario number of in-flight pings.

So if you simulate a TCP connection with 2 queues, one in each direction, up to 5 messages in each

then you need 11 different nonces (ok maybe 10 would suffice), which means you get extra 11!-ish states from all the ways your queues can be stuffed with various pings and pongs...