Re: [tlaplus] Strange label enforcement in plus-cal?

[Hillel Wayne <hwayne@xxxxxxxxx>]

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

H

On 2/28/19 6:03 PM, fwefew 4t4tg wrote:

Consider this fragment:

1 procedure logMessage(op, procId, e)

2   variables clockId = 0;

3 begin

4  a99:call IncrementClock();

5  clockId := ClockIds[self];

6   MessageLog := Append(MessageLog, [ time |-> clockId, oper |-> op, pid |-> procId, datum |-> e]);

7  return;

8 end procedure;

Here the objecitve is to do all of the following in a single atomic step,

- increment a clock

- transfer the value of the clock for process ’self’ to a local variable

- append an entry to MessageLog

where MessageLog, ClockIds are globals. Hence I group everything under/with label ‘a99’.

However, when converting from Plus-Cal to TLA+ I see these errors,

Missing label line 5

Missing label line 7

But depending on what I want to do, this will break the atomicy I need. 

What limitation am I hitting, or what am I misunderstanding?

tlaplus@xxxxxxxxxxxxxxxx

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

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