> 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.
--
FL