FAQ

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.