IncrementClock is a procedure. Procedure calls must be
immediately followed by a return, a label, or a goto. If IncrementClock
is only one step (only has one label), then you should be able to
inline it or make it a macro. That will fix the issue, I believe.
(Also, word of warning: if the clock can always increment and has no maximum then the model will be unbound and TLC may not terminate.)
On 2/28/19 6:03 PM, fwefew 4t4tg wrote:
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.