TLA+ Learning

Some examples and notes while learning TLA+ modeling language.

Notes

TLA+
- Temporal Logic of Actions
- A logical formism based on simple math to describe systems
The mathematical model
- A behavior is a sequence of states
- A state is an assignment of values to variables
- The system is described by a formula about behaviors
  - That's true on behaviors that represent possible system execution
  - Usually obtained combining two formulas:
    - Init to describe initial states
    - Next to describe state transitions

Notes from Leslie Lamport Course

Lesson 1

TLA+ is a language for high-level modeling of digital systems
TLAPS, is the TLA+ proof system
Use TLA+ to model criticla parts of digital systems
Abstract away
- less critical parts
- lower-level implementation details
TLA+ was designed for modeling concurrent and distributed systems
Can help find and correct design errors
- errors hard to find by testing
- before writing any code
Simplifying by removing details is called abstraction
Only through abstraction can we understand complex systems
We can't get systems right if we don't understand them
Precise high-level models are called specifications
TLA+ can specify algorithms and high-level designs
You don't get a 10x reduction in code size by better coding, you get it by coming to a cleaner architecture
An architecture is a higher-level specification - higher than the code level.
We use TLA+ to ensure the systems we build work right
Working right means satisfying certain properties
The properties TLA+ can check are conditions on individual executions.
An execution of a system is represented as a sequence of discrete steps.
Digital system:
- We can abstract its continious evolution as a sequence of discrete events.
We can simulate a concurrent system with a sequential program.
TLA+ describes a step as a step change.
An execution is represented as a sequence of states.
A step is the change from one state to the next.
TLA+ describes a state as an assignment of values to variables.
A behavior is an infinite sequence of states
An execution is represented as a behavior
We want to specify all possible behaviors of a system
A state machine is described by:
1. All possible initial states.
2. What next states can follow any given state.
A state machine halts if there is no possible next state.
In TLA+ a state machine is described by: 0. What the variables are.
1. Possible initial values of variables.
2. A relation between their values in the current state and their possible values in the next state.

Lesson 2

We need precise language to describe state machines
TLA+ uses ordinary, simple math
Must replace AND (&&) by a mathimatical operator ∧ (logical AND)
Must replace OR (||) by a mathimatical operator ∨ (logical OR)
"i in {0,1,...,1000} is written as i ∈ 0..1000 in math
In TLA+ we don't write instructions for computing something, we're writing a formula relating the values.
The TLA+ source is in ASCII
In ASCII, ∧ is typed as /\, ∨ is typed as \/ and ∈ is typed as \in
The = sign in TLA+ means math equality, as in 2 + 2 = 4 unlike in most programming languages where it means assignment
Math is much more expressive than standard programming language
∧ and ∨ are commutative, so interchaning groups in sub-formulas yields an equivalent formula.
The math symbol ≜ means equal by definition. In TLA+ it is written as ==

Lesson 3

Deadlock - Execution stopped when it wasn't supposed to.
Termination - Execution stopped when it was suppose to. Most systems should not stop. The default is for TLC to regard stoppint as deadlock.

Lesson 4

The best way to get started on a spec is to write a single correct behavior.
TLA+ has no type declarations.
Type correctness means all the variables have sensible values.
We can define a formula that asserts type correctness. This helps readers understand the formula.
TLC can check that type correctness is valid by checking the formula is always true.
Names must be defined before they are used.
A formula that is true in every reachable state is called an invariant
The not equal operator is ≠ and is written in ASCII as /= or #
≤ is =< in TLA+ ASCII
To keep things simple, use a primed variable v' only in one of these two kinds of formulas:
- v' = ... and v' ∈ ... where ... contains no primed variables
comment out blocks with (* and *)
∃ means There is exists and is writen as \E in ASCII.

Lesson 5

Use CONSTANT to declare a value that is the same throughout every behavior.
In TLA+, every value is a set.
Negation operator in C ! is ¬ in TLA+ and is written as ~ in ASCII

TLA+ has two kinds of comments

* an end of line comment"

