Statements in TLA

130 views
Skip to first unread message

marta zhango

unread,
May 19, 2024, 5:24:28 AMMay 19
to tlaplus
Have seen that statements in TLA are of the form [A]_p, where A is an action and p is a property.

But what are things without action formalism like

Cardinality(assignments[t])

and expressions such as
/\ assignments \in [Tasks -> SUBSET CPUs]

and

IsSorted(seq) == \A i, j \in 1..Len(seq): i < j => seq[i] <= seq[j]

What are the latter ? Because they do not look like TLA statements
in the form of [A]_p.

Stephan Merz

unread,
May 19, 2024, 5:38:51 AMMay 19
to tla...@googlegroups.com
In fact, there is no such thing as "statements" in TLA+, only formulas of different levels (constant, state, action, temporal). This is not nitpicking, but quite a fundamental distinction.

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e6ae5a2d-4fed-4a6b-83f5-e211a540737bn%40googlegroups.com.

marta zhango

unread,
May 19, 2024, 6:44:49 AMMay 19
to tlaplus
I actually need some nitpicking.  TLA is a scheme for precise and clear description,
whereas the documentation is not.  

What are the basic constructs then ?  As this is what I would like to neatly summarise.

Stephan Merz

unread,
May 19, 2024, 7:01:36 AMMay 19
to tla...@googlegroups.com
I don’t know documentation you looked at.

From a user’s perspective, Leslie Lamport’s video lectures [1] and/or Hillel Wayne’s Web site and book [2] are probably the best introduction (with the latter focusing on PlusCal, but this includes TLA+ expressions).

If you are looking for more mathematical descriptions covering the language and its semantics, Specifying Systems [3], the original paper introducing TLA (but not the specification language TLA+) [4] or an old paper of mine [5] may be helpful.

Hope this helps,
Stephan

marta zhango

unread,
May 19, 2024, 7:08:42 AMMay 19
to tlaplus

Actually, it is for TLA+ itself.  You have mentioned: constant, state, action, temporal.  Any important
others?  Would you be so kind to show a general syntax for each ?

marta zhango

unread,
May 19, 2024, 9:18:13 AMMay 19
to tlaplus
Systems are specified as formulas.  I also see functions described using logical connectives such as
implication (=>), conjunction (∧),  disjunction (V) and quantification (\A, \E).

Is TLA+ specified as formulas or functions ? Or something else ?

Andrew Helwer

unread,
May 19, 2024, 9:36:27 AMMay 19
to tlaplus
Examples of constant-level expressions:
 - 5 + 15
 - 0 .. 10
 - {1, 2, 3, 4, 5}
 - "foobar"
 - op, where op was declared as op == (constant expression)
 - x, where x was declared as CONSTANT x

Examples of state-level expressions:
 - n + 5, where n was declared as VARIABLE n
 - op, where op was declared as op == (state-level expression)

Examples of action-level expressions:
 - z' = z + 5, where z was declared as VARIABLE z
 - op, where op was declared as op == (action-level expression)

Examples of temporal-level expressions:
 - <>[](x > 5), where x was declared as VARIABLE x
 - P ~> Q, where P and Q are action-level expressions or below (I believe)

There is additional related terminology outside of this:
 - State: an assignment of values to variables; variables are accessed with no prime, like x
 - Step: A pair of successive states, where variables are addressed by being primed or not, like x' or x
 - Behavior: An infinite sequence of states
 - Spec: A set of behaviors comprising the possible executions of the system you are modeling
 - Formula: a bit of an imprecise term but is usually used to refer to temporal formulas, so either specs or temporal-level expressions

Constant-level expressions are just that, they can be evaluated without reference to any state or anything by just looking at them. State-level expressions can only be evaluated within the context of a specific state. Action-level expressions can only be evaluated within the context of a specific step. Temporal-level expressions can only be evaluated within the context of a specific behavior, or spec.

Actually I'm a bit confused about the last one. It would seem to me that <>P and []<>P are two different levels of formulas, since <>P can be true or false of a specific behavior whereas []<>P seems to be a statement over multiple behaviors. Can anybody help me out here?

Anyway how this all helped.

Andrew Helwer

Andrew Helwer

unread,
May 19, 2024, 9:47:13 AMMay 19
to tlaplus
Oh I figured out the difference myself. []<>P can of course be true or false of a specific behavior. <>P is true if P is true at least once at any point in the behavior. []<>P is only true when, if P becomes false after becoming true, it eventually becomes true again.

Andrew

marta zhango

unread,
May 19, 2024, 9:51:50 AMMay 19
to tlaplus
Rather than examples, I was hoping for a general syntax for the expressions described.

From what I understand, TLA+ is based upon Specifications that use various statements expressed
by mathematical-like formulas.  With Logical Connectives used to combine and relate statements.
such as Implication (=>), Conjunction (/\), Disjunction (\/), and Quantification (\A, \E).

