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

Re: End labels

> You can simply replace "goto endlbl" by "goto Done" and
> remove the bogus label "endlbl".
Thank you. I'll use it tomorrow.

> then I'm sorry, PlusCal is not the language for you; you'll have to
> write it in TLA+. There are many more interesting specs that can be
> written in TLA+ and are difficult or practically impossible to write
> in PlusCal. 
Sure but we will no longer be able to benefit from the first-rate work
done by PlusCal as regards states and transitions modelization.
But anyway for the moment I only modify by hand the Init macro
when generated. But I need to remember to modify it every time I
generate it again.