(******************)
(* boxed comments *)
(* like this      *)
(******************)

We can add pretty printed seperator lines with ---- in between statements

Lesson 6

Records
- the definition
  - r ≜ [prof |-> "Fred", num |-> 42]
    - defines r to be a record with two fields prof and num.
    - The values of it's two fields are
      - r.prof = "Fred" and r.num = 42
  - Chaning the order of the fields makes no difference
- TLA+ format is
  - [prof : {"Fred", "Ted", "Ned"}, num : 0..99]
    - is the set of all records
      - [prof |-> ..., num |-> ...]
    - with prof field in set {"Fred", "Ted", "Ned"} and
      - num field in set 0..99
  - So [prof |-> "Ned", num |-> 24] is in this set.
- This record is a function
  - [prof |-> "Fred", num |-> 42]
    - is a function f with domain {"prof", "num"}
    - such that f["prof"] = "Fred" and f["num"] = 42
- f.prof is an abbreviation for f["prof"]
- This except expression equals the record that is the same as f except it's prof field is the string red
  - [f EXCEPT !["prof"] = "Red"]
    - this can be abbreviated as
      - [f EXCEPT !.prof = "Red"]
Subset ⊆ is written as \subseteq in ASCII and read is a subset of
Union set operator ∪ is written as \union in ASCII S ∪ T is the set of all elements S or T or both

UNCHANGED <<value1, value2, value3>> is equivalent to

  ^ value1' = value1
  ^ value2' = value2
  ^ value3' = value3

Angle brackets ⟨ ⟩ is written as << >> in ASCII.
The expression << >> is for ordered tuples.
Enabling conditions should go before any prime action formulas.

Lesson 7

CHOOSE v \in S : P equals
- if there is a v in S for which P is true
  - then some such v
  - else a completely unspecified value
In math, any expression equals itself
- (CHOOSE i \in 1..99 : TRUE) = (CHOOSE i \in 1..9: TRUE)
There is no nondetermism in a mathematical expression.
x' \in 1..99
- Allows the value of x in the next state to be any number in 1..99
x' = CHOOSE i \in 99 : TRUE
- Allows the value of x in the next state to be on particular number
M \ {x}
- S \ T is the set of elements in S not in T
  - e.g. (10..20) \ (1..14) = 15..20
Two Set constructors
- { v \in S : P}
  - the subset of S consisting of all v satisfying P
    - e.g. { n \in Nat : n > 17} = {18,19,20,...}
      - The set of all natural numbers greater than 17
- { e : v \in S }
  - The set of all e for v in S
    - e.g. { n^2 : n \in Nat} = {0, 1, 4, 9, ...}
      - The set of all squares of natural numbers
The LET clause makes the definitions local to the LET expressions.
- The defined identifiers can only be used in the LET expressions.
Elements of a symmetry set, or a constant assigned elements of a symmetry set, may not appear in a CHOOSE expression.

Lesson 8

P => Q
- if P is true, then Q is true
- the symbol ⇒ written => and is read implies
P => Q equals ~Q => ~P
In speech, implication asserts causality.
In math, implication asserts only correlation.
A module-closed expression is a TLA+ expression that contains only:
- identifiers declared locally within it
A module-closed formula is a boolean-valued module-closed expression.
A constant expression is a (module-complete) expression that (after expanding all definitions):
- has no declared variables
- has no non-constant operators. e.g. some non-constant operators are ' (prime) and UNCHANGED
The value of a constant expression depends only on the values of the declared constants it contains.
An assumptionat (ASSUME) must be a constant formula.
A state expression can contain anything a constant expression can as well as declared variables.
The value of a state expression depends on:
- The value of declared constants
- The value of declared variables
A state expression has a value on a state. A state assigns values to variables.
A constant expression is a state expression that has the same value on all states.
An action expression can contain anything a state expression can as well as ' (prime) and UNCHANGED.
A state expression has a value on a step (a step is a pair of states).
A state expression is an action expression whose value on the step s -> t depends only on state s.
An action formula is simply called an action.
A temporal formula has a boolean value on a sequence of states (behavior)
TLA+ has only boolean-valued temporal expressions.
Example spec:
- Initial formula
  - TPInit
