From Wikipedia, the free encyclopedia
Logic used to describe behaviours of concurrent systems.
Temporal logic of actions (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions. It is used to describe behaviours of concurrent and distributed systems. It is the logic underlying the specification language TLA+.
Statements in the temporal logic of actions are of the form [ A ] t {\displaystyle [A]_{t}} , 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 x + x ′ ∗ y = y ′ {\displaystyle x+x'*y=y'} . 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 [ A ] t {\displaystyle [A]_{t}} 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.
Specification languages[edit]There are multiple specification languages that implement Temporal Logic of Actions. Each language has unique features and use cases:
TLA+ is the default and most widely used specification language for TLA. It is a mathematical language designed to describe the behavior of concurrent and distributed systems. The specification is written in functional style.
----------------------------- MODULE HourClock ----------------------------- EXTENDS Naturals VARIABLES hour Init == hour = 1 Next == hour' = IF hour = 12 THEN 1 ELSE hour + 1 Spec == Init /\ [][Next]_hour =============================================================================
PlusCal is a high-level algorithm language that translates to TLA+. It allows users to write algorithms in a familiar pseudocode-like syntax, which are then automatically converted into TLA+ specifications. This makes PlusCal ideal for those who prefer to think in terms of algorithms rather than state machines.
----------------------------- MODULE HourClock ----------------------
EXTENDS Naturals
(*--algorithm HourClock {
variable hour = 1;
{
while (TRUE) {
hour := (hour % 12) + 1;
}
}
} --*)
Quint is another specification language that translates to TLA+. Quint combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art type checking and development tooling. Unlike PlusCal, the Quint operators and keywords have one-to-one translation to TLA+. Quint provides a REPL, random simulator and integration with the TLA+ model checkers.
module hour_clock {
var hour: int
action init = hour' = 1
action step = hour' = if (hour == 12) 1 else hour + 1
}
FizzBee[1] is an alternative to TLA+ with higher level specification language using a Python-like syntax designed to bring formal methods for mainstream software engineers working on distributed systems. While based on Temporal Logic of Actions, it does not translate to or use TLA+ under the hood unlike PlusCal or Quint.
action Init: hour = 1 atomic action Tick: # The body of the actions is Starlark (a Python dialect) hour = (hour % 12) + 1
A gentle intro to TLA+ at Build
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4