It's absolutely bonkers that TLA+ struggles with this, given that a system is eventually consistent IFF it is logically monotonic (CALM) [1].
This also doesn't make intuitive sense to me. Model checking should be easier for monotonic models, because because the total model check can be viewed as a consistent sum of all partial checks. I've collaborated on a monotonic parser once, which was essentially a monotonic logic programming language. One of the key insights was that you can replace backtracking search of the state space with solving a set covering problem where you attempt to find the union of all sub-parses that cover the sentence fully. So for monotonic systems you should be able to dynamically program / divide and conquer the heck out of it.
It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting.
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.
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.
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.
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.)
This also doesn't make intuitive sense to me. Model checking should be easier for monotonic models, because because the total model check can be viewed as a consistent sum of all partial checks. I've collaborated on a monotonic parser once, which was essentially a monotonic logic programming language. One of the key insights was that you can replace backtracking search of the state space with solving a set covering problem where you attempt to find the union of all sub-parses that cover the sentence fully. So for monotonic systems you should be able to dynamically program / divide and conquer the heck out of it.
1. https://arxiv.org/abs/1901.01930