Re: [tlaplus] Pluscal missing labels and TLA+ nested tuples errors

I haven't tried to understand your spec but here's what I see just looking at the module.

On 9 Feb 2022, at 23:49, marius...@kernkonzept.com <marius.melzer@xxxxxxxxxxxxxxx> wrote:

Hi,

I'm new to TLA+, so sorry for the maybe entry level questions. I'm trying to model a webrtc offer/answer exchange where both peers may send an offer at an arbitrary point in time.

1) I get an error at inb[0][0] in the definition of InboxOfferNoInc (which shall make sure that the offer numbers in the inbox are always increasing for the same type of message). Is it not possible to access nested tuples in that way or is where does the error come from?

you probably meant to write "=" instead of "==" on the right-hand side (in TLA+, "==" means "is defined as", not "equals", and it cannot be used inside expressions).

2) I'm getting a lot of missing label errors (when trying to translate the PlusCal to TLA+ in the toolbox) at strange lines, e.g. at line 40 (peers[peer].offerNo := peers[peer].offerNo + 1;). My understanding of Pluscal is that whereever I put a label, I allow a switch between processes at this point, right? If that's correct, I do not want to put more labels in my code. Could somebody explain me (maybe at the example of l. 40) why there need to be additional labels?

PlusCal allows only one assignment to the same variable in a group of statements between two labels. The variable here is "peers", and therefore each assignment to a different field of peers[peer] counts as an assignment to the same variable.

However, you can combine these assignments into one multi-assignment and write

peers[peer].makingOffer := TRUE || peers[peer].pendingOffer := ... || peers[peer].offerNo := ...

The "send" macro should then be moved before these assignments so that the old offerNo is sent (since apparently that's what you intend).

For full information about labeling rules, please check the PlusCal reference manual.

Hope this helps,

Stephan

Code:

-------------------------------- MODULE offeranswer --------------------------------

EXTENDS Naturals, TLC

THEOREM makingOffer == \A p \in 1..2: ~peers[p].makingOffer ~> peers[p].makingOffer
THEOREM sendingAnswer == \A p \in 1..2: ~peers[p].sendingAnswer ~> peers[p].sendingAnswer
InboxOfferNoInc(inb) == \A e \in Tail(inb): inb[0][0] == e[0] -> e[1] > inb[0][1]
THEOREM inboxOffer == \A p \in 1..2: Len(inbox[p]) < 2 \/ InboxOfferNoInc(inbox[p])

(* --algorithm offeranswer
variables peers = [ peer \in 1..2 |-> [ makingOffer |-> FALSE, pendingOffer |-> NULL, sendingAnswer |-> FALSE, offerNo |-> 1 ] ],
inbox = [ peer \in 1..2 |-> <<<>>> ],
localDesc = [ peer \in 1..2 |-> <<<0, 0>>> ],
remoteDesc = [ peer \in 1..2 |-> <<<0, 0>>> ],
lastAccepted = [ peer \in 1..2 |-> 0 ],
offerPeer = 1;

macro pop(queue, element) begin
await queue /= <<<>>>;
element := Head(queue);
queue := Tail(queue);
end macro;

macro send(sender, type, val) begin
inbox[(sender + 1) % 2] := Append(inbox[(sender + 1) % 2], <<<type, val>>>)
end macro;

macro setDesc(queue, peer, offerNo) begin
queue := <<<peer, offerNo>>>;
assert offerNo > lastAccepted[peer]
end macro;

procedure sendOffer(peer) begin
SendOffer:
if ~peers[peer].makingOffer then
peers[peer].makingOffer := TRUE;
AfterCreateOffer:
peers[peer].pendingOffer := peers[peer].offerNo;
send(peer, "offer", peers[peer].offerNo);
peers[peer].offerNo := peers[peer].offerNo + 1;
end if;
return;
end procedure;

procedure receiveOffer(peer, offerNo) begin
ReceiveOffer:
if peers[peer].makingOffer /\ peer = offerPeer then return; end if;
if peers[peer].sendingAnswer then return; end if;
peers[peer].pendingOffer := NULL;
peers[peer].makingOffer := FALSE;
peers[peer].sendingAnswer := FALSE;
SetRemoteDescOnOffer:
setDesc(remoteDesc[peer], (peer + 1) % 2, offerNo);
call sendAnswer(peer, offerNo);
return;
end procedure;

procedure sendAnswer(peer, offerNo) begin
SendAnswer:
setDesc(localDesc[peer], (peer + 1) % 2, offerNo);
send(peer, "answer", offerNo);
peers[peer].sendingAnswer := FALSE;
return;
end procedure;

procedure receiveAnswer(peer, offerNo) begin
ReceiveAnswer:
setDesc(localDesc[peer], peer, offerNo);
SetRemoteDescOnAnswer:
setDesc(localDesc[peer], peer, offerNo);
lastAccepted[peer] := offerNo;
return;
end procedure;

process peer \in 1..2
variables message = NULL
begin P:
while True do
either
call sendOffer(peer);
or
pop(inbox[peer], message);
if message[0] = "offer" then
call receiveOffer(peer, message[1]);
else
call receiveAnswer(peer, message[1]);
end if;
end either;
end while;
end process;

end algorithm; *)

=======================================================================

Thanks in advance!

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d20f4ef0-19c2-474c-b969-f0ebff2c2910n%40googlegroups.com.