Untitled attachment

Notices where this attachment appears

1. Embed this notice
   Wolf480pl (wolf480pl@mstdn.io)'s status on Sunday, 22-Dec-2024 06:37:33 JST Wolf480pl

   in reply to

   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...