This is an old revision of the document!
FAQ
Do you need to know math to learn TLA+?
Can I use TLA+ for web development?
Do you get trace for violated temporal properties?
No, state trace for violated temporal properties is not supported.
What are the basic building blocks of TLA+ specifications?
TLA+ specifications are built using:
- Actions: These represent atomic state transitions in the system.
- State predicates: Boolean expressions that describe properties of a single state.
- Temporal operators: These connect actions and state predicates to describe how the system's behavior evolves over time.
fponzi