*** Real-Time Maude 2.1 specification of AER/NCA, by Peter Csaba Olveczky *** Executable file for the NCA-RC protocol. *** Extends ncarc.rtmaude with initial states and analysis commands, *** commented away ... in AER-prelude.rtmaude in AER-commonclasses.rtmaude in AER-shared-atts.rtmaude in EfficientWindow.rtmaude *** Imports list of natural numbers. in ncarc.rtmaude (tomod NCA-RC1 is protecting NCA-RC . op RCstate1 : -> GlobalSystem . eq RCstate1 = ({< 'a : RCsenderAlone | clock : 0, children : 'b, 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, nextNoToSend : 1, sendDataTimer : 6000, sentTimes : nil > < 'b : RCrepairserverAlone | children : 'c, repairserver : 'a > < 'c : RCreceiverAlone | isNominee : false, msgRcvd : nil > < 'env : Env | msgsFromEnv : dly(nomineeIs('c), 1444) dly(NAMPacket(true) from 'a to 'c, 1444) > < 'ab : Link | up : 'a, down : 'b, bound : 6, propDelay : 10, 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) --- Prototyping --- ----------- ---(trew RCstate1 in time <= 6800 .) --- gives slightly unexpected result --- It gets more fishy from here on, as we check whether also some more --- expected results can be reached ... --- Search for the result in the thesis: --- ------------------------------------ --- Using timed rewriting of this specification in Version 1.0 --- of the tool gave a more desired result. That indicates that --- the specification may be quite nondeterministic. Is it possible to --- find the desired state? --- We search for all the states reachable in exactly time 6700: ***( (tsearch RCstate1 =>* {C:Configuration} in time-interval between >= 6700 and <= 6700 .) )*** --- Unfortunately, because of the high degree of nondeterminism, the above --- search does not terminate within reasonable time/memory --- Instead, we split the search into --- a. search for all states reachable in time 6000 --- b. check if a state resembling the one in the thesis is found --- c. search for all states reachable from the state found in b --- in time 6200 --- d. check if a state resembling the one in the thesis is found --- e. search for all states reachable from the state found in b --- in time 6400 --- ... --- finish: check if the desired state is found in time 6700. --- Start with the state reachable in time 6000 and find --- the states reachable in time 6200: ***( (tsearch {< 'b : RCrepairserverAlone | children : 'c, repairserver : 'a > < 'a : RCsenderAlone | clock : 6000, children : 'b, csmNominee : 'c, ccmTimer : INF, maxBurstCount : 1, fastRecovSeq : 0, fastRecovFlag : false, backOffFactor : 1, ssThreshold : 64, ccmTimeout : 1000, rttVariance : 0, smoothedRTT : 0, maxSeqSent : 1, dupLowerSeq : 0, winLowerSeq : 1, winSize : 1, timerNominee : noOid, sentTimes : 6000, nextNoToSend : 2, sendDataTimer : 1 > < 'c : RCreceiverAlone | isNominee : true, msgRcvd : nil > < 'env : Env | msgsFromEnv : none > < 'ab : Link | upSize : 0, upMsgs : nil, downSize : 1, downMsgs : dly(ncarcDataPacket(1,6000,false), 22), linkSpeed : 1, propDelay : 10, bound : 6, up : 'a, down : 'b > < 'bc : Link | upSize : 0, upMsgs : nil, downSize : 0, downMsgs : nil, linkSpeed : 1, propDelay : 10, bound : 3, up : 'b, down : 'c >} in time 6000 =>* {C:Configuration} in time-interval between >= 6200 and <= 6200 .) )*** --- Continue the search ... take the most promising of 6200-states and --- search for states reachable in time 6300: ***( (tsearch {< 'b : RCrepairserverAlone | children : 'c, repairserver : 'a > < 'a : RCsenderAlone | clock : 6200, children : 'b, csmNominee : 'c, ccmTimer : 102, maxBurstCount : 2, fastRecovSeq : 0, fastRecovFlag : false, backOffFactor : 1, ssThreshold : 64, ccmTimeout : 103, rttVariance : 9, smoothedRTT : 67, maxSeqSent : 9, dupLowerSeq : 0, winLowerSeq : 5, winSize : 5, timerNominee : 'c, sentTimes : (6000 ++ 6066 ++ 6067 ++ 6132 ++ 6133 ++ 6144 ++ 6145 ++ 6198 ++ 6199), nextNoToSend : 10, sendDataTimer : 1 > < 'c : RCreceiverAlone | isNominee : true, msgRcvd : (1 ++ 2 ++ 3 ++ 4 ++ 5 ++ 6) > < 'env : Env | msgsFromEnv : none > < 'ab : Link | upSize : 1, upMsgs : dly(ccmPacket('c,6,6133,false),10), downSize : 2, downMsgs : (dly(ncarcDataPacket(8,6198,false), 20) + dly(ncarcDataPacket(9,6199,false), 32)), linkSpeed : 1, propDelay : 10, bound : 6, up : 'a, down : 'b > < 'bc : Link | upSize : 1, upMsgs : dly(ccmPacket('c,7,6144,false),11), downSize : 1, downMsgs : dly(ncarcDataPacket(7,6145,false), 12), linkSpeed : 1, propDelay : 10, bound : 3, up : 'b, down : 'c >} in time 6200 =>* {C:Configuration} in time-interval between >= 6300 and <= 6300 .) )*** --- note that just this subsearch had 512 distinct solutions ... --- Continue search to time 6400 with promising result from above: ***( (tsearch {< 'b : RCrepairserverAlone | children : 'c, repairserver : 'a > < 'a : RCsenderAlone | clock : 6300, children : 'b, csmNominee : 'c, ccmTimer : 117, maxBurstCount : 1, fastRecovSeq : 0, fastRecovFlag : false, backOffFactor : 1, ssThreshold : 64, ccmTimeout : 117, rttVariance : 11, smoothedRTT : 73, maxSeqSent : 22, dupLowerSeq : 0, winLowerSeq : 12, winSize : 12, timerNominee : 'c, sentTimes : (6000 ++ 6066 ++ 6067 ++ 6132 ++ 6133 ++ 6144 ++ 6145 ++ 6198 ++ 6199 ++ 6210 ++ 6211 ++ 6222 ++ 6223 ++ 6234 ++ 6235 ++ 6264 ++ 6265 ++ 6276 ++ 6277 ++ 6288 ++ 6289 ++ 6300), nextNoToSend : 23, sendDataTimer : 1 > < 'c : RCreceiverAlone | isNominee : true, msgRcvd : (1 ++ 2 ++ 3 ++ 4 ++ 5 ++ 6 ++ 7 ++ 8 ++ 9 ++ 10 ++ 11 ++ 12) > < 'env : Env | msgsFromEnv : none > < 'ab : Link | upSize : 0, upMsgs : nil, downSize : 6, downMsgs : (dly(ncarcDataPacket(15,6235,false), 4) + dly(ncarcDataPacket(16,6264,false), 16) + dly(ncarcDataPacket(17,6265,false), 28) + dly(ncarcDataPacket(18,6276,false), 40) + dly(ncarcDataPacket(20,6288,false) ,52 )+ dly(ncarcDataPacket(22,6300,false),64)), linkSpeed : 1, propDelay : 10, bound : 6, up : 'a, down : 'b > < 'bc : Link | upSize : 1, upMsgs : dly(ccmPacket('c,13,6222,false), 1), downSize : 2, downMsgs : (dly(ncarcDataPacket(13,6223,false), 2) + dly(ncarcDataPacket(14,6234,false), 14)), linkSpeed : 1, propDelay : 10, bound : 3, up : 'b, down : 'c >} in time 6300 =>* {C:Configuration} in time-interval between >= 6400 and <= 6400 .) )*** --- This subsearch had 1024 solutions! --- Continue with search for states in time 6500! ***( (tsearch {< 'b : RCrepairserverAlone | children : 'c, repairserver : 'a > < 'a : RCsenderAlone | clock : 6400, children : 'b, csmNominee : 'c, ccmTimer : 147, maxBurstCount : 0, fastRecovSeq : 0, fastRecovFlag : false, backOffFactor : 1, ssThreshold : 64, ccmTimeout : 164, rttVariance : 18, smoothedRTT : 92, maxSeqSent : 37, dupLowerSeq : 1, winLowerSeq : 19, winSize : 19, timerNominee : 'c, sentTimes : (6000 ++ 6066 ++ 6067 ++ 6132 ++ 6133 ++ 6144 ++ 6145 ++ 6198 ++ 6199 ++ 6210 ++ 6211 ++ 6222 ++ 6223 ++ 6234 ++ 6235 ++ 6264 ++ 6265 ++ 6276 ++ 6277 ++ 6288 ++ 6289 ++ 6300 ++ 6301 ++ 6312 ++ 6313 ++ 6324 ++ 6325 ++ 6336 ++ 6337 ++ 6348 ++ 6349 ++ 6360 ++ 6361 ++ 6372 ++ 6373 ++ 6384 ++ 6385), nextNoToSend : 38, sendDataTimer : 1 > < 'c : RCreceiverAlone | isNominee : true, msgRcvd : (1 ++ 2 ++ 3 ++ 4 ++ 5 ++ 6 ++ 7 ++ 8 ++ 9 ++ 10 ++ 11 ++ 12 ++ 13 ++ 14 ++ 15 ++ 16 ++ 17 ++ 18 ++ 20 ++ 22 ++ 24) > < 'env : Env | msgsFromEnv : none > < 'ab : Link | upSize : 1, upMsgs : dly(ccmPacket('c,19,6300,false), 8), downSize : 4, downMsgs : (dly(ncarcDataPacket(30,6348,false), 12) + dly(ncarcDataPacket(32,6360,false), 24) + dly(ncarcDataPacket(34,6372,false), 36) + dly(ncarcDataPacket(36,6384,false), 48)), linkSpeed : 1, propDelay : 10, bound : 6, up : 'a, down : 'b > < 'bc : Link | upSize : 1, upMsgs : dly(ccmPacket('c,19,6312,false), 9), downSize : 2, downMsgs : (dly(ncarcDataPacket(26,6324,false), 10) + dly(ncarcDataPacket(28,6336,false), 22)), linkSpeed : 1, propDelay : 10, bound : 3, up : 'b, down : 'c >} in time 6400 =>* {C:Configuration} in time-interval between >= 6500 and <= 6500 .) )*** --- The final search. The last result is the one given in the paper. ***( (tsearch {< 'b : RCrepairserverAlone | children : 'c, repairserver : 'a > < 'a : RCsenderAlone | clock : 6500, children : 'b, csmNominee : 'c, ccmTimer : 47, maxBurstCount : 0, fastRecovSeq : 0, fastRecovFlag : true, backOffFactor : 1, ssThreshold : 64, ccmTimeout : 145, rttVariance : 11, smoothedRTT : 101, maxSeqSent : 37, dupLowerSeq : 9, winLowerSeq : 19, winSize : 19, timerNominee : 'c, sentTimes : (6000 ++ 6066 ++ 6067 ++ 6132 ++ 6133 ++ 6144 ++ 6145 ++ 6198 ++ 6199 ++ 6210 ++ 6211 ++ 6222 ++ 6223 ++ 6234 ++ 6235 ++ 6264 ++ 6265 ++ 6276 ++ 6277 ++ 6288 ++ 6289 ++ 6300 ++ 6301 ++ 6312 ++ 6313 ++ 6324 ++ 6325 ++ 6336 ++ 6337 ++ 6348 ++ 6349 ++ 6360 ++ 6361 ++ 6372 ++ 6373 ++ 6384 ++ 6385), nextNoToSend : 38, sendDataTimer : 1 > < 'c : RCreceiverAlone | isNominee : true, msgRcvd : (1 ++ 2 ++ 3 ++ 4 ++ 5 ++ 6 ++ 7 ++ 8 ++ 9 ++ 10 ++ 11 ++ 12 ++ 13 ++ 14 ++ 15 ++ 16 ++ 17 ++ 18 ++ 20 ++ 22 ++ 24 ++ 26 ++ 28 ++ 30 ++ 32 ++ 34 ++ 36) > < 'env : Env | msgsFromEnv : none > < 'ab : Link | upSize : 0, upMsgs : nil, downSize : 0, downMsgs : nil, linkSpeed : 1, propDelay : 10, bound : 6, up : 'a, down : 'b > < 'bc : Link | upSize : 0, upMsgs : nil, downSize : 0, downMsgs : nil, linkSpeed : 1, propDelay : 10, bound : 3, up : 'b, down : 'c >} in time 6500 =>* {C:Configuration} in time-interval between >= 6700 and <= 6700 .) )*** --- The last of those solutions is it!!