Temporal logic of actions
||This article includes a list of references, related reading or external links, but its sources remain unclear because it lacks inline citations. (January 2011)|
Statements in temporal logic are of the form , where A is an action and t contains a subset of the variables appearing in A. An action is an expression containing primed and non-primed variables, such as . The meaning of the non-primed variables is the variable's value in this state. The meaning of primed variables is the variable's value in the next state. The above expression means the value of x today, plus the value of x tomorrow times the value of y today, equals the value of y tomorrow.
The meaning of is that either A is valid now, or the variables appearing in t do not change. This allows for stuttering steps, in which none of the program variables change their values.
Some TLA+ editors include:
- TLA+ Toolbox (an Eclipse IDE for TLA+ tools, including PlusCal translator, TLC model checker and TLA+ Proof System)
- Eclipse TLA+ Plugin
- TLA Editor
- TLA# Plugin for Microsoft Visual Studio 2005
- Lamport, Leslie (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. ISBN 0-321-14306-X. Retrieved 2007-02-02.
- Leslie Lamport (16 December 1994), Introduction to TLA, retrieved 2010-09-17
- Lamport's page on TLA
- Official TLA+ site
- The TLA+ Proof System
- Leslie Lamport, Thinking for Programmers, a gentle intro to TLA+ at Build 2014.
|This formal methods-related article is a stub. You can help Wikipedia by expanding it.|