Q about ASSUME

[n s]

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

[Leslie Lamport]

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

[n s]

Ok, thanks for clarifying that Leslie. I think I understand.

[Aman Shaikh]

Wouldn't it be possible to make N > 0 an invariant and specify it as such in .cfg file provided to TLC?

aman

[n s]

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