# Hillel Wayne - Termination :: Learn TLA+ (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article0.00998d930354.png) ## Metadata **Cover**:: https://readwise-assets.s3.amazonaws.com/static/images/article0.00998d930354.png **Source**:: #from/readwise **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Hillel Wayne]] **Full Title**:: Termination :: Learn TLA+ **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [learntla.com](https://learntla.com/temporal-logic/termination/) **Host**:: [[learntla.com]] **Highlighted**:: [[2020-09-20]] **Created**:: [[2022-09-26]] ## Highlights - What we want is something called *fairness*: the property that if a given label is always enabled, we will eventually run it. We make this happen by specifying the process as a `fair process`. - The most common temporal logic you’ll want to check is *Termination*,