How do definitions, functions, properties and actions fits in all this ?

Andrew Helwer

unread,
May 19, 2024, 10:06:49 AMMay 19
to tlaplus
You can see a grammar for the language here if you want: https://github.com/tlaplus-community/tree-sitter-tlaplus/blob/main/grammar.js

Definitions are just any definition of a symbol, like VARIABLE x, CONSTANT y, z == ...

Functions are maps between a domain set and a range set. There are a few different ways to write them.

Properties are temporal-level expressions.

Actions are action-level expressions.

Andrew

Stephan Merz

unread,
May 19, 2024, 10:08:13 AMMay 19
to tla...@googlegroups.com

On 19 May 2024, at 15:51, marta zhango <marta...@gmail.com> wrote:

Rather than examples, I was hoping for a general syntax for the expressions described.

marta zhango

unread,
May 19, 2024, 10:23:31 AMMay 19
to tlaplus
In TLA+, specifications use statements that are either Definitions or
Assertions.  Definitions introduce new symbols and specify their
meaning, whilst assertions describe properties and constraints that
the system must satisfy.

Would you consider Functions and Properties as Assertions ? How about
actions ? Do actions form part of an assertion ?  I have not seen actions
on their own.



Andrew Helwer

unread,
May 19, 2024, 10:30:02 AMMay 19
to tlaplus
Within your definition/assertion view of TLA+ functions can be used in either definitions or assertions. Properties are generally only used in assertions, with the exception of the root Spec definition itself which is both a property and a definition. Actions are generally used in definitions, but much more rarely are used as assertions of the form <><<A>>_vars or [][A]_vars.

Actions are any statement containing both primed and unprimed variables. So you probably have seen them!

Andrew

marta zhango

unread,
May 19, 2024, 11:16:30 AMMay 19
to tlaplus
Yes, I have seen actions as statements with primed and unprimed variables.  Is my general description
of the TLA+ syntax as either a definition or assertion correct ?  Or would I have to include other basic
things that would also constitute a specification statement?

I understand most things, but to explain them to others is not straightforward right now.

Andrew Helwer

unread,
May 19, 2024, 3:26:33 PMMay 19
to tlaplus
I think that's a pretty good way to think about it, and it is the way I think about it when writing a spec. Definitions describe how your system generates state traces, and assertions are things you want to be true of those state traces. As you get more advanced you'll realize that the line between definition and assertion is quite blurry and occasionally a definition can be used as an assertion - for example when checking refinement - or an assertion can be used as a definition - for example to constrain generated states -  but the definition/assertion categorization will serve you well enough.

Andrew

Hillel Wayne

unread,
May 20, 2024, 1:53:12 PMMay 20
to tla...@googlegroups.com

Expert mode: find a use-case for <>[]<>P (or prove it's just []<>P or something)

H

Andrew Helwer

unread,
May 21, 2024, 10:05:39 AMMay 21
to tlaplus
I do think intuitively <>[]<>P is equivalent to []<>P although I tried for about an hour to prove so without success. A good sign that I really need to work on my proof skills!

Andrew

Stephan Merz

unread,
May 21, 2024, 10:14:05 AMMay 21
to tla...@googlegroups.com
OK, one half is easy because F => <>F is valid for any temporal formula F.

The other half needs some index reasoning:

sigma |= <>[]<>P means that sigma[n ..] |= []<>P for some n \in Nat. [1]
Thus, for any m >= n, there is some k >=m such that sigma[k ..] |= P.    (*)

You want to prove that sigma |= []<>P, i.e., for any i \in Nat there is some j >= i such that sigma[j ..] |= P.

If i >= n, this follows from (*).
If i < n, find a suitable j by applying (*) to n.

Stephan

[1] I write sigma[n ..] to denote the suffix of behavior sigma from index n.


Karolis Petrauskas

unread,
May 21, 2024, 10:14:25 AMMay 21
to tla...@googlegroups.com
I probably took a too simple way. This says OK for me.

---- MODULE a ----
EXTENDS TLAPS

THEOREM ASSUME NEW TEMPORAL P, <>[]<>P PROVE []<>P
BY PTL

====

Karolis

Andrew Helwer

unread,
May 21, 2024, 12:10:01 PMMay 21
to tlaplus
Leslie emailed me to tell me that he actually covered this exact topic in section 3.4.2.7 of his new book! https://lamport.azurewebsites.net/tla/science.pdf

Quoting:

"You might expect that we can keep constructing more and more complicated operators like []<><>[][]<>[] with sequences of [] and <>. We can’t. Any such sequence is equivalent to [], <>, <>[] or []<>."

Andrew
Reply all
Reply to author
Forward
0 new messages