*** AER/NCA repair service component for Real-Time Maude 2.1 *** By Peter Csaba Olveczky *** Since the stand-alone protocol is least independent *** of NCA-NOM and AER-RTT, *** we must somehow get new RTT estimates to use cases B13 and C13. *** Furthermore, the nominees must be provided, since *** not much work without knowing who is the nominee. *** We'd also need a nice fastRecovFlag value coming from somewhere, *** or just run cases where this is either true or false. *** To execute the protocol, the file appLayerX.maude reads the necessary files *** and including those of the definition of an "application layer" *** and some initial states. (tomod AER-RS is including LINK . protecting TIMED-RANDOM . including COMMON-CLASSES . including TICK-RULE . including SHARED-ATTS . including SHARED-MSGS . including ENVIRONMENT . protecting AER-TIME-DOMAIN . protecting INT . including ERROR-OBJECT . var DB : DataBuffer . vars Q Q' Q'' Q''' : Oid . var OS : OidSet . vars M M' : Msg . vars NZN NZN' NZN'' : NzNat . vars TI TI' TI'' : TimeInf . var DB : DataBuffer . vars R R' R'' R''' : Time . vars DQ DQ' : DefOid . vars MC MC' RTB : MsgConfiguration . vars NEMC NEMC' : NEMsgConfiguration . vars N N' N'' N''' : Nat . vars I I' : Int . vars X Y Z X' XX : Bool . vars DI DI' : DataInfo . vars NS NS' : NAKstates . var OS : OidSet . var BB : BoundedBuffer . vars ML ML' : MsgList . *** Just to refer/identify the various data packets sent by the "user" *** of the protocol, I let each data block from the upper layer be identified *** by some text, that is, some Qid. Furthermore, the "size" of the data *** block in terms of the number of packets is also indicated. The actual *** data part is not explicitly represented in the data packets relayed, but *** are given from the identifier and the sequence number. *** The last argument is (new for Boston) the desired send rate for *** these messages. That is, the rate at which the sender attempts a *** sending of a new data block. In the combined protocol this sending *** will depend on the sendAllowed check, which is tested at the *** frequency determined by the rate given above. msg dataBlock : Qid Oid NzNat Time -> Msg . *** dataBlock(content, senderObject, size, sendingRate) *** The actual data packets to send around: msg dataPacket : Qid NzNat Time Bool Bool Bool -> LargePacket . *** dataPacket(identifier, seqNo, timeStamp, firstSegmentFlag, *** segmentationFlag, reTransmissionFlag) msg NAKPacket : NzNat Nat Bool -> Packet . *** NAKPacket(seqNo, NAKcount, fastRepairFlag) class RSsender | nextSeq : NzNat, *** initially 1 SPMTimer : TimeInf, *** initially INF reTransBuf : MsgConfiguration, *** Retransmission buffer unsentDataPackets : DataBuffer, *** defined below sendDataTimer : TimeInf . *** When to TRY to send a data packet? subclass RSsender < Sender Clock . class RSsenderAlone . subclass RSsenderAlone < RSsender . *** Use case A.1. msg startRS : Oid -> Msg . *** Initializes the sender and starts the protocol. rl [A1] : startRS(Q) < Q : RSsender | children : OS, nextSeq : NZN, SPMTimer : TI > => < Q : RSsender | nextSeq : 1, SPMTimer : 4000 > multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) multiSend(SPMPacket(0), Q, OS) . rl [A2] : < Q : RSsender | nextSeq : s N, children : OS, SPMTimer : 0 > => < Q : RSsender | SPMTimer : 4000 > multiSend(SPMPacket(N), Q, OS) . *** I assume that the data packets of a big data block are supposed to be *** sent out one by one. The unsent data packets are placed in a buffer *** "unsentDataBuffer" of sort DataBuffer. The sent data packets are *** placed in the retransmission buffer. sort DataBuffer . op data : Qid NzNat NzNat Time -> DataBuffer . *** data(q, m, n, r) represents an unsent data packets m, m+1, m+2, ..., n *** stemming from one data block having "data" q, and sendRate r. op nil : -> DataBuffer . op __ : DataBuffer DataBuffer -> DataBuffer [assoc id: nil] . *** Receive data from "upper layer". Also starts the timer for sending *** data packets. I let the timer be 5000, just to be sure that some nominees *** are found before time: rl [A3getDataBlock] : dataBlock(Q, Q', NZN, R) < Q' : RSsender | unsentDataPackets : DB, sendDataTimer : TI, nextSeq : NZN' > => < Q' : RSsender | unsentDataPackets : (DB data(Q, 1, NZN, R)), sendDataTimer : (if TI == INF then (if NZN' == 1 then 5000 else R fi) else TI fi) > . *** Note that the data packets to be sent do not contain a NAK count, *** while the data packets in the retransmission buffer also has *** to keep record of the NAKcount. Therefore, I let *** MsgAndNAK be a wrapper taking a data packet message and a NAK count *** giving a new message (could be of another sort as well) containing *** both the original message and its NAK count. msg MsgAndNAK : Msg Nat -> Msg . *** usage: MsgAndNAK(message, NAKcountOfmessage) *** A3 -- sending of data packets, triggered by sendDataTimer, rl [A3send] : < Q : RSsenderAlone | children : OS, clock : R, unsentDataPackets : data(Q', NZN, NZN', R') DB, reTransBuf : RTB, nextSeq : NZN'', sendDataTimer : 0 > => < Q : RSsenderAlone | unsentDataPackets : (if NZN == NZN' then nil else data(Q', NZN + 1, NZN', R') fi) DB, reTransBuf : RTB MsgAndNAK(dataPacket(Q', NZN'', R, NZN == 1, NZN =/= 1 and NZN =/= NZN', false), 0), nextSeq : NZN'' + 1, sendDataTimer : (if NZN =/= NZN' then R' else sendRate(DB) fi) > multiSend(dataPacket(Q', NZN'', R, NZN == 1, NZN =/= 1 and NZN =/= NZN', false), Q, OS) . op sendRate : DataBuffer -> TimeInf . eq sendRate(nil) = INF . eq sendRate(data(Q, NZN, NZN', R) DB) = R . *** Use case A4. *** Set the retransmission field accordingly in the packet sent: rl [A4] : (NAKPacket(NZN, N, X') from Q'' to Q) < Q : RSsender | children : OS, reTransBuf : (MC MsgAndNAK(dataPacket(Q', NZN, R, X, Y, Z), N')) > => < Q : RSsender | reTransBuf : (MC MsgAndNAK(dataPacket(Q', NZN, R, X, Y, if N' < N then true else Z fi), max(N, N'))) > (if N' < N then multiSend(dataPacket(Q', NZN, R, X, Y, true), Q, OS) else none fi) . *** Use case A5. *** I do not bother with stops now. It is more than obvious that this can *** be trivially solved in many steps, but let's not waste *** time with that now. *** ******************************** *** Timed behavior of sender *** ******************************** eq mte(< Q : RSsenderAlone | SPMTimer : TI', sendDataTimer : TI'' >) = min(TI', TI'') . eq delta(< Q : RSsenderAlone | clock : R', SPMTimer : TI' , sendDataTimer : TI'' >, R) = < Q : RSsenderAlone | clock : R' plus R, SPMTimer : TI' monus R, sendDataTimer : TI'' monus R > . *** ******************************** *** RECEIVER *** ******************************** *** Receiver protocol. We assume the topology. Essentially, each *** data packet receive is stored in a buffer, or has been given to *** the "end application". *** To get rid of messages, I assume that the "receiver application" works *** in "asynchronous receive mode", and relay the messages to the *** application "in order". If multiple packets can be relayed to the *** application at the same time, the receiver object first *** "concatenates" these packets together, so that the receiver *** will receive these packets (as one large packet) in order. *** The message buffer then contains the received messages with seqNo *** greater than or equal to readNextSeq. *** For all sequence numbers, we also need to store the sequence number, *** the corresponding suppression and retransmission timers, and the NAK- *** count. class RSreceiver | fastRepairFlag : Bool, readNextSeq : NzNat, *** the NEXT expected seqNo to application. smoothedRTT : Int, *** smoothed RTT estimate to source rttVariance : Int, suppressTO : Time, *** time before sending NAK packet retransTO : Time, *** time before resending NAK packet dataBuffer : MsgConfiguration, *** buffers dataPackets dataInfo : DataInfo, *** store info about repairs SPMread : Bool . *** SPM message read? subclass RSreceiver < Receiver . subclass RSreceiver < SharedRSNCA . *** attribute "isNominee : Bool" class RSreceiverAlone . subclass RSreceiverAlone < RSreceiver . *** For each sequence number, we need to store suppression and *** retransmission timer and NAK count: sort DataInfo . op info : NzNat TimeInf TimeInf Nat -> DataInfo . *** info(seqNo, suppressionTimer, retransmissionTimer, NAKcount) op none : -> DataInfo . op __ : DataInfo DataInfo -> DataInfo [assoc comm id: (none).DataInfo] . *** Use case B2. For each sequence number in the interval between *** the received SPM-number and the latest data packet receiver or NAK count *** greater than 1, we need to do a lot of things. Therefore, some functions *** return the highest seqNo in the dataBuffer and the highest seqNo *** with NAKcount > 0. rl [firstSPM] : (SPMPacket(N) from Q to Q') < Q' : RSreceiverAlone | SPMread : false > => (SPMPacket(N) from Q to Q') < Q' : RSreceiverAlone | SPMread : true, repairserver : Q > . rl [B2a] : (SPMPacket(0) from Q to Q') < Q' : RSreceiver | SPMread : true > => < Q' : RSreceiver | repairserver : Q > . rl [B2b] : (SPMPacket(NZN) from Q to Q') < Q'' : RandomNGen | seed : N > < Q' : RSreceiver | SPMread : true, fastRepairFlag : X, readNextSeq : NZN', suppressTO : R, dataBuffer : MC, dataInfo : DI > => < Q'' : RandomNGen | seed : if X then N else repeatRandom(N, NZN - max(NZN' - 1, highestSeqNo(MC), highestNzNAKSeqNo(DI))) fi > < Q' : RSreceiver | repairserver : Q, dataInfo : updateDI(DI, X, max(NZN', highestSeqNo(MC) + 1, highestNzNAKSeqNo(DI) + 1), NZN, R, N) > . *** updateDI updates the info about repairs for the packets *** found missing, by creating a new packet (or changing the NAK count to 1) *** with suppression timer 0 if in fast repair mode and with the appropriate *** suppression-time value otherwise. op updateDI : DataInfo Bool Nat Nat Time Nat -> DataInfo . *** Usage: updateDI(dataInfo, fastRepairFlag, lowSeqNo, highSeqNo, *** suppressTO, randomSeed) eq updateDI(DI, X, N, N', R, N'') = if N' < N then DI else (info(N, suppr(X, R, N''), INF, 1) updateDI(removeSeqNo(DI, N), X, N + 1, N', R, if X then N'' else random(N'') fi)) fi . op removeSeqNo : DataInfo NzNat -> DataInfo . *** Removes the info with the given sequence number: eq removeSeqNo((info(NZN, TI, TI', N) DI), NZN) = DI . ceq removeSeqNo(DI, NZN) = DI if not NZN in DI . *** Finds new suppression timer value: op suppr : Bool Time Nat -> Time . *** Usage: suppr(fastRepairFlag, suppressTO, randomSeed) eq suppr(true, R, N) = 0 . eq suppr(false, R, N) = random(N) rem (((R * 3) quo 2) + 1) . *** Highest seqNo in data info with NAK count > 0: op highestNzNAKSeqNo : DataInfo -> Nat . eq highestNzNAKSeqNo(none) = 0 . ceq highestNzNAKSeqNo(DI DI') = max(highestNzNAKSeqNo(DI), highestNzNAKSeqNo(DI')) if DI =/= none and DI' =/= none . eq highestNzNAKSeqNo(info(NZN, TI, TI', N)) = if N == 0 then 0 else NZN fi . *** highestSeqNo gives the highest seq no of datapackets in the buffer op highestSeqNo : MsgConfiguration -> Nat . eq highestSeqNo(none) = 0 . eq highestSeqNo(NEMC NEMC') = max(highestSeqNo(NEMC), highestSeqNo(NEMC')) . eq highestSeqNo(dataPacket(Q, NZN, R, X, Y, Z)) = NZN . op _in_ : NzNat DataInfo -> Bool . eq NZN in (none).DataInfo = false . ceq NZN in (DI DI') = (NZN in DI) or (NZN in DI') if DI =/= none and DI' =/= none . eq NZN in info(NZN', TI, TI', N) = (NZN == NZN') . crl [B3a] : (dataPacket(Q, NZN, R, X', Y, Z) from Q' to Q'') < Q'' : RSreceiver | readNextSeq : NZN', dataBuffer : MC, dataInfo : DI > => < Q'' : RSreceiver | dataInfo : cancelTimers(DI, NZN) > if NZN < NZN' or NZN seqNoIn MC . op cancelTimers : DataInfo NzNat -> DataInfo . eq cancelTimers(none, NZN) = none . eq cancelTimers((info(NZN, TI, TI', N) DI), NZN) = (info(NZN, INF, INF, N) DI) . ceq cancelTimers(DI, NZN) = DI if not (NZN in DI) . op _seqNoIn_ : NzNat MsgConfiguration -> Bool . eq NZN seqNoIn none = false . eq NZN seqNoIn (NEMC NEMC') = (NZN seqNoIn NEMC) or (NZN seqNoIn NEMC') . eq NZN seqNoIn dataPacket(Q, NZN', R, X, Y, Z) = (NZN == NZN') . *** Now, the rest is more or less as when receiving a SPM packet, with some *** exceptions: The wholes and stuff must be counted from packetNo-1, *** and possibly some packets must be delivered to the "Application" *** and some timers must be turned off. When delivering packets to *** the application, we also remove corresponding data *** from the data buffer and the info-thing. *** Since we are assuming "asynchronous receiver mode", the next value *** of readNextSeq should also be the "least outstanding message number". *** The following defines the output packets to the application. To make *** it easier for the application to reassemble the packets, it *** gets the message in the form of a sequence of data packets in the right *** order. msg toApplication : Oid Msg -> Msg . *** message sent to an application from the receiver Oid. *** In order to use a sort MsgList, we'd to extend Configuration, there- *** fore, just the sort Msg: op _cat_ : MsgConfiguration MsgConfiguration -> MsgConfiguration [assoc id: none] . op _cat_ : Msg Msg -> Msg [assoc id: none] . *** The following function defines which packets to send the application: op toApp : MsgConfiguration NzNat Oid -> MsgConfiguration . *** which calls the following workhorse: op toApp : MsgConfiguration NzNat -> MsgConfiguration . *** toApp(dataPackets, readNextSeq) eq toApp(MC, NZN, Q) = if toApp(MC, NZN) =/= none then toApplication(Q, toApp(MC, NZN)) else none fi . ceq toApp(MC, NZN) = (none).EmptyConfiguration if not (NZN seqNoIn MC) . eq toApp((dataPacket(Q, NZN, R, X, Y, Z) MC), NZN) = (dataPacket(Q, NZN, R, X, Y, Z) cat toApp(MC, NZN + 1)) . *** The following function removes the dataPackets sent to the application. op rmDelivered : MsgConfiguration Nat -> MsgConfiguration . op lastSeqNo : MsgConfiguration -> Nat . eq lastSeqNo(none) = 0 . eq lastSeqNo(dataPacket(Q, NZN, R, X, Y, Z)) = NZN . eq lastSeqNo(MC cat dataPacket(Q, NZN, R, X, Y, Z)) = NZN . eq rmDelivered(MC, N) = rmUpTo(MC, lastSeqNo(toApp(MC, N))) . op rmUpTo : MsgConfiguration Nat -> MsgConfiguration . *** Removes all dataPackets up to the one with seqNo = 2nd argument eq rmUpTo(none, N) = none . eq rmUpTo(MC, 0) = MC . eq rmUpTo(NEMC NEMC', NZN) = rmUpTo(NEMC, NZN) rmUpTo(NEMC', NZN) . eq rmUpTo(dataPacket(Q, NZN, R, X, Y, Z), NZN') = if NZN <= NZN' then none else dataPacket(Q, NZN, R, X, Y, Z) fi . *** Removes from dataInfo all the guys with seqNo <= 2nd argument: op remove : DataInfo Nat -> DataInfo . eq remove(none, N) = none . ceq remove(DI DI', N) = remove(DI, N) remove(DI', N) if DI =/= none and DI' =/= none . eq remove(info(NZN, TI, TI', N), N') = if NZN <= N' then none else info(NZN, TI, TI', N) fi . crl [B3b] : (dataPacket(Q''', NZN, R, X, Y, Z) from Q to Q') < Q'' : RandomNGen | seed : N > < Q' : RSreceiverAlone | fastRepairFlag : X', readNextSeq : NZN', suppressTO : R', dataBuffer : MC, dataInfo : DI > => < Q'' : RandomNGen | seed : (if X' then N else repeatRandom(N, (NZN - 1) monus max(NZN' - 1, highestNzNAKSeqNo(DI), highestSeqNo(MC))) fi) > < Q' : RSreceiverAlone | readNextSeq : max(NZN', lastSeqNo(toApp( (dataPacket(Q''', NZN, R, X, Y, Z) MC), NZN')) + 1), dataBuffer : rmDelivered(MC dataPacket(Q''', NZN, R, X, Y, Z), NZN'), dataInfo : remove(updateDI( cancelTimers(DI, NZN), X', max(NZN', highestSeqNo(MC) + 1, highestNzNAKSeqNo(DI) + 1), NZN - 1, R', N), lastSeqNo(toApp(MC dataPacket(Q''', NZN, R, X, Y, Z), NZN'))) > toApp((dataPacket(Q''', NZN, R, X, Y, Z) MC), NZN', Q') if NZN' <= NZN and not (NZN seqNoIn MC) . *** Use case B5. rl [B5] : < Q : RSreceiver | readNextSeq : NZN, fastRepairFlag : X, dataBuffer : MC, repairserver : Q', dataInfo : (info(NZN', 0, TI, N) DI), retransTO : R > => if (NZN' seqNoIn MC) or (NZN' < NZN) then < Q : RSreceiver | dataInfo : (info(NZN', INF, TI, N) DI) > else (if 48 < N then ERROR("Use case B5, too high NAK count for RSreceiver", (dataInfo : (info(NZN', 0, TI, N) DI))) else < Q : RSreceiver | dataInfo : (info(NZN', INF, R, N) DI) > send(NAKPacket(NZN', N, X), Q, Q') fi) fi . *** Use case B6. rl [B6] : < Q : RandomNGen | seed : N > < Q' : RSreceiver | readNextSeq : NZN, suppressTO : R, fastRepairFlag : X, dataBuffer : MC, dataInfo : (info(NZN', TI, 0, N') DI) > => if (NZN' < NZN) or (NZN' seqNoIn MC) then < Q : RandomNGen | > < Q' : RSreceiver | dataInfo : (info(NZN', TI, INF, N') DI) > else < Q : RandomNGen | seed : (if X then N else random(N) fi) > < Q' : RSreceiver | dataInfo : (info(NZN', suppr(X, R, N), INF, N' + 1) DI) > fi . *** Use case B7. *** First case, we already have datainfo about the seqNo the *** NAK concerns: rl [B7a] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSreceiver | readNextSeq : NZN', retransTO : R, dataBuffer : MC, dataInfo : (info(NZN, TI, TI', N') DI) > => if (NZN seqNoIn MC) or (N < N') or (NZN < NZN') then < Q' : RSreceiver | > else < Q' : RSreceiver | dataInfo : (info(NZN, TI, R, N) DI) > fi . crl [B7b] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSreceiver | readNextSeq : NZN', retransTO : R, dataInfo : DI > => < Q' : RSreceiver | dataInfo : (if NZN' <= NZN then (info(NZN, INF, R, N) DI) else DI fi) > if not (NZN in DI) . rl [B10B11] : (NAMPacket(X) from Q' to Q) < Q : RSreceiver | > => < Q : RSreceiver | isNominee : X, fastRepairFlag : X > . *** Use case B12: As mentioned earlier, we don't treat stops here! *** Use case B13: When new RTT values are found in the RTT part, that part *** calls a method newRTT(senderRTT, groupRTT, object). *** Note that use case was changed to also take possible INFs *** into account. rl [B13a] : newRTT(R, TI, Q) < Q : RSreceiver | smoothedRTT : I, rttVariance : I', suppressTO : R' > => if I == 0 then < Q : RSreceiver | smoothedRTT : R, rttVariance : R quo 4, retransTO : R plus R, suppressTO : (if TI =/= INF then TI else R' fi) > else < Q : RSreceiver | smoothedRTT : ((R - I) quo 8) + I, rttVariance : I' + ((abs(R - I) - I') quo 4), retransTO : (((R - I) quo 8) + I) + ((4 * (abs(R - I) - I')) quo 4), suppressTO : (if TI =/= INF then TI else R' fi) > fi . rl [B13b] : newRTT(INF, TI, Q) < Q : RSreceiver | suppressTO : R > => < Q : RSreceiver | suppressTO : (if TI =/= INF then TI else R fi) > . *** Timed behavior of RSreceiver: op mte : DataInfo -> TimeInf . eq mte(< Q : RSreceiverAlone | dataInfo : DI >) = mte(DI) . eq mte((none).DataInfo) = INF . ceq mte(DI DI') = min(mte(DI), mte(DI')) if DI =/= none and DI' =/= none . eq mte(info(NZN, TI, TI', N)) = min(TI, TI') . op delta : DataInfo Time -> DataInfo . eq delta(< Q : RSreceiverAlone | dataInfo : DI >, R) = < Q : RSreceiverAlone | dataInfo : delta(DI, R) > . eq delta((none).DataInfo, R) = (none).DataInfo . ceq delta(DI DI', R) = delta(DI, R) delta(DI', R) if DI =/= none and DI' =/= none . eq delta(info(NZN, TI, TI', N), R) = info(NZN, TI monus R, TI' monus R, N) . *** ************************************* *** Repairserver *** ************************************* class RSrepairserver | SPMread : Bool, *** SPM packet read? maxSeqRcvd : Nat, *** max data packet seq no received smoothedRTT : Int, *** smoothed RTT to source value, init 0 rttVariance : Int, *** init 3000 retransTO : Time, *** time between errorhandlings, init 6000 suppressTO : Time, *** suppress repair request, init 100 SPMWaitTimer : TimeInf, *** system dead if > 60s between SPM NAKStates : NAKstates, *** info about repairs dataBuffer : BoundedBuffer . *** data packet cache subclass RSrepairserver < Repairserver . class RSrepairserverAlone . subclass RSrepairserverAlone < RSrepairserver . *** For each seq no in the cache (?), the repair server needs to store *** various NAK data about the seq no: sort NAKstates . op none : -> NAKstates . op __ : NAKstates NAKstates -> NAKstates [assoc comm id: (none).NAKstates] . op nakState : NzNat Nat Nat Bool TimeInf TimeInf -> NAKstates . *** nakState(seqNo, NAKcount, downStreamNAKcount, NAKpending, NAKsuppTimer, *** NAKretransTimer) *** The cache of a repair server is limited. We store the packets in *** the "cache" as a "bounded buffer": sort BoundedBuffer . op bBuf : MsgList Nat NzNat -> BoundedBuffer [ctor] . *** Usage: bBuf(Buffer, Size, bound) op add : BoundedBuffer Msg -> BoundedBuffer . op _seqNoIn_ : NzNat BoundedBuffer -> Bool . op _seqNoIn_ : NzNat MsgList -> Bool . eq add(bBuf(M + ML, NZN, NZN), M') = bBuf(ML + M', NZN, NZN) . ceq add(bBuf(ML, N, NZN), M) = bBuf(ML + M, N + 1, NZN) if N < NZN . eq NZN seqNoIn bBuf(ML, N, NZN') = NZN seqNoIn ML . eq NZN seqNoIn (nil).MsgList = false . eq NZN seqNoIn dataPacket(Q, NZN', R, X, Y, Z) + ML = NZN == NZN' or NZN seqNoIn ML . *** Use case C1. *** Instead of repeating all the SPM-receiving operations both *** when reading the initial state, and when reading in an ordinary state, *** in the initialization phase, I just notice that the message is read, *** and don't destroy the message! I assume that this is not dangerous, *** in the sense that nothing can come between first observing the existence *** of the first SPM message, and then treat it in another rule. rl [C1init] : (SPMPacket(N) from Q to Q') < Q' : RSrepairserverAlone | SPMread : false > => (SPMPacket(N) from Q to Q') < Q' : RSrepairserverAlone | SPMread : true > . *** Use case C2. This is one interpretation of the text. rl [C2] : < Q : RSrepairserver | SPMWaitTimer : 0 > => ERROR("Use case C2, expired SPMWaitTimer at RSrepairserver") . *** Use case C3: rl [C3] : (SPMPacket(N) from Q to Q') < Q'' : RandomNGen | seed : N' > < Q' : RSrepairserver | SPMread : true, children : OS, maxSeqRcvd : N'', suppressTO : R, NAKStates : NS > => < Q'' : RandomNGen | seed : repeatRandom(N', noOfNewNAKs(NS, N'', N)) > < Q' : RSrepairserver | repairserver : Q, SPMWaitTimer : 60000, NAKStates : updateNAKstates(NS, N'', N, N', R) > multiSend(SPMPacket(N), Q', OS) newNAKPackets(NS, N'', N, Q', OS) . op noOfNewNAKs : NAKstates Nat Nat -> Nat . *** noOfNewNAKs(NAKstates, maxSeqRcvd, seq-1) eq noOfNewNAKs(NS, 0, N) = 0 . eq noOfNewNAKs(NS, NZN, N) = if N <= NZN then 0 else (if (NZN in NS) then 0 else 1 fi) + noOfNewNAKs(NS, NZN + 1, N) fi . op _in_ : NzNat NAKstates -> Bool . eq NZN in (none).NAKstates = false . ceq NZN in (NS NS') = (NZN in NS) or (NZN in NS') if NS =/= none and NS' =/= none . eq NZN in nakState(NZN', N, N', X, TI, TI') = (NZN == NZN') . op updateNAKstates : NAKstates Nat Nat Nat Time -> NAKstates . *** updateNAKstates(NAKstate, maxSeqRcvd, seq-1, seed, suppressTO) eq updateNAKstates(NS, 0, N, N', R) = NS . eq updateNAKstates(NS, NZN, N, N', R) = if N <= NZN then NS else updateNAKstates(if (NZN in NS) then NS else (nakState(NZN, 1, 1, true, random(N') rem (((R * 3) quo 2) + 1), INF) NS) fi, NZN + 1, N, random(N'), R) fi . op newNAKPackets : NAKstates Nat Nat Oid OidSet -> Configuration . *** newNAKPackets(NAKstate, maxSeqRcvd, seq-1, sender, receivers) eq newNAKPackets(NS, 0, N, Q, OS) = none . eq newNAKPackets(NS, NZN, N, Q, OS) = if N <= NZN then (none).EmptyConfiguration else (newNAKPackets(NS, NZN + 1, N, Q, OS) (if (NZN in NS) then none else multiSend(NAKPacket(NZN, 1, false), Q, OS) fi)) fi . *** Use case C4. The "retransmission flag" in the data packet indicates *** whether the data packet is an original packet, or resent. crl [C4a] : (dataPacket(Q, NZN, R, X, Y, Z) from Q' to Q'') < Q'' : RSrepairserver | dataBuffer : BB > => < Q'' : RSrepairserver | > if NZN seqNoIn BB . crl [C4b] : (dataPacket(Q, NZN, R, X, Y, Z) from Q' to Q'') < Q''' : RandomNGen | seed : N > < Q'' : RSrepairserver | children : OS, maxSeqRcvd : N', dataBuffer : BB, NAKStates : NS, suppressTO : R' > => < Q'' : RSrepairserver | maxSeqRcvd : max(NZN, N'), dataBuffer : add(BB, dataPacket(Q, NZN, R, X, Y, Z)), NAKStates : (if (N' == 0) then cancelTimersAndSetFalse(NZN, NS) else updateNAKstates( cancelTimersAndSetFalse(NZN, NS), N', NZN - 1, N, R) fi) > < Q''' : RandomNGen | seed : repeatRandom(N, noOfNewNAKs(NS, N', NZN - 1)) > (if ((not Z) or NAKpending(NS, NZN)) then multiSend(dataPacket(Q, NZN, R, X, Y, Z), Q'', OS) else none fi) newNAKPackets(NS, N', NZN - 1, Q'', OS) if not (NZN seqNoIn BB) . op NAKpending : NAKstates NzNat -> Bool . *** Checks both if NAK state exists and then whether the NAK is pending: ceq NAKpending(NS, NZN) = false if not(NZN in NS) . eq NAKpending(nakState(NZN, N, N', X, TI, TI') NS, NZN) = X . op cancelTimersAndSetFalse : NzNat NAKstates -> NAKstates . *** Cancels the timers and sets NAK pending to false. eq cancelTimersAndSetFalse(NZN, nakState(NZN, N, N', X, TI, TI') NS) = nakState(NZN, N, N', false, INF, INF) NS . ceq cancelTimersAndSetFalse(NZN, NS) = NS if not NZN in NS . *** Use case C7. We have to make sure that in this use case we treat *** only downstreams messages: *** Packet in cache; don't worry about repairs: crl [C7a] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSrepairserver | repairserver : Q, dataBuffer : BB > => < Q' : RSrepairserver | > if NZN seqNoIn BB . *** Packet not in cache; update and forward if higher NAK count received: crl [C7b] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSrepairserver | repairserver : Q, dataBuffer : BB, retransTO : R, NAKStates : (nakState(NZN, N', N'', Y, TI, TI') NS), children : OS > => < Q' : RSrepairserver | NAKStates : (nakState(NZN, max(N, N'), if N' < N then N else N'' fi, Y, INF, R) NS) > (if N' < N then multiSend(NAKPacket(NZN, N, false), Q', OS) else none fi) if not (NZN seqNoIn BB) . *** Packet not in cache, and no NAK state: crl [C7c] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSrepairserver | repairserver : Q, dataBuffer : BB, retransTO : R, children : OS, NAKStates : NS > => < Q' : RSrepairserver | NAKStates : (nakState(NZN, N, N, true, INF, R) NS) > multiSend(NAKPacket(NZN, N, false), Q', OS) if not (NZN seqNoIn BB or NZN in NS) . *** Use case C8. Have to make sure that we treat *** only upstreams (unicast) messages: *** NAK does not exists, fastRepFlag is true, data not buffered: crl [C8a] : (NAKPacket(NZN, N, true) from Q to Q') < Q' : RSrepairserver | repairserver : Q'', children : Q OS, retransTO : R, dataBuffer : BB, NAKStates : NS > => < Q' : RSrepairserver | NAKStates : (nakState(NZN, N, N, true, INF, R) NS) > multiSend(NAKPacket(NZN, N, false), Q', Q OS) send(NAKPacket(NZN, N, true), Q', Q'') if not (NZN seqNoIn BB or NZN in NS) . *** no NAK exists, data not buffered, fastRepFlag false: crl [C8b] : (NAKPacket(NZN, N, false) from Q to Q') < Q'' : RandomNGen | seed : N' > < Q' : RSrepairserver | children : Q OS, suppressTO : R, dataBuffer : BB, NAKStates : NS > => < Q'' : RandomNGen | seed : random(N') > < Q' : RSrepairserver | NAKStates : (nakState(NZN, N, N, true, random(N') rem (((3 * R) quo 2) + 1), INF) NS) > multiSend(NAKPacket(NZN, N, false), Q', Q OS) if not (NZN seqNoIn BB or NZN in NS) . *** data not in buffer, NAK state exists: crl [C8c] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSrepairserver | repairserver : Q'', children : Q OS, NAKStates : (nakState(NZN, N', N'', Y, TI, TI') NS), retransTO : R, dataBuffer : BB > => (if (N' < N) then < Q' : RSrepairserver | NAKStates : (nakState(NZN, N, N, true, if X then INF else TI fi, if X then R else TI' fi) NS) > multiSend(NAKPacket(NZN, N, false), Q', Q OS) (if X then send(NAKPacket(NZN, N, true), Q', Q'') else none fi) else (if (N'' < N) then < Q' : RSrepairserver | NAKStates : (nakState(NZN, N', N, Y, TI, TI') NS) > multiSend(NAKPacket(NZN, N, false), Q', Q OS) else < Q' : RSrepairserver | > fi) fi) if not (NZN seqNoIn BB) . *** Next, the message is in the buffer, but the NAK state does not exist. crl [C8d] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSrepairserver | children : Q OS, dataBuffer : bBuf(ML + dataPacket(Q'', NZN, R, Y, Z, XX) + ML', N', NZN'), NAKStates : NS > => < Q' : RSrepairserver | NAKStates : (nakState(NZN, N, N, false, INF, INF) NS) > multiSend(dataPacket(Q'', NZN, R, Y, Z, true), Q', Q OS) if not (NZN in NS) . *** The sequence number exists in both data buffer and NAK state: rl [C8e] : (NAKPacket(NZN, N, X) from Q to Q') < Q' : RSrepairserver | children : Q OS, dataBuffer : bBuf(ML + dataPacket(Q'', NZN, R, Y, Z, XX) + ML', N''', NZN'), NAKStates : (nakState(NZN, N', N'', X', TI, TI') NS) > => if N' < N then < Q' : RSrepairserver | NAKStates : (nakState(NZN, N, N, false, TI, TI') NS) > multiSend(dataPacket(Q'', NZN, R, Y, Z, true), Q', Q OS) else < Q' : RSrepairserver | > fi . *** Use case C11. *** It is invariant that no NAKseqNo has more than one timer active! rl [C11] : < Q : RSrepairserver | dataBuffer : BB, NAKStates : (nakState(NZN, N, N', X, 0, TI) NS), retransTO : R, repairserver : Q' > => if (X and not (NZN seqNoIn BB)) then < Q : RSrepairserver | NAKStates : (nakState(NZN, N, N', X, INF, R) NS) > send(NAKPacket(NZN, N, false), Q, Q') else < Q : RSrepairserver | NAKStates : (nakState(NZN, N, N', X, INF, TI) NS) > fi . rl [C12] : < Q : RandomNGen | seed : N > < Q' : RSrepairserver | suppressTO : R, dataBuffer : BB, children : OS, NAKStates : (nakState(NZN, N', N'', X, TI, 0) NS) > => if (X and not (NZN seqNoIn BB)) then < Q : RandomNGen | seed : random(N) > < Q' : RSrepairserver | NAKStates : (nakState(NZN, N' + 1, N'', X, random(N) rem (((R * 3) quo 2) + 1), INF) NS) > multiSend(NAKPacket(NZN, N' + 1, false), Q', OS) else < Q : RandomNGen | > < Q' : RSrepairserver | NAKStates : (nakState(NZN, N', N'', X, TI, INF) NS) > fi . *** Use case C13: This should be combined with something in the RTT *** protocol. In the absence of that, we assume that there is a message *** newRTT where the first argument is senderRTT and the second is groupRTT. *** Note: Use case updated by Mark to accomodate INF arguments. rl [C13a] : newRTT(R, TI, Q) < Q : RSrepairserver | smoothedRTT : I, rttVariance : I', suppressTO : R' > => if I == 0 then < Q : RSrepairserver | smoothedRTT : R, rttVariance : R quo 4, retransTO : R plus R, suppressTO : (if TI =/= INF then TI else R' fi) > else < Q : RSrepairserver | smoothedRTT : ((R - I) quo 8) + I, rttVariance : I' + ((abs(R - I) - I') quo 4), retransTO : ((R - I quo 8) + I) + ((4 * (abs(R - I) - I')) quo 4), suppressTO : (if TI =/= INF then TI else R' fi) > fi . rl [C13b] : newRTT(INF, TI, Q) < Q : RSrepairserver | suppressTO : R > => < Q : RSrepairserver | suppressTO : (if TI == INF then R else TI fi) > . *** Timed behavior of repairserver: op mte : NAKstates -> TimeInf . eq mte(< Q : RSrepairserverAlone | SPMWaitTimer : TI, NAKStates : NS >) = min(TI, mte(NS)) . eq mte((none).NAKstates) = INF . ceq mte(NS NS') = min(mte(NS), mte(NS')) if NS =/= none and NS' =/= none . eq mte(nakState(NZN, N, N', X, TI, TI')) = min(TI, TI') . op delta : NAKstates Time -> NAKstates . eq delta(< Q : RSrepairserverAlone | SPMWaitTimer : TI, NAKStates : NS >, R) = < Q : RSrepairserverAlone | SPMWaitTimer : TI monus R, NAKStates : delta(NS, R) > . eq delta((none).NAKstates, R) = (none).NAKstates . ceq delta(NS NS', R) = delta(NS, R) delta(NS', R) if NS =/= none and NS' =/= none . eq delta(nakState(NZN, N, N', X, TI, TI'), R) = nakState(NZN, N, N', X, TI monus R, TI' monus R) . endtom)