Описание тега tla+

Описание тега Вопросы с тегом

TLA+ is a language and toolchain for specifications based on TLA, the Temporal Logic of Actions. The TLA Toolbox includes a translator from PlusCal to TLA+, the TLC model checker, and an IDE.

TLA+ is a language and toolchain for specifications based on TLA (Temporal Logic of Actions). The TLA toolbox include

SANY, a parser and pretty-printer for TLA+
TLC, a model checker and simulator for a subclass of TLA+ specifications
TLAPS, a checker for TLA+ proofs
a translator from the PlusCal algorithm language
an IDE (integrated development environment)

TLA is a temporal logic models systems with mutable state by distinguishing x (the value of x in the current state) from x' (the value of x in the next state). It is usually used to model concurrent and reactive systems. For questions about the logic itself, try our sister site Computer Science.