*** Real-Time Maude 2.1 specification of the combined AER/NCA *** protocol suite, including test commands. *** By Peter Csaba Olveczky *** Attempt at combining the protocols. Contain the common rules, etc. in AER-prelude.rtmaude in AER-commonclasses.rtmaude in AER-shared-atts.rtmaude in AER-shared-msgs.rtmaude in EfficientWindow.rtmaude in rtt.rtmaude in nom.rtmaude in ncarc.rtmaude in AER-error-object.rtmaude in rs.rtmaude in appLayer.rtmaude (tomod COMBINED-PROTOCOL is including AER-RTT . including NCA-NOM . including NCA-RC . including AER-RS . *** Define the combined classes: subclass SenderCombined < RTTsender NOMsender RCsender RSsender . subclass RepairserverCombined < RTTrepairserver NOMrepairserver . subclass RepairserverCombined < RCrepairserver RSrepairserver . subclass ReceiverCombined < RTTreceiver NOMreceiver RCreceiver RSreceiver . vars N N' MSS WLS MBC BOF : Nat . vars NZN NZN' NZN'' : NzNat . vars Q Q' Q'' Q''' Q'''' : Oid . var OS : OidSet . vars R R' R'' CCMTO : Time . var DB : DataBuffer . vars RTB MC : MsgConfiguration . vars DQ DQ' : DefOid . vars WS : PosRat . vars X Y Z X' FRF : Bool . var TI TI' TI'' TI''' : TimeInf . var DI : DataInfo . var W : Window . var NS : NAKstates . vars DR DR' : DefRat . *** The first part is the initialization part: rl [init] : (SPMPacket(N) from Q to Q') < Q'' : RandomNGen | seed : N' > < Q' : ReceiverCombined | SPMread : false > => (SPMPacket(N) from Q to Q') < Q'' : RandomNGen | seed : repeatRandom(N', 2) > < Q' : ReceiverCombined | SPMread : true, getRTTResendTimer : random(N') rem 31, csmTimer : repeatRandom(N', 2) rem 5001 > . *** The next part is the sending part, namely rules A3send, G11, and G12: rl [A3sendG11G12] : < Q : SenderCombined | children : OS, clock : R, unsentDataPackets : data(Q', NZN, NZN', R') DB, reTransBuf : RTB, nextSeq : NZN'', sendDataTimer : 0, maxSeqSent : MSS, winLowerSeq : WLS, csmNominee : DQ, winSize : WS, fastRecovFlag : FRF, maxBurstCount : MBC, ccmTimer : TI, timerNominee : DQ', backOffFactor : BOF, ccmTimeout : CCMTO > => if (NZN'' == MSS plus 1) and sendAllowed(MSS, WLS, WS, FRF, MBC) then < Q : SenderCombined | 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), 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) > multiSend(dataPacket(Q', NZN'', R, NZN == 1, NZN =/= 1 and NZN =/= NZN', false), Q, OS) else < Q : SenderCombined | sendDataTimer : 1 > fi . *** Reception of a data packet which is not stored (or already sent *** to application). crl [B3bE2H1] : (dataPacket(Q''', NZN, R, X, Y, Z) from Q to Q') < Q'' : RandomNGen | seed : N > < Q' : ReceiverCombined | isNominee : X', fastRepairFlag : FRF, repairserver : Q'''', readNextSeq : NZN', suppressTO : R', dataBuffer : MC, dataInfo : DI, msgWindow : W > => < Q'' : RandomNGen | seed : (if FRF then N else repeatRandom(N, (NZN - 1) monus max(NZN' - 1, highestNzNAKSeqNo(DI), highestSeqNo(MC))) fi) > < Q' : ReceiverCombined | 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), FRF, max(NZN', highestSeqNo(MC) + 1, highestNzNAKSeqNo(DI) + 1), NZN - 1, R', N), lastSeqNo(toApp(MC dataPacket(Q''', NZN, R, X, Y, Z), NZN'))), msgWindow : add(NZN, W) > toApp((dataPacket(Q''', NZN, R, X, Y, Z) MC), NZN', Q') (if X' then send(ccmPacket(Q', max(NZN', lastSeqNo(toApp(dataPacket(Q''', NZN, R, X, Y, Z) MC, NZN')) + 1), R, Z), Q', Q'''') else none fi) if NZN' <= NZN and not (NZN seqNoIn MC) . rl [C1initR2F1] : (SPMPacket(N) from Q to Q') < Q'' : RandomNGen | seed : N' > < Q' : RepairserverCombined | SPMread : false > => (SPMPacket(N) from Q to Q') < Q'' : RandomNGen | seed : random(N') > < Q' : RepairserverCombined | SPMread : true, csmTimer : 7000, getRTTResendTimer : random(N') rem 31 > . *** We are also supposed to combine D2 and G14, but I fail to *** see how G14 will apply. Anyways, on request, here it comes: rl [D2D3G14] : (csmPacket(DR, TI, DQ') from Q to Q') < Q' : SenderCombined | clock : R, csmNominee : DQ, csmLPE : DR', csmRTT : TI', csmSetTime : R', NAMTimer : TI'', ccmTimeout : CCMTO > => if updateNomValues(DR, TI, DQ', DQ, DR', TI', R, R') then < Q' : SenderCombined | csmNominee : DQ', csmLPE : DR, csmRTT : TI, csmSetTime : R, NAMTimer : (if DQ =/= DQ' then 7000 else TI'' fi), ccmTimeout : (if DQ' == noOid and DQ' =/= DQ then 1000 else CCMTO 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' : SenderCombined | > fi . *** Timed behavior: eq mte(< Q : SenderCombined | NAMTimer : TI, ccmTimer : TI', SPMTimer : TI'', sendDataTimer : TI''' >) = min(TI, TI', TI'', TI''') . eq delta(< Q : SenderCombined | clock : R, NAMTimer : TI, ccmTimer : TI', sendDataTimer : TI'', SPMTimer : TI''' >, R') = < Q : SenderCombined | clock : R plus R' , NAMTimer : TI monus R', ccmTimer : TI' monus R', sendDataTimer : TI'' monus R', SPMTimer : TI''' monus R' > . eq mte(< Q : RepairserverCombined | getRTTResendTimer : TI, csmTimer : TI', SPMWaitTimer : TI'', NAKStates : NS >) = min(TI, TI', TI'', mte(NS)) . eq delta(< Q : RepairserverCombined | clock : R, getRTTResendTimer : TI, csmTimer : TI', SPMWaitTimer : TI'', NAKStates : NS >, R') = < Q : RepairserverCombined | clock : R plus R', getRTTResendTimer : TI monus R', csmTimer : TI' monus R', SPMWaitTimer : TI'' monus R', NAKStates : delta(NS, R') > . eq mte(< Q : ReceiverCombined | getRTTResendTimer : TI, csmTimer : TI', dataInfo : DI >) = min(TI, TI', mte(DI)) . eq delta(< Q : ReceiverCombined | clock : R, getRTTResendTimer : TI, csmTimer : TI', dataInfo : DI >, R') = < Q : ReceiverCombined | clock : R plus R', getRTTResendTimer : TI monus R', csmTimer : TI' monus R', dataInfo : delta(DI, R') > . endtom) (tomod COMBINED-PROTOCOL1 is including COMBINED-PROTOCOL . including AER-APPLICATIONS . var N : Nat . *** The next System is one proposed by Mark Keaton in Boston: op State2 : Nat -> GlobalSystem . --- send 21 packets to 4 rcvr applications eq State2(N) = ({ startRS('a) < 'SenderApp : SenderApplication | dataBlocksToBeSent : dly(dataBlock('first, 'a, 20, 5), 100) + dly(dataBlock('second, 'a, 1, 100), 800) > < 'RecvrAppB : RecvrApplication | receiver : 'b, dataRead : none > < 'RecvrAppE : RecvrApplication | receiver : 'e, dataRead : none > < 'RecvrAppF : RecvrApplication | receiver : 'f, dataRead : none > < 'RecvrAppG : RecvrApplication | receiver : 'g, dataRead : none > < 'a : SenderCombined | clock : 0, sourceRTT : 0, children : 'b 'c, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, NAMTimer : INF, csmLPE : noRat, csmRTT : 0, csmSetTime : 0, csmNominee : noOid, timerNominee : noOid, winSize : 1, winLowerSeq : 1, dupLowerSeq : 0, maxSeqSent : 0, smoothedRTT : 0, rttVariance : 0, ccmTimeout : 1000, ssThreshold : 64, backOffFactor : 1, fastRecovFlag : false, fastRecovSeq : 0, maxBurstCount : 0, ccmTimer : INF, nextSeq : 1, SPMTimer : INF, reTransBuf : none, unsentDataPackets : nil, sendDataTimer : INF > < 'b : ReceiverCombined | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, isNominee : false, msgWindow : initWindow(4), csmTimer : INF, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'c : RepairserverCombined | clock : 0, sourceRTT : INF, children : 'd 'e, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF , SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'd : RepairserverCombined | clock : 0, sourceRTT : INF, children : 'f 'g, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'e : ReceiverCombined | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, isNominee : false, msgWindow : initWindow(4), csmTimer : INF, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'f : ReceiverCombined | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, isNominee : false, msgWindow : initWindow(4), csmTimer : INF, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'g : ReceiverCombined | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, isNominee : false, msgWindow : initWindow(4), csmTimer : INF, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'random : RandomNGen | seed : N > < 'ab : Link | up : 'a, down : 'b, bound : 5, propDelay : 21, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'ac : Link | up : 'a, down : 'c, bound : 21, propDelay : 28, linkSpeed : 3, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'cd : Link | up : 'c, down : 'd, bound : 9, propDelay : 23, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'ce : Link | up : 'c, down : 'e, bound : 4, propDelay : 17, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'df : Link | up : 'd, down : 'f, bound : 12, propDelay : 5, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'dg : Link | up : 'd, down : 'g, bound : 12, propDelay : 5, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 >}) . op State3 : Nat -> GlobalSystem . --- send 35 packets eq State3(N) = ({ startRS('a) < 'SenderApp : SenderApplication | dataBlocksToBeSent : dly(dataBlock('first, 'a, 35, 5), 100) > < 'RecvrAppC : RecvrApplication | receiver : 'c, dataRead : none > < 'a : SenderCombined | clock : 0, sourceRTT : 0, children : 'b, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, NAMTimer : INF, csmLPE : noRat, csmRTT : 0, csmSetTime : 0, csmNominee : noOid, timerNominee : noOid, winSize : 1, winLowerSeq : 1, dupLowerSeq : 0, maxSeqSent : 0, smoothedRTT : 0, rttVariance : 0, ccmTimeout : 1000, ssThreshold : 64, backOffFactor : 1, fastRecovFlag : false, fastRecovSeq : 0, maxBurstCount : 0, ccmTimer : INF, nextSeq : 1, SPMTimer : INF, reTransBuf : none, unsentDataPackets : nil, sendDataTimer : INF > < 'b : RepairserverCombined | clock : 0, sourceRTT : INF, children : 'c, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF , SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'c : ReceiverCombined | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF, isNominee : false, msgWindow : initWindow(4), csmTimer : INF, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'random : RandomNGen | seed : N > < 'ab : Link | up : 'a, down : 'b, bound : 10, propDelay : 100, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'bc : Link | up : 'b, down : 'c, bound : 10, propDelay : 1, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 >}) . endtom) --- ------------ --- Prototyping: --- (trew State3(1) in time <= 20000 .) --- successfull, all 35 packets delivered to rcvr application --- but lots of repairs have been successfully performed, which is good --- (trew State2(1) in time <= 20000 .) --- also successfull --- Further model checking and search --- --------------------------------- --- We could be interested in either finding new errors, or checking --- whether the errors discovered earlier are actually possible in --- the combined protocol, which they of course are/should be. --- The only really interesting problem is checking whether the serious --- problems in the RS component also can show up in the combined protocol. --- However, these searches choke on my machines: ***( (tsearch [1] State3(1) =>* {ERROR(S:String, AS:AttributeSet) C:Configuration} in time <= 5900 .) )*** --- it doesn't go much beyond 5900 (in 482 sec on a 2 GHz machine) --- even for this fairly simple initial state