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

Re: [tlaplus] End labels

> For such a simple case your proposed condition can equivalently be replaced by a set-valued initialization such as

> variable p \in ValidPointer 
It depends what you mean by the predicate VALIDPOINTER. It might be more complex. Or
more generally, it might be a predicate with no meaning declared by a constant and intended
to be used with an opaque data

> TLC would not be able to evaluate arbitrary predicates appearing in preconditions.

Yes its true. But it is to be used with tlaps. And with tlaps I think it might be very helpful. But
it's true if such a clause were added to PlusCal it should be reported that it doesn't work with
TLC so that users are not misled.