*** Real-Time Maude 2.1 specification of RC component of AER/NCA *** protocol suite. *** By Peter Csaba Olveczky *** Adds to the sender the list of times when each message is sent. *** Four adjustment come immediately to mind to run the protocol separately: *** 1. Every ms a message *** ncarcDataPacket(sequenceNumber, timestamp, retransmissionFlag) *** is attempted sent by the sender. *** 2. The repairserver only relays mesages. *** 3. The receiver does everything it is supposed to do. (tomod NCA-RC is including LINK . including COMMON-CLASSES . including TICK-RULE . including ENVIRONMENT . including SHARED-ATTS . protecting ORDERED-NAT-TIME-LIST . protecting POSRAT-TIME-DOMAIN . *** Including rationals including min, max msg ncarcDataPacket : NzNat Time Bool -> LargePacket . *** usage: ncarcDataPacket(seqNo, timestamp, retransmissionflag) msg ccmPacket : Oid Nat Time Bool -> Packet . *** usage : ccmPacket(originator, sequenceNo, timeStamp, retransmissionFlag) *** In case we want to reset the isNominee flag: msg NAMPacket : Bool -> Msg . *** usage: NAMPacket(receiverIsNominee?) class RCsender | timerNominee : DefOid, *** nominee when timer set winSize : PosRat, winLowerSeq : Nat, dupLowerSeq : Nat, *** no of ccmPackets with seqNo winLowerSeq maxSeqSent : Nat, *** seqNo of last original data packet sent smoothedRTT : Int, rttVariance : Int, ccmTimeout : Time, ssThreshold : PosRat, *** threshold for slower winSize-increase backOffFactor : Nat, *** no of times the timer has expired in a row fastRecovFlag : Bool, *** fast recovery mode? fastRecovSeq : Nat, *** last seqNo for which should stay in fR mode maxBurstCount : Nat, *** number of original data packets sent *** since last ccm packet received ccmTimer : TimeInf . subclass RCsender < Clock Sender . subclass RCsender < NCANOM-NCARCsender . *** attribute "csmNominee" class RCsenderAlone | sendDataTimer : TimeInf, *** Timer to send data. Initialized to 2000 *** to let the system find a nominee first. nextNoToSend : NzNat, *** Next message number to send. sentTimes : OrderedTimeList . *** Times of sendings of data packets. subclass RCsenderAlone < RCsender . vars DQ DQ' : DefOid . vars FROM TO : Oid . var SEQNO : NzNat . vars TIMESTAMP R CCMTO : Time . vars RTFLAG FRF : Bool . vars WS SST : PosRat . vars N WLS DLS MSS BOF FRS MBC : Nat . vars RTTV SRTT : Int . vars Q Q' Q'' Q''' : Oid . var CCMT : TimeInf . vars R R' : Time . var OS : OidSet . vars TI TI' : TimeInf . vars MC MC' : MsgConfiguration . var M : Msg . vars X Y : Bool . var TL : OrderedTimeList . crl [G2a] : (ccmPacket(FROM, SEQNO, TIMESTAMP, RTFLAG) from Q to TO) < TO : RCsender | csmNominee : DQ > => < TO : RCsender | > if FROM =/= DQ . *** Use cases G2 to G10: rl [G2b] : (ccmPacket(FROM, SEQNO, TIMESTAMP, RTFLAG) from Q to TO) < TO : RCsender | clock : R, csmNominee : FROM, winSize : WS, winLowerSeq : WLS, dupLowerSeq : DLS, maxSeqSent : MSS, smoothedRTT : SRTT, rttVariance : RTTV, ccmTimeout : CCMTO, ssThreshold : SST, backOffFactor : BOF, fastRecovFlag : FRF, fastRecovSeq : FRS, maxBurstCount : MBC, ccmTimer : CCMT > => < TO : RCsender | winSize : (if (SEQNO =/= WLS and FRF and FRS < max(SEQNO, WLS)) then max(min(SST, 256), 1) else (if (SEQNO =/= WLS and (not FRF) and 3 < newDupLowerSeq(SEQNO, WLS, DLS)) then max(min(max(g7winSize(SEQNO, WLS, FRF, WS, SST) / 2, 2) + 3, 256), 1) else (if (SEQNO =/= WLS and FRF and max(SEQNO, WLS) <= FRS) then max(min(g7winSize(SEQNO, WLS, FRF, WS, SST) + 1, 256), 1) else g7winSize(SEQNO, WLS, FRF, WS, SST) fi) fi) fi), winLowerSeq : max(SEQNO, WLS), dupLowerSeq : newDupLowerSeq(SEQNO, WLS, DLS), smoothedRTT : (if RTFLAG then SRTT else (if SRTT == 0 then max(1, R - TIMESTAMP) else (SRTT + (max(1, R - TIMESTAMP) - SRTT) quo 8) fi) fi), rttVariance : (if RTFLAG or (SRTT == 0) then RTTV else (if RTTV == 0 then abs(max(1, R - TIMESTAMP) - SRTT) else RTTV + ((abs(max(1, R - TIMESTAMP) - SRTT) - RTTV) quo 4) fi) fi), ssThreshold : (if (SEQNO =/= WLS and (not FRF) and (3 < newDupLowerSeq(SEQNO, WLS, DLS))) then max(g7winSize(SEQNO, WLS, FRF, WS, SST) / 2, 2) else SST fi), ccmTimeout : (if RTFLAG then CCMTO else (if SRTT == 0 then max(1, R - TIMESTAMP) else (if RTTV == 0 then (4 * abs(max(1, R - TIMESTAMP) - SRTT)) + (SRTT + (max(1, R - TIMESTAMP) - SRTT) quo 8) else (SRTT + (max(1, R - TIMESTAMP) - SRTT) quo 8) + 4 * (RTTV + ((abs(max(1, R - TIMESTAMP) - SRTT) - RTTV) quo 4)) fi) fi) fi), fastRecovFlag : (if FRF then max(SEQNO, WLS) <= FRS else (3 <= newDupLowerSeq(SEQNO, WLS, DLS)) fi), fastRecovSeq : (if (SEQNO =/= WLS and FRF and FRS < max(SEQNO, WLS)) then 0 else (if (SEQNO =/= WLS and (not FRF) and 3 < newDupLowerSeq(SEQNO, WLS, DLS)) then (max(WLS, SEQNO) + g7winSize(SEQNO, WLS, FRF, WS, SST)) - 1 else FRS fi) fi), backOffFactor : 1, maxBurstCount : 0, ccmTimer : (if MSS < max(WLS, SEQNO) then INF else CCMT fi) > . op newDupLowerSeq : Nat Nat Nat -> Nat . eq newDupLowerSeq(SEQNO, WLS, DLS) = if SEQNO == WLS then DLS + 1 else (if WLS < SEQNO then 0 else DLS fi) fi . op g7winSize : Nat Nat Bool PosRat PosRat -> PosRat . *** Gives the winSize at the line "if (fastRecovFlag == TRUE)" *** in the protocol: eq g7winSize(SEQNO, WLS, FRF, WS, SST) = (if (FRF or (SEQNO <= WLS)) then WS else max(min((if (WS <= SST) then (WS + 1) else (WS + (1 quo floor(WS))) fi), 256), 1) fi) . *** Use case G.11. The following function decides whether a new data packet *** can be sent "now": op sendAllowed : Nat Nat PosRat Bool Nat -> Bool . *** usage: sendAllowed(maxSeqSent, winLowerSeq, winSize, fastRecFlag, *** maxBuCount) eq sendAllowed(MSS, WLS, WS, FRF, MBC) = (MSS < (WLS + (WS - 1))) and (if FRF then (MBC < 2) else (MBC < 4) fi) . *** Use case G12. Sending is attempted every ms: rl [G12] : < Q : RCsenderAlone | children : OS, clock : R, csmNominee : DQ, sendDataTimer : 0, nextNoToSend : NZN, maxSeqSent : MSS, winLowerSeq : WLS, winSize : WS, fastRecovFlag : FRF, maxBurstCount : MBC, ccmTimer : TI, timerNominee : DQ', backOffFactor : BOF, ccmTimeout : CCMTO, sentTimes : TL > => if (NZN == MSS + 1) and sendAllowed(MSS, WLS, WS, FRF, MBC) then < Q : RCsenderAlone | sendDataTimer : 1, nextNoToSend : NZN + 1, maxSeqSent : MSS + 1, ccmTimer : (if WLS <= MSS then (BOF * CCMTO) else INF fi), maxBurstCount : MBC + 1, timerNominee : (if WLS <= MSS then DQ else DQ' fi), sentTimes : TL ++ R > multiSend(ncarcDataPacket(NZN, R, false), Q, OS) else < Q : RCsenderAlone | sendDataTimer : 1 > fi . *** G13: rl [G13] : < Q : RCsender | ccmTimer : 0, timerNominee : DQ, ssThreshold : SST, backOffFactor : BOF, winSize : WS, winLowerSeq : WLS, maxSeqSent : MSS, fastRecovFlag : FRF, fastRecovSeq : FRS, maxBurstCount : MBC > => < Q : RCsender | ccmTimer : INF, ssThreshold : (if DQ == noOid then 64 else max(WS / 2, 2) fi) , backOffFactor : (if DQ == noOid then 1 else min(2 * BOF, 64) fi), winSize : 1, winLowerSeq : MSS + 1, fastRecovFlag : false, fastRecovSeq : 0, maxBurstCount : 0 > . *** Use case G14. I do not really understand when this should happen, *** and who will update the csmNominee to be noOid. *** However, for completeness, here it is: msg nomineeIs : DefOid -> Msg . rl [G14] : nomineeIs(DQ) < Q : RCsenderAlone | csmNominee : DQ', ccmTimeout : R > => < Q : RCsenderAlone | csmNominee : DQ, ccmTimeout : (if (DQ == noOid and DQ =/= DQ') then 1000 else R fi) > . *** ******************************** *** Timed behavior of sender *** ******************************** eq mte(< Q : RCsenderAlone | ccmTimer : TI, sendDataTimer : TI' >) = min(TI, TI') . eq delta(< Q : RCsenderAlone | clock : R', ccmTimer : TI, sendDataTimer : TI' >, R) = < Q : RCsenderAlone | clock : R' + R, ccmTimer : TI monus R, sendDataTimer : TI' monus R > . *** **************** *** REPAIRSERVER *** *** **************** class RCrepairserver . subclass RCrepairserver < Repairserver . class RCrepairserverAlone . subclass RCrepairserverAlone < RCrepairserver . *** In a first attempt, the repairserver just forwards messages *** to its children: rl [RCrepserv] : (ncarcDataPacket(NZN, R, X) from Q to Q') < Q' : RCrepairserverAlone | children : OS > => < Q' : RCrepairserverAlone | > multiSend(ncarcDataPacket(NZN, R, X), Q', OS) . rl [RCrepserv2] : (ccmPacket(Q, NZN, R, X) from Q'' to Q') < Q' : RCrepairserver | repairserver : Q''' > => < Q' : RCrepairserver | > send(ccmPacket(Q, NZN, R, X), Q', Q''') . *** Timed behavior is trivial: eq delta(< Q : RCrepairserverAlone | >, R) = < Q : RCrepairserverAlone | > . eq mte(< Q : RCrepairserverAlone | >) = INF . *** ************** *** RECEIVER ***** *** ************** *** The sender has the attributes "isNominee" (inherited from *** sharedRSNCA) and a store of message *** sequence numbers received, together with their time stamps. *** To send the next outstanding packet number to the sender, *** the receiver needs to know this number, which normally would be in *** the readNextSeq attribute of the combined protocol. In the separate *** protocol, we need a list of message numbers to compute this value. class RCreceiver . subclass RCreceiver < SharedRSNCA . class RCreceiverAlone | msgRcvd : OrderedNzNatList . subclass RCreceiverAlone < RCreceiver . vars NNL NNL' : OrderedNzNatList . vars NZN NZN' NZN'' NZN''' NZN'''' : NzNat . var R : Time . op lowestOutstanding : OrderedNzNatList -> NzNat . eq lowestOutstanding(nil) = 1 . eq lowestOutstanding(NZN ++ NNL) = if NZN =/= 1 then 1 else firstMissing(NZN ++ NNL) fi . op firstMissing : OrderedNzNatList -> NzNat . eq firstMissing(NZN ++ NZN' ++ NNL) = if (NZN + 1) =/= NZN' then (NZN + 1) else firstMissing(NZN' ++ NNL) fi . eq firstMissing(NZN) = NZN + 1 . *** Use case H1: rl [H1] : (ncarcDataPacket(NZN, R, X) from Q to Q') < Q' : RCreceiverAlone | isNominee : Y, msgRcvd : NNL > => < Q' : RCreceiverAlone | msgRcvd : add(NZN, NNL) > (if (Y and (not (NZN inList NNL))) then send(ccmPacket(Q', lowestOutstanding(add(NZN, NNL)), R, X), Q', Q) else none fi) . rl [resetIsNominee] : (NAMPacket(X) from Q' to Q) < Q : RCreceiverAlone | > => < Q : RCreceiverAlone | isNominee : X > . *** Subsumed by B10B11E4 in combined protocol. *** Timed behavior is trivial: eq delta(< Q'' : RCreceiverAlone | >, R) = < Q'' : RCreceiverAlone | > . eq mte(< Q'' : RCreceiverAlone | >) = INF . endtom)