Hacker News new | ask | show | jobs
by colanderman 964 days ago
I find this to be an almost everpresent problem in my own TLA+ specs, and generally resort to a similar solution. It's ugly and annoying when the counter values end up in many places in your specification -- garbage collection becomes quite complex. (Perhaps a level of indirection, along with reference counting, might help here.)

I've always felt this is a great candidate for a new built-in TLA+ "ordered opaque value" type. I know though that symmetry clauses can mess with checking temporal properties, and I haven't had time to think through whether there would be similar issues with such a built in type.
2 comments
ahelwer 964 days ago
That's an interesting idea about a built-in ordered opaque value type. You should bring it up at the next monthly TLA+ foundation community call on November 14th![0] It would be interesting to hear peoples' feedback on it.

[0] Details hidden in the google calendar link on this thread in the mailing list: https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfS...

link
colanderman 964 days ago
That's a good idea! I've been hoping to attend these but usually they conflict with Day Job meetings.
link
_flux 963 days ago
Yes, this would be very nice to have!

The workaround for a slightly different issue (similar as in using global state) I've used is to have an integer for identifier and then have a predicate that finds all the uses of those integers in the state and then picks the smallest integer not in the set of those ids. Now that I'm writing this I'm wondering how useful this was, though, even if it does avoid the GC step..

Maintaining that predicate is a bit cumbersome and error-prone in presence of multiple different kind of nodes in the system much like with GC, however, so a builtin magical id type would help a lot.

It seems that this approach of actually modifying the ids could be more effective in reducing the searh space, but will then introduce additional state transitions in the form of the GC step.

link
colanderman 963 days ago
Instead of integers you could use symmetric model values which you map to integers in a separate dedicated variable. Then it's easier to find the values in the other variables, and you don't have to mutate those other variables. (It's still hard to find them in e.g. the body of a function with infinite domain.)

(Of course with model values you must allocate them ahead of time. And with symmetry, the practical limit is 3-5 such values.)

link