Files

.devcontainer
.github
specifications
- Bakery-Boulangerie
- BlockingQueue
- CASPaxos
- CCF
- Caesar
- CarTalkPuzzle
- Chameneos
- CheckpointCoordination
- CigaretteSmokers
- CoffeeCan
- DataPort
- DieHard
- DiningPhilosophers
- Disruptor
- EinsteinRiddle
- FiniteMonotonic
- GameOfLife
- HLC
- Huang
- KeyValueStore
- KnuthYao
- L1
- LearnProofs
- LeastCircularSubstring
- LevelChecking
- LoopInvariance
- Majority
- MisraReachability
- MissionariesAndCannibals
- MultiCarElevator
- MultiPaxos-SMR
- MultiPaxos
- N-Queens
- NanoBlockchain
- ParalleRaft
- Paxos
- PaxosHowToWinATuringAward
- Prisoners
- ReadersWriters
- SDP_Verification
- SimplifiedFastPaxos
- SingleLaneBridge
- SlidingPuzzles
- SlushProtocol
- SnapshotIsolation
- SpanningTree
- SpecifyingSystems
- Stones
- SyncConsensus
- TLC
  - TLCMC.tla
  - TestGraphs.cfg
  - TestGraphs.tla
- TeachingConcurrency
- TencentPaxos
- Termination
- Tla-tortoise-hare
- TransitiveClosure
- TwoPhase
- VoldemortKV
- YoYo
- aba-asyn-byz
- acp
- allocator
- async-comm
- azure-cosmos-tla
- bcastByz
- bcastFolklore
- bosco
- braf
- byihive
- byzpaxos
- c1cs
- cbc_max
- cf1s-folklore
- chang_roberts
- detector_chan96
- dijkstra-mutex
- diskpaxos
- echo
- egalitarian-paxos
- ewd426
- ewd687a
- ewd840
- ewd998
- fastpaxos
- fpaxos
- glowingRaccoon
- lamport_mutex
- leaderless
- losa_ap
- losa_rda
- m2paxos
- mongo-repl-tla
- naiad
- nbacc_ray97
- nbacg_guer01
- nfc04
- raft
- spanning
- sums_even
- tcp
- tower_of_hanoi
- transaction_commit
- README
.ciignore
.gitattributes
.gitignore
.gitmodules
.gitpod.Dockerfile
.gitpod.yml
CITATION.cff
CNAME
CONTRIBUTING.md
DEVELOPING.md
LICENSE.md
README.md
manifest-schema.json
manifest.json

TestGraphs.cfg

Add PlusCal spec of TLC's safety checking implementation

Mar 26, 2021

911dac1 · Mar 26, 2021