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?
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?
-------------------------------- 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; *)
=======================================================================