[HN Gopher] Breaking the limits of TLA+ model checking
       ___________________________________________________________________
        
       Breaking the limits of TLA+ model checking
        
       Author : todsacerdoti
       Score  : 93 points
       Date   : 2023-04-17 15:11 UTC (7 hours ago)
        
 (HTM) web link (www.hillelwayne.com)
 (TXT) w3m dump (www.hillelwayne.com)
        
       | dwohnitmok wrote:
       | RE the OP's work to add probability-weighted state transitions,
       | more generally TLA+ doesn't have the ability to talk about state
       | transitions (i.e. actions in TLA+) themselves in a first class
       | way, which makes certain invariants very annoying or impossible
       | to state (e.g. we will converge after no more than 5 steps). I
       | wonder if there's a clean way to extend TLA+ to cover these
       | cases. Admittedly they don't come up that frequently.
        
         | nano_o wrote:
         | In your example, you can just add a variable that is
         | incremented at every step and then use it to state your
         | invariant that convergence must happen within 5 steps.
         | 
         | Sometimes you can encode properties that might initially seem
         | hard to state in TLA+ in a similar way. Lamport has a recent
         | paper explaining how to do that for hyperproperties such as
         | information-flow security:
         | http://lamport.azurewebsites.net/pubs/pubs.html?from=https:/...
        
       | Nezteb wrote:
       | The repo: https://github.com/hwayne/tla-graphing-demo
        
       ___________________________________________________________________
       (page generated 2023-04-17 23:00 UTC)