*** Real-Time Maude 2.1 specification of AER/NCA protocol suite *** Specification of the RTT component, by Peter Csaba Olveczky *** Note that this file defines the protocol, but does not read *** any files. If the protocol is executed separately, that job *** is done by the file rttX.rtmaude, which also defines some initial *** states. (tomod AER-RTT is including LINK . *** Both of these include the crucial module including TIMED-RANDOM . *** "TIMED-OO-SYSTEM" including AER-TIME-DOMAIN . *** Also included in LINK including COMMON-CLASSES . including TICK-RULE . including SHARED-MSGS . *** Class hierarchy. All RTT objects are subclasses of RTT: class RTT | sourceRTT : TimeInf . *** This next class is sender and repairserver: class RTTsendable | maxDownRTT : TimeInf, maxDownRTTSetTime : Time, maxRecentDownRTT : Time . subclass RTTsendable < RTT Sendable Clock . *** This next class is repairserver and receiver: class RTTreceivable | resendInterval : Time, maxUpRTT : TimeInf, myUpRTT : TimeInf, getRTTResendTimer : TimeInf . subclass RTTreceivable < RTT Receivable Clock . *** Sender both in stand-alone and combined protocols: class RTTsender . subclass RTTsender < RTTsendable . class RTTreceiver . subclass RTTreceiver < RTTreceivable . class RTTrepairserver . subclass RTTrepairserver < RTTreceivable RTTsendable . *** The objects for stand-alone protocol only: class RTTsenderAlone . subclass RTTsenderAlone < RTTsender . class RTTreceivableAlone . subclass RTTreceivableAlone < RTTreceivable . class RTTreceiverAlone . subclass RTTreceiverAlone < RTTreceiver RTTreceivableAlone . class RTTrepairserverAlone . subclass RTTrepairserverAlone < RTTrepairserver RTTreceivableAlone . var M : Msg . vars R R' R'' R''' R'''' R''''' : Time . vars TI TI' TI'' TI''' : TimeInf . vars Q Q' Q'' : Oid . var N : Nat . var DQ : DefOid . var OS : OidSet . msg getRTTRequest : Time TimeInf -> Packet . *** usage: getRTTRequest(xmitTime, upRTT). msg getRTTResponse : Time TimeInf TimeInf -> Packet . *** Usage: getRTTResponse(xmitTime, peerGroupRTT, globalRTT) *** Initialization of the attributes is not done *** explicitly, but by giving an appropriate initial state with *** the following values: *** clock: 0 *** started: false *** sourceRTT: 0 if sender else INF, *** maxDownRTT=maxUpRTT=myUpRTT: INF, *** maxDownRTTSetTime: "current time" *** maxRecentDownRTT: 0, *** resendInterval: 200 *** getRTTResendTimer: INF. *** Furthermore, we require from the initial state that the *** children attributes together with the links *** should be consistent with the topology. *** Note also that the initial state has sort System. *** Initialization. The various initial values of the attributes *** should be given in the initial states to rewrite. In use case R2, *** the system is started by a startRTT message to the sender, which *** then sends only one SPM packet downstreams, so that all downstream *** objects can update their repairserver attributes and start *** their getRTTResendTimers msg startRTT : Oid -> Msg . rl [startRTT] : startRTT(Q) < Q : RTTsenderAlone | children : OS > => < Q : RTTsenderAlone | > multiSend(SPMPacket(0), Q, OS) . *** Note that we assume for the stand-alone protocol that only one SPM *** packet will be received by each object. rl [R2rs] : (SPMPacket(0) from Q' to Q) < Q'' : RandomNGen | seed : N > < Q : RTTrepairserverAlone | children : OS > => < Q'' : RandomNGen | seed : random(N) > < Q : RTTrepairserverAlone | repairserver : Q', getRTTResendTimer : random(N) rem 31 > multiSend(SPMPacket(0), Q, OS) . rl [R2rcv] : (SPMPacket(0) from Q' to Q) < Q'' : RandomNGen | seed : N > < Q : RTTreceiverAlone | > => < Q'' : RandomNGen | seed : random(N) > < Q : RTTreceiverAlone | repairserver : Q', getRTTResendTimer : random(N) rem 31 > . *** Use case R.3. rl [R3] : < Q : RTTreceivable | clock : R, repairserver : Q', resendInterval : R', myUpRTT : TI, getRTTResendTimer : 0 > => < Q : RTTreceivable | getRTTResendTimer : R' > send(getRTTRequest(R, TI), Q, Q') . *** Use case R.4. *** It may look somewhat simpler to split it up in several cases ... *** First of all, it must be noted that the received upRTT-value may be *** INF. The informal spec does not mention this case *** explicitly. I therefore assume that we should only do the *** "latter" part in that case, that is, send the respons and perform *** the last actions. *** First case. upRTT and maxDownRTT are both time values, *** and upRTT > maxDownRTT. Note, in this case, the "second part" of *** the use case will not apply. crl [R4a] : (getRTTRequest(R, R') from Q to Q') < Q' : RTTsendable | clock : R'', sourceRTT : TI, maxDownRTT : R''' > => < Q' : RTTsendable | maxDownRTT : R', maxDownRTTSetTime : R'', maxRecentDownRTT : 0 > send(getRTTResponse(R, R', TI), Q', Q) if R''' lt R' . *** In the next case, upRTT is still a time value, but maxDownRTT is *** now INF. Is it still true that the first case applies?: rl [R4b] : (getRTTRequest(R, R') from Q to Q') < Q' : RTTsendable | clock : R'', sourceRTT : TI, maxDownRTT : INF > => < Q' : RTTsendable | maxDownRTT : R', maxDownRTTSetTime : R'', maxRecentDownRTT : 0 > send(getRTTResponse(R, R', TI), Q', Q) . *** If upRTT is INF, then I GUESS that the second part of the use case *** applies, regardless of whether maxDownRTT is a time value: rl [R4c] : (getRTTRequest(R, INF) from Q to Q') < Q' : RTTsendable | clock : R', sourceRTT : TI, maxDownRTT : TI', maxDownRTTSetTime : R'', maxRecentDownRTT : R''' > => if (R'' + 3500) < R' then < Q' : RTTsendable | maxDownRTT : R''', maxDownRTTSetTime : R', maxRecentDownRTT : 0 > send(getRTTResponse(R, R''', TI), Q', Q) else < Q' : RTTsendable | > send(getRTTResponse(R, TI', TI), Q', Q) fi . *** The final case: Both upRTT and maxDownRTT *** are concrete values, and upRTT <= maxDownRTT: crl [R4d] : (getRTTRequest(R, R') from Q to Q') < Q' : RTTsendable | clock : R'', sourceRTT : TI, maxDownRTT : R''', maxDownRTTSetTime : R'''', maxRecentDownRTT : R''''' > => (if (R'''' + 3500) lt R'' then < Q' : RTTsendable | maxDownRTT : max(R', R'''''), maxDownRTTSetTime : R'', maxRecentDownRTT : 0 > send(getRTTResponse(R, max(R', R'''''), TI), Q', Q) else < Q' : RTTsendable | maxRecentDownRTT : max(R',R''''') > send(getRTTResponse(R, R''', TI), Q', Q) fi) if R' le R''' . *** Use case R.5. *** I split again in two, even though it may strictly speaking not be *** necessary. First case is when either maxUpRTT is INF *** or peerGroupRTT is INF: *** Note that in both cases, the maxUpRTT seems to have been updated, so *** I call the method newRTT if in the combined protocol: crl [R5a] : (getRTTResponse(R, TI, TI') from Q to Q') < Q' : RTTreceivable | clock : R', sourceRTT : TI'', resendInterval : R'', maxUpRTT : TI''' > => < Q' : RTTreceivable | sourceRTT : (if TI' =/= INF then TI' + (R' monus R) else TI'' fi), resendInterval : min(2 * (R' monus R), 3000), maxUpRTT : (if TI =/= INF then max(R' monus R, TI) else (R' monus R) fi), myUpRTT : R' monus R, getRTTResendTimer : R' monus R > send(getRTTRequest(R', R' monus R), Q', Q) (if (< Q' : RTTreceivable | > :: CombinedObject) then newRTT(if TI' =/= INF then TI' + (R' monus R) else TI'' fi, if TI =/= INF then max(R' monus R, TI) else (R' monus R) fi, Q') else none fi) if TI''' == INF or TI == INF . *** Now, neither peerGroupRTT nor maxUpRTT has INF value: rl [R5b] : (getRTTResponse(R, R', TI) from Q to Q') < Q' : RTTreceivable | clock : R'', sourceRTT : TI', resendInterval : R''', maxUpRTT : R'''' > => < Q' : RTTreceivable | sourceRTT : (if TI =/= INF then TI + (R'' monus R) else TI' fi), resendInterval : min(2 * R''', 3000), maxUpRTT : max(R'' monus R, R'), myUpRTT : R'' monus R > (if (< Q' : RTTreceivable | > :: CombinedObject) then newRTT(if TI =/= INF then TI plus (R'' monus R) else TI' fi, max(R'' monus R, R'), Q') else none fi) . *** This should end the use cases. Now, we define the behavior *** in time for the system. eq delta(< Q : RTTsenderAlone | clock : R >, R') = < Q : RTTsenderAlone | clock : R + R' > . eq delta(< Q : RTTreceivableAlone | clock : R, getRTTResendTimer : TI >, R') = < Q : RTTreceivableAlone | clock : R + R', getRTTResendTimer : TI monus R' > . eq mte(< Q : RTTsenderAlone | >) = INF . eq mte(< Q : RTTreceivableAlone | getRTTResendTimer : TI >) = TI . endtom)