- Next-state formula
  - TPNext
- TPSpec should be true on s1 -> s2 -> s3 -> ... iff
- TPInit is true on s1
- TPNext is true on s_i -> s_i+1 for all i
- TPInit is considered to be an action.
⎕ typed [] in ASCII, is read as always. The always operator.
⎕TPNext - "Always TPNext"
TPSpec ≜ TPInit /\ [⎕TPNext]<<v1,v2,v3>>
- The specification with
  - Initial formula Init
  - Next-state formula Next
  - Declared variables v1,...vn
- Is expressed by the temporal formula
  - Init /\ ⎕[Next]<<v1...,vn>>
For a temporal formula TF;
- THEOREM TF
  - asserts that TF is true on every possible behavior.
THEOREM TPSpec => []TPTypeOK
- Asserts that for every behavior:
  - if TPSpec is true on the bheavior
  - then []TPTypeOK is true on the behavior (means TPTypeOK is true on every state of the behavior).
- Asserts that TPTypeOK is an invariant of TPSpec.
INSTANCE TCCommit
- THEOREM TPSpec => TCSpec
  - Asserts that for every behavior:
    - if it satisfies TPSpec
    - then it satisfies TCSpec
Dpecifications are not programs; they're mathematical formulas.
A specification does not describe the correct behavior of a system, rather it describes a universe in which the system and its environment are behaving correctly.
The spec says nothing about irrelevant parts of the universe.
THEOREM TPSpec => TCSpec
- This theorem makes sense because both formuals are assertions about the same kinds of behavior.
- It asserts that every behavior satisfying TPSpec satisfies TCSpec.
Steps that leave all the spec's variables unchanged are called stuttering steps
Every TLA+ spec allows stuttering steps
We represent a terminating execution by a behavior ending in an infinite sequence of stuttering steps.
- The universe keeps going even if the system terminates.
- All behaviors are infinite sequences of states.
Specs specify what the system may do.
- They don't specify what it must do.
- These are different kinds of requirments and should be specified seperately.

Lesson 9

List are finite sequences.
Tuples are simply finite sequences.
<< -3, "xyz", {0,2} >> is a sequence of length 3
A sequence of length N is a function with domain 1..N
- << -3, "xyz", {0,2} >>[1] = -3
- << -3, "xyz", {0,2} >>[2] = "xyz"
- << -3, "xyz", {0,2} >>[3] = {0,2}
The sequence <<1,4,9,...,N^2>> is the function such that
- <<1,4,9,...,N^2>>[i] = i^2
- for all i in 1..N
  - This is writen as: [i \In 1..N |-> i^2]
Tail(<<s1,..,sn>>) equals <<s2,...,sn>>
Head(seq) == seq[1]
◦ (concatenation) written as \o concaneates two sequences
- <<3,2,1>> ◦ <<"a","b">> = <<3,2,1,"a","b">>
Any non-empty sequence is the concaneation of it's head with it's tail
- IF seq # <<>> THEN seq = <<Head(seq)>> \o Tail(seq)
The Append operator appends an element to the end of the sequence
- Append(seq, e) == seq \o <>
The operator Len applied to a sequence equals the sequences' length
- Len(seq)
The domain of a sequence seq is 1..Len(seq)
- 1..0 = {}, which is the domain of <<>>
Seq(S) is the set of all sequences with elements in S.
- Seq({3}) = {<<>>, <<3>>, <<3,3>>, <<3,3,3>>, ...} (infinite sequences)
Remove(i, seq) == [j \in 1..(Len(seq) - 1) |-> IF j < i THEN seq[j] ELSE seq[j + 1]]
Len(Remove(i, seq)) = Len(seq) -1
The Cartesian Product
- For any sets S and T
  - S × T equals the set of all <<a, b>> with a ∈ S and b ∈ T
  - S × T = {<<a, b>>: a \in S, b \in T}
