[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Statements in TLA



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

[1] https://lamport.azurewebsites.net/video/videos.html 
[2] https://learntla.com/introduction/https://www.amazon.com/Practical-TLA-Planning-Driven-Development/dp/1484238281
[3] https://lamport.azurewebsites.net/tla/book.html
[4] https://lamport.azurewebsites.net/pubs/pubs.html#lamport-actions
[5] https://members.loria.fr/SMerz/papers/tla+logic2008.html

On 19 May 2024, at 12:44, marta zhango <martazhango@xxxxxxxxx> wrote:

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.

On Sunday, May 19, 2024 at 9:38:51 PM UTC+12 Stephan Merz wrote:
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 <marta...@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+u...@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/6a37ca7d-e03e-4c5e-afc5-603b3ed5c736n%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/D923A267-B96B-44F8-A7F3-54CECD8A4C8D%40gmail.com.