[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Q about ASSUME
Wouldn't it be possible to make N > 0 an invariant and specify it as such in .cfg file provided to TLC?
On 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
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.
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.
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/c3da8616-a9a3-4a11-9987-a453af1f8366n%40googlegroups.com.