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

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

Looking up "print" in the index of the PlusCal manual will lead you to Section 2.3, which answers your question.


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.