|
|
|
|
|
|
by nano_o
1155 days ago
|
|
|
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:/... |
|
|