Examples
Examples copied to clipboard
tlaplus
A collection of TLA⁺ specifications of varying complexities
As [discussed](https://twitter.com/lemmster/status/1111683005695692800) on twitter.
## Implementation Process 0d341eea047625a85b1967fb64391f18167015d2 I implemented the EWD998 algorithm based on the TLA+ specification EWD998Chan. The implementation took two hours, during which I did not run or debug the code....
Currently we manually exclude specific modules from proof checking in the CI because they run too long. Given that proof checking time can have as high of variability as model...
Currently no specs included in the repository have an Apalache model. It would be nice to have some examples of this. The Einstein's Riddle spec would be an ideal first...
I'm adding basic TLC models to a bunch of specs for #107 and ran into trouble with this spec, could you help? Tagging authors @konnov @josef-widder @banhday I'm attempting to...
I've been defining models as part of work on #107. Currently these properties fail so these specs can only be subject to safety checking. Some fairness assumptions are required for...
As possibly encountered in #104, some bitrot could have set in for the gitpod and codespaces. This issue exists as a reminder to check that these still work.
I whipped up a quick script then downloaded & ran TLAPS 1.4.5 on macOS against all the modules containing proofs, and the following failed validation (no additional solvers installed, no...
Opening a PR, even though this is likely lacking in documentation and too technical to serve as a good example. On the other hand, the more, the merrier. :-)