Examples
Examples copied to clipboard
tlaplus
A collection of TLA⁺ specifications of varying complexities
The steps to remove a process from the waiting queue are - get the head of the queue - remove the head by keeping the tail of the queue These...
Use "IsRead/IsWrite" instead of "read/write" as names of the predicates checking the type of processes. Using "Is*" naming pattern for predicates in other specifications seems to be the norm. It...
This change adds a Twirp Wire Protocol (v7) TLA+ spec. The protocol is defined at https://twitchtv.github.io/twirp/docs/spec_v7.html I am new to TLA+ and we use Twirp at work so I thought...
Conflict-free Replicated Data Types (CRDT) are replicated data types that encapsulate the mechanisms for resolving concurrent conflicts. we propose a reusable framework for modeling and verifying CRDT protocols.
Hi, I am new to TLA+ and am learning the PlusCal language. I found this repository very useful and wanted to contribute simple distributed algorithms to the repository that I...
* https://en.wikipedia.org/wiki/Huang's_algorithm (related https://github.com/tlaplus/CommunityModules/issues/4) * https://dl.acm.org/doi/10.5555/647172.716117
https://github.com/tlaplus/Examples/commit/4686a0be8af77260a27351cad2491873ac124d60 adds rudimentary support for Github Codespaces. TODOs: * Include the latest version of TLA+ vscode extension (https://github.com/lemmy/vscode-tlaplus/releases which comes with the debugger?) * Integrate Apalache (https://github.com/informalsystems/apalache/issues/716) ```shell ## Waiting...
Unfinished, random math exercises collected from Specifying Systems, LearnTLA, and elsewhere. ```tla ---- MODULE F ---- EXTENDS Naturals, FiniteSets, Sequences (* 1. Set of all permutations of {"T","L","A"} including repetitions....
* Modeling towers as Naturals in [Hanoi.tla](https://github.com/tlaplus/Examples/blob/master/specifications/tower_of_hanoi/Hanoi.tla) is rather low-level/close to an implementation. A high-level spec is likely simpler to grasp if it models towers as sequences... * Current Hanoi.tla...
The [current README](https://github.com/tlaplus/Examples/blob/master/README.md) does not order examples that make it easy to pick beginner-friendly examples. TLA+ concepts by which to cluster (tag?) specs: ---------------- * Constant-level expressions * Set of...