# Hillel Wayne - Processes :: Learn TLA+ (Highlights)  ## Metadata **Cover**:: https://readwise-assets.s3.amazonaws.com/static/images/article2.74d541386bbf.png **Source**:: #from/readwise **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Hillel Wayne]] **Full Title**:: Processes :: Learn TLA+ **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [learntla.com](https://learntla.com/concurrency/processes/) **Host**:: [[learntla.com]] **Highlighted**:: [[2020-09-20]] **Created**:: [[2022-09-26]] ## Highlights - ---- MODULE module\_name ---- \* TLA+ code (* --algorithm algorithm\_name variables global\_variables process p\_name = foo variables local\_variables begin \* pluscal code end process process p\_group \in bar \* set variables local\_variables begin \* pluscal code end process end algorithm; *) ==== - so all processes in a behavior *must* be comparable and *should* be unique. - You can get a process’s value with `self` - Variables declared in a process scope are local to *that process*. - If you use `\in` for the variables, TLC will create one state for each combination of initial states in each process. - Is there a way to prevent a step from running? We can do this with `await`: