[HN Gopher] Wrangling Monotonic Systems in TLA+
       ___________________________________________________________________
        
       Wrangling Monotonic Systems in TLA+
        
       Author : ahelwer
       Score  : 30 points
       Date   : 2023-11-01 19:01 UTC (3 hours ago)
        
 (HTM) web link (ahelwer.ca)
 (TXT) w3m dump (ahelwer.ca)
        
       | colanderman wrote:
       | 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.
        
       ___________________________________________________________________
       (page generated 2023-11-01 23:00 UTC)