*** Real-Time Maude 2.1 specification of the NOM component of *** the AER/NCA protocol suite *** By Peter Csaba Olveczky *** File defining the NOM part of the protocol. To execute this part, *** the file nomX.rtmaude must be read. *** Uses SPMPacket's to initialize csm timers and the repairserver attributes! *** To run the protocol separately, *** the only "external" data this protocol needs is the value of the *** sourceRTT attribute for the receivers. We could have gotten this *** in messages, (thereby having the opportunity to change it *** in-between), but I think that it is enough *** to "pre-compute" the source RTT, and have it as an attribute. *** Actually, precomputing the RTT value failed to show what happens *** in the initial stages when sourceRTT is noTimeValue for *** the receivers. That is now taken into account in the specification, *** but is probably worth trying out. *** For more sophisticated prototyping, the sourceRTT attribute *** could be changed by messages. (tomod NCA-NOM is including TIMED-RANDOM . including LINK . including WINDOW . including COMMON-CLASSES . including TICK-RULE . including SHARED-ATTS . including SHARED-MSGS . including ENVIRONMENT . vars RAT RAT' : Rat . vars DR DR' DR'' DR''' : DefRat . vars R R' R'' R''' R'''' R''''' : Time . vars Q Q' Q'' Q''' Q'''' : Qid . vars DQ DQ' DQ'' : DefOid . var W : Window . var N : Nat . var NZN : NzNat . vars X Y Z : Bool . vars TI TI' TI'' : TimeInf . var OS : OidSet . msg csmPacket : DefRat TimeInf DefOid -> Packet . *** usage: csmPacket(lpe, RTT, addrLeafNode) *** The sort of the last field was changed to DefOid at Mark's request, *** even though it seems obvious that it can never be noOid! msg startNOM : Oid -> Msg . *** Starts the protocol in the Alone case, that is, it makes the sender *** send one SPMPacket to each receivable, so that csm Timers and *** repairserver attributes are initialized. Usage: startNOM(sender) *** The following message was defined in our December meeting: msg dataPacket : NzNat Time -> LargePacket . *** usage: dataPacket(seqNo, timeStamp). *** Note that the messages *** seem to come from outside the protocol ... *** In our case, we assume they come through channels though. class NOMsender | NAMTimer : TimeInf, *** initially INF csmLPE : DefRat, *** initially noRat csmRTT : TimeInf, *** initially 0. csmSetTime : Time . *** initially current time (=0?) subclass NOMsender < Sender Clock . subclass NOMsender < NCANOM-NCARCsender . *** Attribute "csmNominee : DefOid" class NOMsenderAlone . subclass NOMsenderAlone < NOMsender . *** Initialization: rl [initNOM] : startNOM(Q) < Q : NOMsenderAlone | children : OS > => < Q : NOMsenderAlone | > multiSend(SPMPacket(0), Q, OS) . *** Use cases D2 and D3. *** We isolate the long boolean test, which also occurs in use case F2: op updateNomValues : DefRat TimeInf DefOid DefOid DefRat TimeInf Time Time -> Bool . *** usage: updateNomValues(lpe, RTT, addr, csmNominee/csmAddress, csmLPE, *** csmRTT, currentTime, csmSetTime) . *** Since we can't compute with the noRat value, we need to single out *** the special cases where lpe or csmLPE is noRat: ceq updateNomValues(DR, TI, DQ, DQ', DR', TI', R, R') = (DQ' == noOid) or *** no current nominee: update! (DQ == DQ') or *** update current nominees values! (DR == noRat and DR' == noRat *** no lpe values, so ... and TI =/= INF and TI' =/= INF *** ... choose longest RTT as nominee and TI gt TI') or (R' + 17000 < R) *** too long time since last update if DR == noRat or DR' == noRat . eq updateNomValues(RAT, TI, DQ, DQ', RAT', TI', R, R') = (DQ' == noOid) or *** no current nominee: update! (DQ == DQ') or *** update current nominees values! (R' + 17000 < R) or *** too long time since last update (RAT >= 0 and RAT <= 1 and *** new lpe values sensible RAT' >= 0 and RAT' <= 1 and *** old lpe values sensible gSquare(RAT, TI) > gSquare(RAT', TI')) . *** new worst revcr *** The function g is not easy to compute since we only have natural *** numbers, but since we only are going to compare two g-values, *** we can as well compare compare their squares. op gSquare : Rat TimeInf -> Rat . eq gSquare(RAT, R) = RAT * R * R . eq gSquare(RAT, INF) = 0 . *** Use cases D2 and D3. *** ASSUMES that the receiver address in the csmPacket cannot be noOid: *** Note that even though DQ' never can be noOid, Mark asked me to still take *** that possibility into consideration, and combine this rule with *** G14. rl [D2D3] : (csmPacket(DR, TI, DQ') from Q to Q') < Q' : NOMsenderAlone | clock : R, csmNominee : DQ, csmLPE : DR', csmRTT : TI', csmSetTime : R', NAMTimer : TI'' > => if updateNomValues(DR, TI, DQ', DQ, DR', TI', R, R') then < Q' : NOMsenderAlone | csmNominee : DQ', csmLPE : DR, csmRTT : TI, csmSetTime : R, NAMTimer : (if DQ =/= DQ' then 7000 else TI'' fi) > (if DQ =/= DQ' and DQ' =/= noOid then (NAMPacket(true) from Q' to DQ') else none fi) (if DQ =/= DQ' and DQ =/= noOid then (NAMPacket(false) from Q' to DQ) else none fi) else < Q' : NOMsenderAlone | > fi . *** Note, that this sending directly to the appropriate receivers is unicast, *** and we agreed on that it should be sent instantaneously to the receiver, *** with no delay, and without passing through channels. *** Use case D4: rl [D4] : < Q : NOMsender | csmNominee : DQ, NAMTimer : 0 > => if DQ =/= noOid then (< Q : NOMsender | NAMTimer : 7000 > (NAMPacket(true) from Q to DQ)) else < Q : NOMsender | NAMTimer : INF > fi . *** ************************************************ *** Repair server *** ************************************************ class NOMrepairserver | csmLPE : DefRat, *** initially noRat csmRTT : TimeInf, *** initially 0. csmAddress : DefOid, *** initially noOid csmSetTime : Time, *** initially "current time" csmTimer : TimeInf . *** initially INF??? subclass NOMrepairserver < Repairserver . *** children attribute not needed! subclass NOMrepairserver < Clock . class NOMrepairserverAlone . subclass NOMrepairserverAlone < NOMrepairserver . *** Initialize csm timer and repairserver attribute. Assumes that *** only one SPM packet is received when operated alone: rl [F1] : (SPMPacket(0) from Q' to Q) < Q : NOMrepairserverAlone | children : OS > => < Q : NOMrepairserverAlone | repairserver : Q', csmTimer : 7000 > multiSend(SPMPacket(0), Q, OS) . *** Use cases F2 and F3: *** Note again that DQ' can never be noOid, but that that case is taken into *** consideration upon request! rl [F2F3] : (csmPacket(DR, TI, DQ') from Q to Q') < Q' : NOMrepairserver | clock : R, repairserver : Q''', csmAddress : DQ, csmLPE : DR', csmRTT : TI', csmSetTime : R' > => if updateNomValues(DR, TI, DQ', DQ, DR', TI', R, R') then (< Q' : NOMrepairserver | csmAddress : DQ', csmLPE : DR, csmRTT : TI, csmSetTime : R, csmTimer : 7000 > (if DQ' =/= noOid then send(csmPacket(DR, TI, DQ'), Q', Q''') else none fi)) else < Q' : NOMrepairserver | > fi . *** Use case F4: rl [F4] : < Q : NOMrepairserver | clock : R, repairserver : Q', csmLPE : DR, csmRTT : TI, csmAddress : DQ, csmSetTime : R', csmTimer : 0 > => if (R' + 17000) < R then < Q : NOMrepairserver | csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : R, csmTimer : 7000 > else (< Q : NOMrepairserver | csmTimer : 7000 > (if DQ =/= noOid then send(csmPacket(DR, TI, DQ), Q, Q') else none fi)) fi . *** ********************************************************* *** Receiver *** ********************************************************* class NOMreceiver | sourceRTT : TimeInf, *** initially INF. msgWindow : Window, *** Window for storing message numbers *** initially initWindow(200), or somewhat less *** for prototyping purposes ........., csmTimer : TimeInf . subclass NOMreceiver < Receiver . subclass NOMreceiver < SharedRSNCA . *** isNominee attribute. class NOMreceiverAlone . subclass NOMreceiverAlone < NOMreceiver . *** Timer should be started with an initial value randomly chosen between *** 0 and 5000: rl [initNOMreceiver] : (SPMPacket(0) from Q' to Q) < Q'' : RandomNGen | seed : N > < Q : NOMreceiverAlone | > => < Q'' : RandomNGen | seed : random(N) > < Q : NOMreceiverAlone | repairserver : Q', csmTimer : random(N) rem 5001 > . *** In any combined system, this use case has to be combined with *** use cases in RS for receiving data packets. rl [E2] : (dataPacket(NZN, R) from Q to Q') < Q' : NOMreceiverAlone | msgWindow : W > => < Q' : NOMreceiverAlone | msgWindow : add(NZN, W) > . *** In use case E3, there is a test *** in the file so that the LPE estimate is not considered important *** when size of the window is less than 150. rl [E3] : < Q : NOMreceiver | csmTimer : 0, msgWindow : W, repairserver : Q', sourceRTT : TI > => < Q : NOMreceiver | csmTimer : 5000 > send(csmPacket(if (size(W) < 2) then noRat else windowLPE(W) fi, TI, Q), Q, Q') . *** IMPORTANT: Only for prototyping purposes have we changed have we changed *** the 150 in the test if (size(W) < 150) to 2!!! This to have a smaller *** example on which to run the thing ... rl [E4] : (NAMPacket(Z) from Q' to Q) < Q : NOMreceiverAlone | > => < Q : NOMreceiverAlone | isNominee : Z > . *** Note that this rule is subsumed by AER-RS rule B10B11 in the combined *** protocol. *** ********** Timed behavior ********************************************* eq delta(< Q : NOMsenderAlone | clock : R', NAMTimer : TI >, R) = < Q : NOMsenderAlone | clock : R' plus R, NAMTimer : TI monus R > . eq delta(< Q : NOMrepairserverAlone | clock : R', csmTimer : TI >, R) = < Q : NOMrepairserverAlone | clock : R' plus R, csmTimer : TI monus R > . eq delta(< Q : NOMreceiverAlone | csmTimer : TI >, R) = < Q : NOMreceiverAlone | csmTimer : TI monus R > . eq mte(< Q : NOMsenderAlone | NAMTimer : TI >) = TI . eq mte(< Q : NOMrepairserverAlone | csmTimer : TI >) = TI . eq mte(< Q : NOMreceiverAlone | csmTimer : TI >) = TI . endtom)