[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)