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?