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

Re: [tlaplus] Statements in TLA





On 19 May 2024, at 15:51, marta zhango <martazhango@xxxxxxxxx> wrote:

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 ?

On Monday, May 20, 2024 at 1:36:27 AM UTC+12 Andrew Helwer wrote:
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

On Sunday, May 19, 2024 at 9:18:13 AM UTC-4 marta zhango wrote:
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 ?

On Sunday, May 19, 2024 at 11:08:42 PM UTC+12 marta zhango wrote:

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 ?





On Sunday, May 19, 2024 at 11:01:36 PM UTC+12 Stephan Merz wrote:
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

On 19 May 2024, at 12:44, marta zhango <marta...@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+u...@xxxxxxxxxxxxxxxx.

-- 
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/2191de5f-07fa-4779-b748-dc1d808a3a05n%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/C6FB24BD-9911-4FE0-A4A5-F5F9F4943DD2%40gmail.com.