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

*From*: n s <nedsri1988@xxxxxxxxx>*Date*: Mon, 10 Apr 2023 16:42:49 -0700 (PDT)*References*: <93e2c0c4-5f31-43dd-93ab-cd360381c19bn@googlegroups.com> <2a1a2f84-bf31-4702-bef5-af187da9f5e1n@googlegroups.com> <afff59e4-648f-4085-9071-fce7320ae6b5n@googlegroups.com> <c3da8616-a9a3-4a11-9987-a453af1f8366n@googlegroups.com>

An invariant is a property that you are trying to prove so making it an assumption wouldn't work

On Monday, April 10, 2023 at 2:28:32 PM UTC-7 Aman Shaikh wrote:

Wouldn't it be possible to make N > 0 an invariant and specify it as such in .cfg file provided to TLC?amanOn Monday, April 10, 2023 at 3:55:38 PM UTC-4 n s wrote:Ok, thanks for clarifying that Leslie. I think I understand.On Monday, April 10, 2023 at 11:34:18 AM UTC-7 Leslie Lamport wrote:What you would like ASSUME N > 0 to mean if N is a variable is

irrelevant. It's what the math says it should mean that counts. And

the TLA formula N > 0 for a variable N asserts that N > 0 is true in

the first state of a behavior. This is something that would be of

very little use. What you would like to say would be asserted by

ASSUME [](N > 0). If you want to assert that for the purpose of

proving properties, you can just make it a THEOREM without a proof.

If you want to tell TLC to make that part of the spec, you would have

to give it the formula [](N > 0) /\ ... as the specification. It would

be impossible for TLC to check specifications written as arbitrary

TLA+ formulas. It has been decided that it is more important to

devote effort to making checking as efficient as possible than

to make TLC handle a larger class of TLA+ formulas as

specifications. In this particular case, it's very simple to

rewrite a formula of the form

[](N > 0) /\ Init /\ [][Next]_vars

so it has the form

Init /\ [][Next]_vars

that TLC accepts.

LeslieOn Monday, April 10, 2023 at 11:06:42 AM UTC-7 nedsr...@xxxxxxxxx wrote:Hello, perhaps I'm too steeped in PL ideas of well-typed programs to see it, but I am still not sure I've completely grasped why ASSUME can't be applied to variables. For example if N is a constant and I have the assumption ASSUME N \in Nat /\ N > 0 then I'm saying that my specification is limited to those traces in which the constant N can only be a Nat greater than 0. Specifically I am excluding states in which N violates this constraint. Why can't I say the same thing about a variable n instead of a constant N? Namely that I am limiting my specification to those traces in which n is a Nat greater than 0.thanks

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/a16d9a35-3a68-4643-9743-610ca2823d4en%40googlegroups.com.

**References**:**[tlaplus] Q about ASSUME***From:*n s

**[tlaplus] Re: Q about ASSUME***From:*Leslie Lamport

**[tlaplus] Re: Q about ASSUME***From:*n s

**[tlaplus] Re: Q about ASSUME***From:*Aman Shaikh

- Prev by Date:
**[tlaplus] Re: Q about ASSUME** - Next by Date:
**[tlaplus] Re: Priming TLA+ formulas** - Previous by thread:
**[tlaplus] Re: Q about ASSUME** - Next by thread:
**[tlaplus] Priming TLA+ formulas** - Index(es):