Jumping to end of process in PlusCal?

[Elliott Jin]

Hello,

Is there a canonical way to indicate "jump to the end of the process" in PlusCal?  I've just been handling this by adding an extra label at the end:

writer_done: 

skip;

 

and then using goto as follows:

if (should_abort) {

goto writer_done;

} 

 

But I was wondering if there was an existing keyword / shorter way to handle this.

Thanks!

-Elliott

[Leslie Lamport]

There is an implicit label "Done" at the end of the process, so you can write

   goto Done

Leslie

[Elliott Jin]

Thanks!  This approach is much nicer.