- The × (times) operator is written as \X in ASCII.
A Safety Formula is a temporal formula that asserts only what may happen.
- It's a temporal formula that if a behavior violates it, then that violation occurs at some particular point in that behavior.
  - Nothing past that point can prevent the violation.
    - For example:
      - Init /\ [][Next]vars can be violated either:
        
        Initial state not satisfying Init
        
        Step not satisfying [Next]vars
        
        Step neither satisfies Next nor leaves vars unchanged.
      - Nothing past that point of violation can cause the formula to be true.
A Liveness Formula is a temporal formula that asserts only what must happen.
- A temporal formula that a behavior can not violate it at any point.
- Example: x = 5 on some state of the behavior.
  - asserted by (x = 5)
  - ◊ is typed as <> is ASCII and is pronounced eventually
The only liveness property sequential programs must satisfy is termination.
- Expressed by formual ◊Terminated
is ~> is ASCII and means leads to.
◊P is equivalent to ¬⎕¬P
- Eventually P is equal to not always not P.
An action A is enabled in a state s if-and-only-if there is a state t such that s → t is an A step.
An action is enabled if the system is not in a deadlocked/terminated state. The safety part of the spec implies that such a state cannot be reached.
A conjunct with no primes is an assertion.
A weak fairness of action A asserts of a behavior:
- If A ever remains continiously enabled, then an A step must eventually occur.
- Or equivalenty:
  - A cannot remain enabled forever without another A step occuring.
Weak fairness of A is written as the temporal formula WF_vars(A), where vars is the tuple of all the spec's variables.
- It's a liveness property because it can always be made true by an A step or a state in which A is not enabled.
A spec with liveness is written
- _Init /\ [][Next]vars /\ Fairness
  - Fairness ia conjunction of one or more WF_vars(A) and SF_vars(A) formulas, where each A is a subaction of Next.
