# Hillel Wayne - A Simple Spec :: Learn TLA+ (Highlights)  ## Metadata **Cover**:: https://readwise-assets.s3.amazonaws.com/static/images/article1.be68295a7e40.png **Source**:: #from/readwise **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Hillel Wayne]] **Full Title**:: A Simple Spec :: Learn TLA+ **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [learntla.com](https://learntla.com/pluscal/a-simple-spec/) **Host**:: [[learntla.com]] **Highlighted**:: [[2020-09-20]] **Created**:: [[2022-09-26]] ## Highlights - ---- MODULE module\_name ---- \* TLA+ code (* --algorithm algorithm\_name begin \* PlusCal code end algorithm; *) ==== - You can only have one PlusCal algorithm per file. - In the `variables` block, `=` is assignment. Everywhere else, `=` is the equality check and `:=` is assignment. - `TLC` is a module that adds `print` and `assert`. - `A:`. That is called a *label*. TLC treats labels as the “steps” in a specification - It’s only between labels that the model can check invariants and switch processes. - you can’t assign to the same variable twice in the same label. - While - This is the only form of looping. - You might have noticed the `y \in {3, 4}`. - TLC will make sure it works for **all** possible values of y. Create multiple behaviors