Re: [tlaplus] Statements in TLA

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On 19 May 2024, at 11:24, marta zhango <martazhango@xxxxxxxxx> wrote:

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.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e6ae5a2d-4fed-4a6b-83f5-e211a540737bn%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/006C3949-160B-4F99-AFF1-86A3652A7851%40gmail.com.