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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Tue, 21 May 2024 09:10:01 -0700 (PDT)*References*: <e6ae5a2d-4fed-4a6b-83f5-e211a540737bn@googlegroups.com> <006C3949-160B-4F99-AFF1-86A3652A7851@gmail.com> <6a37ca7d-e03e-4c5e-afc5-603b3ed5c736n@googlegroups.com> <D923A267-B96B-44F8-A7F3-54CECD8A4C8D@gmail.com> <2f021f54-5da3-4b47-ad23-1efd260a8244n@googlegroups.com> <78ca6604-e088-43dd-a184-9159f8ca9394n@googlegroups.com> <2673743f-02ee-47bd-91ee-8cf142fd41e6n@googlegroups.com> <feb13c29-ea41-4742-9497-5b979d1f6093n@googlegroups.com> <7b55e800-59e2-4ee1-967c-7fb1e9c7b8e9@gmail.com> <3e3e996b-e96b-432e-bdc1-80c3af1da0afn@googlegroups.com> <CAFteov+8Hr5Jy+CUvq2xW+ga02BZvXSTqZwrjqtXYamPpuFGgg@mail.gmail.com>

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

On Tuesday, May 21, 2024 at 10:14:25 AM UTC-4 Karolis Petrauskas wrote:

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

====KarolisOn Tue, May 21, 2024 at 5:05 PM Andrew Helwer <andrew...@xxxxxxxxx> wrote: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--On Monday, May 20, 2024 at 1:53:12 PM UTC-4 Hillel Wayne wrote:Expert mode: find a use-case for <>[]<>P (or prove it's just []<>P or something)

H

On 5/19/2024 8:47 AM, Andrew Helwer wrote:

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

--On Sunday, May 19, 2024 at 9:36:27 AM UTC-4 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 importantothers? 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.

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/feb13c29-ea41-4742-9497-5b979d1f6093n%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.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3e3e996b-e96b-432e-bdc1-80c3af1da0afn%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/ffb16bdb-1f2d-4717-8518-7d670f1e7501n%40googlegroups.com.

**References**:**[tlaplus] Statements in TLA***From:*marta zhango

**Re: [tlaplus] Statements in TLA***From:*Stephan Merz

**Re: [tlaplus] Statements in TLA***From:*marta zhango

**Re: [tlaplus] Statements in TLA***From:*Stephan Merz

**Re: [tlaplus] Statements in TLA***From:*marta zhango

**Re: [tlaplus] Statements in TLA***From:*marta zhango

**Re: [tlaplus] Statements in TLA***From:*Andrew Helwer

**Re: [tlaplus] Statements in TLA***From:*Andrew Helwer

**Re: [tlaplus] Statements in TLA***From:*Hillel Wayne

**Re: [tlaplus] Statements in TLA***From:*Andrew Helwer

**Re: [tlaplus] Statements in TLA***From:*Karolis Petrauskas

- Prev by Date:
**Re: [tlaplus] Statements in TLA** - Next by Date:
**[tlaplus] ToolBox GraphViz encountered problem after cleaning .tlaplus folder** - Previous by thread:
**Re: [tlaplus] Statements in TLA** - Next by thread:
**Re: [tlaplus] Statements in TLA** - Index(es):