*** Test file for RS component of Real-Time Maude 2.1 specification of AER/NCA *** protocol suite. *** By Peter Csaba Olveczky, with warmest thanks to Mark Keaton for suggestions *** of some of the initial states below. *** Executable file for the rs protocol, which also includes the application *** layer, and commands to test the application layer/RS component in AER-prelude.rtmaude *** Starts up everything. in AER-commonclasses.rtmaude in AER-shared-atts.rtmaude in AER-shared-msgs.rtmaude in AER-error-object.rtmaude in rs.rtmaude in appLayer.rtmaude (tomod RS-APPLICATIONS is including AER-APPLICATIONS . var N : Nat . op RSstate1 : Nat -> GlobalSystem . --- send 110 packets eq RSstate1(N) = ({ startRS('a) < 'SenderApp : SenderApplication | dataBlocksToBeSent : dly(dataBlock('first, 'a, 60, 100), 100) + dly(dataBlock('second, 'a, 50, 60), 800) > < 'RecvrAppD : RecvrApplication | receiver : 'd, dataRead : none > < 'RecvrAppI : RecvrApplication | receiver : 'i, dataRead : none > < 'a : RSsenderAlone | clock : 0, children : 'b 'c, nextSeq : 1, SPMTimer : INF, reTransBuf : none, unsentDataPackets : nil, sendDataTimer : INF > < 'b : RSrepairserverAlone | children : 'd, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'c : RSrepairserverAlone | children : 'f, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'd : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'f : RSrepairserverAlone | children : 'i, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'i : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'random : RandomNGen | seed : N > < 'env : Env | msgsFromEnv : dly(NAMPacket(true) from 'b to 'd, 1444) dly(newRTT(70, 70, 'b), 3000) dly(newRTT(30, 70, 'c), 3500) dly(newRTT(90, 20, 'd), 3600) dly(newRTT(86, 10, 'f), 2300) dly(newRTT(96, 10, 'i), 1300) > < 'ac : Link | up : 'a, down : 'c, bound : 6, propDelay : 14, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'ab : Link | up : 'a, down : 'b, bound : 18, propDelay : 35, linkSpeed : 2, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'bd : Link | up : 'b, down : 'd, bound : 14, propDelay : 10, linkSpeed : 8, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'cf : Link | up : 'c, down : 'f, bound : 11, propDelay : 27, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'fi : Link | up : 'f, down : 'i, bound : 12, propDelay : 5, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > }) . *** Suggested by Mark Keaton in Boston: op RSstate2 : Nat -> GlobalSystem . eq RSstate2(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 : RSsenderAlone | clock : 0, children : 'b 'c, nextSeq : 1, SPMTimer : INF, reTransBuf : none, unsentDataPackets : nil, sendDataTimer : INF > < 'b : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'c : RSrepairserverAlone | children : 'd 'e, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'd : RSrepairserverAlone | children : 'f 'g, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'e : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'f : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'g : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'random : RandomNGen | seed : N > < 'env : Env | msgsFromEnv : dly(NAMPacket(true) from 'd to 'f, 1444) dly(newRTT(44, 56, 'b), 75) dly(newRTT(56, 56, 'c), 89) dly(newRTT(92, 48, 'e), 180) dly(newRTT(114, 10, 'f), 362) dly(newRTT(114, 10, 'g), 355) dly(newRTT(104, 48, 'd), 200) > < '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 >}) . *** Some new states suggested by Mark Keaton May 15, 2000. op RSstate3 : Nat -> GlobalSystem . eq RSstate3(N) = ({ startRS('a) < 'SenderApp : SenderApplication | dataBlocksToBeSent : dly(dataBlock('first, 'a, 35, 5), 100) > < 'RecvrAppC : RecvrApplication | receiver : 'c, dataRead : none > < 'a : RSsenderAlone | clock : 0, children : 'b, nextSeq : 1, SPMTimer : INF, reTransBuf : none, unsentDataPackets : nil, sendDataTimer : INF > < 'b : RSrepairserverAlone | children : 'c, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 10), NAKStates : none > < 'c : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'random : RandomNGen | seed : N > < 'env : Env | msgsFromEnv : dly(NAMPacket(true) from 'b to 'c, 2) dly(newRTT(220, 220, 'b), 3) dly(newRTT(210, 4, 'c), 4) > < '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 >}) . *** Case 2 proposed by Mark Keaton May 16, 2000: op RSstate4 : Nat -> GlobalSystem . eq RSstate4(N) = ({ startRS('a) < 'SenderApp : SenderApplication | dataBlocksToBeSent : dly(dataBlock('first, 'a, 35, 5), 100) > < 'RecvrAppC : RecvrApplication | receiver : 'c, dataRead : none > < 'a : RSsenderAlone | clock : 0, children : 'b, nextSeq : 1, SPMTimer : INF, reTransBuf : none, unsentDataPackets : nil, sendDataTimer : INF > < 'b : RSrepairserverAlone | children : 'c, repairserver : noOid, SPMread : false, maxSeqRcvd : 0, SPMWaitTimer : INF, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : bBuf(nil, 0, 1), NAKStates : none > < 'c : RSreceiverAlone | repairserver : noOid, isNominee : false, fastRepairFlag : false, readNextSeq : 1, smoothedRTT : 0, rttVariance : 3000, suppressTO : 100, retransTO : 6000, dataBuffer : none, dataInfo : none, SPMread : false > < 'random : RandomNGen | seed : N > < 'env : Env | msgsFromEnv : dly(NAMPacket(true) from 'b to 'c, 2) dly(newRTT(44, 44, 'b), 3) dly(newRTT(62, 21, 'c), 4) > < 'ab : Link | up : 'a, down : 'b, bound : 10, propDelay : 20, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'bc : Link | up : 'b, down : 'c, bound : 3, propDelay : 10, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 >}) . endtom) --- The following timed rewrite command finds the first error: --- (trew RSstate2(113) in time <= 20000 .) --- This rewrite command should also find an error: --- (trew RSstate3(113) in time <= 400000 .) --- Finally, a good execution, both receiver application objects --- have received all 110 packets: --- (trew RSstate1(113) in time <= 400000 .)