Re: [tlaplus] End labels

[Stephan Merz <Stepha...@xxxxxxxxx>]

> Another clause that I would add to PlusCal is the clause "precondition" because the clause "variable" is not
> enough.
>  
> For instance if we had:
>  
> --algorithm test
> variable v = 0
> precondition VALIDPOINTER(p)
> etc.
>  
> we would have the translation:
>  
> Init ==
>   /\ v = 0
>   /\ VALIDPOINTER(p)

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

variable p \in ValidPointer

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

Regards,
Stephan