[tlaplus] Re: Q about ASSUME

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

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

On 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/2a1a2f84-bf31-4702-bef5-af187da9f5e1n%40googlegroups.com.