TLA+ Wiki

To learn TLA+ you need to be able to think mathematically and precisely. While a deep understanding of advanced mathematical concepts is not necessary, a solid foundation in basic mathematical concepts is important. Here's why:

TLA+ is based on mathematics: The foundation of TLA+ is set theory and first-order logic, which are fundamental to mathematics
TLA+ specifications are written in mathematical language: You'll use mathematical formulas and expressions to describe system behavior, data structures, and properties
TLA+ encourages precise thinking: TLA+ requires you to think carefully and precisely about the system you're modeling to ensure the correctness and completeness of your specifications

No, state trace for violated temporal properties is not supported.

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.

TLA+ can model real-time systems by introducing a special variable, often called now, which represents real time. Temporal properties can then be expressed with timing constraints using this now variable. For instance, you can specify that a certain event must occur within a specific time interval.

The TLA+ ecosystem provides various tools:

Vscode plugin and TLA Toolbox IDE
Syntactic analyzer (SANY): This tool checks the syntax of your TLA+ specification for errors.
TLATeX typesetter: This tool converts TLA+ specifications into beautifully formatted LaTeX documents.
TLC model checker: TLC can automatically verify TLA+ specifications for finite instances of your system. It checks for violations of invariants and temporal properties.

In TLA+, a behavior represents a possible execution of a system. It is an infinite sequence of states, where each state represents a snapshot of the system at a particular point in time. Each state is a mapping from variables to their values at that point in time. A behavior describes how the system's state evolves over time, capturing all possible transitions and actions that can occur.