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.
Leslie
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