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