Wrangling Monotonic Systems in TLA+

It&#x27;s absolutely bonkers that TLA+ struggles with this, given that a system is eventually consistent IFF it is logically monotonic (CALM) [1].<p>This also doesn&#x27;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&#x27;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 &#x2F; divide and conquer the heck out of it.<p>1. <a href="https:&#x2F;&#x2F;arxiv.org&#x2F;abs&#x2F;1901.01930" rel="nofollow noreferrer">https:&#x2F;&#x2F;arxiv.org&#x2F;abs&#x2F;1901.01930</a>

I find this to be an almost everpresent problem in my own TLA+ specs, and generally resort to a similar solution. It&#x27;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.)<p>I&#x27;ve always felt this is a great candidate for a new built-in TLA+ &quot;ordered opaque value&quot; type. I know though that symmetry clauses can mess with checking temporal properties, and I haven&#x27;t had time to think through whether there would be similar issues with such a built in type.