Ignas Kiela on Nostr: nprofile1q…utslx right, but what I'm saying is that noonce isn't really something ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq0cq07ulfyc7y2l8rczk9s36g8j65tq3m6xk9us8hr3ua4ktfmaqqeutslx (nprofile…tslx) right, but what I'm saying is that noonce isn't really something that you even need at all in TLA+, the model would be equisatisfiable if you just sent pings without a noonce and sent pongs to a specific ping message (by say, numbering messages in general). It's state that you don't generally need.

I've been doing a bunch of stuff with SAT and SMT solvers on the side and eliminating unnecessary state has provided me with way faster solutions most of the time (there's a balance to be had between size of state and complexity of the problem, but most problems aren't that hard).