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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Sun, 19 May 2024 12:26:32 -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> <2191de5f-07fa-4779-b748-dc1d808a3a05n@googlegroups.com> <C6FB24BD-9911-4FE0-A4A5-F5F9F4943DD2@gmail.com> <b8d49384-8a9d-4b63-9b00-93bd52071d2dn@googlegroups.com> <2aa54871-76c5-4f68-9f37-d9b2913ddbd4n@googlegroups.com> <99fe2cdf-f1c1-46ed-8f5c-b93e978743c5n@googlegroups.com>

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

On Sunday, May 19, 2024 at 11:16:30 AM UTC-4 marta zhango wrote:

Yes, I have seen actions as statements with primed and unprimed variables. Is my general descriptionof the TLA+ syntax as either a definition or assertion correct ? Or would I have to include other basicthings that would also constitute a specification statement?I understand most things, but to explain them to others is not straightforward right now.On Monday, May 20, 2024 at 2:30:02 AM UTC+12 Andrew Helwer wrote: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!AndrewOn Sunday, May 19, 2024 at 10:23:31 AM UTC-4 marta zhango wrote: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 thatthe system must satisfy.Would you consider Functions and Properties as Assertions ? How aboutactions ? Do actions form part of an assertion ? I have not seen actionson their own.On Monday, May 20, 2024 at 2:08:13 AM UTC+12 Stephan Merz wrote:On 19 May 2024, at 15:51, marta zhango <marta...@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 expressedby 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 xExamples 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 expressionsConstant-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 HelwerOn 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 asimplication (=>), 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,StephanOn 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.StephanOn 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 likeCardinality(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/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/cecb6b92-da54-4f20-8964-a982838c873bn%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:*marta zhango

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

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

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

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

- Prev by Date:
**[tlaplus] Definitions inside and outside of an algorithm and macros** - Next by Date:
**[tlaplus] Re: Definitions inside and outside of an algorithm and macros** - Previous by thread:
**Re: [tlaplus] Statements in TLA** - Next by thread:
**[tlaplus] Definitions inside and outside of an algorithm and macros** - Index(es):