Hi Chris,
This sounds like a reasonable enhancement of the PlusCal language. We'll check that it doesn't change the translation of any files now accepted by the translator and will then take a look at what you have done. If it looks good, we'll add it to the next release. Thanks for the suggestion and the implementation.
By the way, the TLA+ specs of the translation say that they are valid only for the version of PlusCal at the date indicated at the beginning of the spec. I think those versions are now 10 years old and a number of changes have been made to PlusCal since then. I stopped keeping the specs up to date because I had too many other things to do. I didn't think there was too much point to keeping the specs current, since no one was going to use them to understand the semantics of PlusCal.
Leslie
On Friday, June 23, 2017 at 3:26:39 PM UTC-7, Chris Pacejo wrote:
Hi, I have found it desirable in PlusCal to be able to issue a call immediately followed by a goto without an intervening label (for example, in certain cases inside a with block). I see no reason why this relaxation of the labeling rules should be invalid (indeed, it is not much different from the call-followed-by-return case).
Attached please find a patch which adds this feature to the PlusCal compiler. Feedback would be appreciated as I'm sure I've missed something. In particular I'm not sure which of the various .tla files in the source tree are kept up-to-date (at least one of them has "Old" in its name); I'd be glad to also modify the relevant modules if I can be pointed in the right direction. I have tested the patch and it seems to work for my purposes.