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

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


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 --------------------------------


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
    if ~peers[peer].makingOffer then
      peers[peer].makingOffer := TRUE;
      peers[peer].pendingOffer := peers[peer].offerNo;
      send(peer, "offer", peers[peer].offerNo);
      peers[peer].offerNo := peers[peer].offerNo + 1;
    end if;
end procedure;

procedure receiveOffer(peer, offerNo) begin
      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;
      setDesc(remoteDesc[peer], (peer + 1) % 2, offerNo);
      call sendAnswer(peer, offerNo);
end procedure;

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

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

process peer \in 1..2
variables message = NULL
begin P:
  while True do
      call sendOffer(peer);
      pop(inbox[peer], message);
      if message[0] = "offer" then
        call receiveOffer(peer, message[1]);
        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.