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.
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.
[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...
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.
(Of course with model values you must allocate them ahead of time. And with symmetry, the practical limit is 3-5 such values.)