- A subaction of Next is when every possible A step is a Next step.
WF_vars(A) asserts of a behavior:
- If A /\ (vars' # vars) ever remains continiously enabled:
  - then an A /\ (vars' # vars) step must eventually occur.
- An A /\ (vars' # vars) step is a non-stuterring A step
ABS == INSTANCE ABSpec
- Imports all definitions of Spec,... from ABSpec, renamed as ABS!Spec,...
THEOREM Spec => ABS!Spec
- This theorem states that the safety specification Spec implements it's high level safety specification ABS!Spec
Weak fairness of A asserts of a behavior:
- If A ever remains continiously enabled, then an A step must eventually occur.
Strong fairness of action A asserts of a behavior:
- If A is repeatedly enabled, then an A step must eventually occur.
- Or equivalently:
  - A cannot be repeatedly enabled forever, without another A step occuring.
For systems without hard real-time response requirements, liveness checking is a useful way to find errors that prevent things from happening.
Many systems use timeouts only to ensure that something must happen.
- Correctness of such a system does not depend on how long it takes the timeouts to occur.
- Specifications of these systems can describe timeouts as actions with not time constraints, only weak fairness conditions.
- This is true for most systems with no bounds on how long it can take an enabled operation to occur.
A reason to add liveness is to catch errors in the safetey formula Spec.

Ron Pressler course notes

Part 1

TLA+ is like a blueprint when designing a house
In TLA+ the abstraction/implementation relation is expressed by logical implication: X ⇒ Y is the proposition that X implements Y, or conversely that Y abstracts X.
Specifying in TLA+ is ultimately specifying with mathematics. But math doesn't save you from thinking; it just helps you organize your thoughts.
A signature, which is a set of symbols with a specifiy arity - how many arguments the symbol takes.
- e.g. 5 (0-ary), = (2-ary), < (2-ary), * (2-ary)
Expressions can have quantifier, like \A ("for all") and "existential quantifier" \E ("there exists")
\A x ... means "for all objects s such that ..."
\E x ... means "there exists an object x such that ..."
A well-formed expression is called a term (of the language), so the syntax is thought of as the set of all the terms.
A formula is a boolean-valued expression, either true or false.
Variables that appear in a formula unbound are called free variables_
A formula that has no free variables is called a sentence or closed formula
A model is the relationship between the syntax and semantics: a model of a formula is a structure that satisfies it.
It satisfies it by assigment of values to the variables taht make the formula true (truth is a semantic property).
⊨ or |= in ASCII, is the symbol for satisfies, on the left is a structure that make the formula on the right true
The collection of all models of a formula A forms its formal semantics is written as [[A]]
Examples
- [[A∧B]]=[[A]]∩[[B]] - the model for A /\ B is the intersection of model A with model B.
- [A∨B]]=[[A]]∪[[B]] - the model for A / B is the union of model A with model B.
- [[¬A]]=[[A]]c - the model ~A is the complement of the model A
Ehen working with logic, we work within a specific logical theory, which is a set of formulas called axioms, taken to be equivalent to TRUE.
A model of a theory is a structure that satisfies all axioms of the theory; the theory specifies a model.
Peano axioms - logical theory that characterizes the natural numbers and familiar arithmetic operations
A logic also hash a calculus a syntactic system for deriving expressions from other expressions, like natural deduction.
- If formula C can be derived by a finite number of application of inference rules from formulas A and B, we write A,B ⊢ C, and say that A and B prove C or entail C, where A and B are the assumptions.
- If formula A is entaile dby theory's axioms alone without any other assumptions, we write ⊢A and say A is a tautology
- If ⊢A and A is not an axiom, we say that A is a theorem. If we want to prove the theorem A, but we havne't yet done so, we call A a proposition

Glossary

TLC - TLA+ model checker
TLA+ Toolbox - create specs and run tools on them
TLAPS - the TLA+ proof system
Deadlock - Execution stopped when it wasn't supposed to.
Termination - Execution stopped when it was suppose to.
The TLA+ syntax for an array valued expression: [ variable ∈ set ↦ expression ]
- Example: sqr ≜ [i ∈ 1..42 ↦ i^2]
  - defines sqr to be an array with index set 1..42
  - such that sqr[i] = i^2 for all i in 1..42
↦ is typed as |-> in ASCII
In Math, we use parentheses for function application instead of brackets.
in TLA+ we write formulas not programs so we use math terminology,
- function instead of array, domain instead of index set,
- however TLA+ uses square brackets for function application to avoid confusing with
- another way mathemiatics uses paranethesis
Math and TLA+ allow a function to have any set as its domain, for example, the set of all integers.
The for all symbol ∀ is typed as \A in ASCII
the exponentiation operator is represented by the carat chractor e.g. (i^2)
≡ or ⇔ or <=> is "if-and-only-if" equivalence

Syntax

EXTENDS Integers - imports arithmetic operators like + and ..
VARIABLES i, pc - Declares identifiers
Init and Next are convention names used
<>[]P - a termporal operator that every behaviour must conform to where eventually P becomes true and then always stays true. P may switch between true or false but must be true when program terminates.

Operators

/\ is "AND"
\/ is "OR"
~ is "not" negation
-> is "if-then" implication
<=> is "if-and-only-if" equivalence
i^n is exponentiation operator

Terminology

A	B
Programming	Math
Array	Function
Index Set	Domain
f[e]	f(e)

CLI

Compile pluscal program:

pcal program.tla

Run TLA+ program:

tlc program.tla

Generate LaTeX:

tlatex program.tla

Generate PDF from LaTeX:

pdflatex program.tex

Resources

License

MIT

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
examples		examples
.gitignore		.gitignore
LICENSE		LICENSE
README.md		README.md

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

examples

examples

.gitignore

.gitignore

LICENSE

LICENSE

README.md

README.md

Repository files navigation

TLA+ Learning

Notes

Glossary

Syntax

Operators

Terminology

CLI

Resources

License

About

Releases

Packages

License

miguelmota/tla-learning

Folders and files

Latest commit

History

Repository files navigation

TLA+ Learning

Notes

Glossary

Syntax

Operators

Terminology

CLI

Resources

License

About

Topics

Resources

License

Stars

Watchers

Forks