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

[tlaplus] Strange label enforcement in plus-cal?

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.