# Hillel Wayne - Labels :: Learn TLA+ (Highlights)  ## Metadata **Cover**:: https://readwise-assets.s3.amazonaws.com/static/images/article3.5c705a01b476.png **Source**:: #from/readwise **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Hillel Wayne]] **Full Title**:: Labels :: Learn TLA+ **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [learntla.com](https://learntla.com/concurrency/labels/) **Host**:: [[learntla.com]] **Highlighted**:: [[2020-09-20]] **Created**:: [[2022-09-26]] ## Highlights - The first line in a process has to have a label. - A label must come before a `while` statement. - A label must come right after a `call`, `return`, or `goto`. - If you have a control statement, such as `if` or `either`, and one possible branch has a label in it, then the whole control structure must be followed with a label. - You cannot put labels in a `with` statement. - You cannot assign to any given variable more than once in a label. - switching two variables, or assigning to different records of the same structure. In these cases you can use `||` to chain assignments