[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

You can find the answer to this question by looking up "call" in the index of the PlusCal manual and going to the end of that discussion.  


On Thursday, February 28, 2019 at 4:04:16 PM UTC-8, 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?

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.