*** Real-Time Maude 2.1 Specification of the AER/NCA Protocol Suite. *** Written by Peter Csaba Olveczky. *** Prelude for the Real-Time Maude 2.1 version of the AER protocol. load ../real-time-maude *** Start Real-Time Maude *** Time domain: We choose again the Natural numbers as the time domain. (fmod AER-TIME-DOMAIN is protecting NAT-TIME-DOMAIN-WITH-INF . endfm) *** Datatype of ordered lists of time values and of natural numbers. *** Used e.g. in the RC component to record stored messages *** and sending times. (fmod ORDERED-NAT-TIME-LIST is protecting NAT-TIME-DOMAIN . sorts OrderedNatList OrderedNzNatList OrderedTimeList . subsort NzNat < OrderedNzNatList . subsort Nat < OrderedNatList . subsort Time < OrderedTimeList . subsorts OrderedNzNatList < OrderedNatList < OrderedTimeList . op nil : -> OrderedNzNatList . op _++_ : OrderedNzNatList OrderedNzNatList -> OrderedNzNatList [assoc id: nil] . op _++_ : OrderedNatList OrderedNatList -> OrderedNatList [assoc id: nil] . op _++_ : OrderedTimeList OrderedTimeList -> OrderedTimeList [assoc id: nil] . *** Some helpful functions op last : OrderedTimeList -> Nat . *** Last element of a list [0 if empty] op _inList_ : Time OrderedTimeList -> Bool . op add : Time OrderedTimeList -> OrderedTimeList . vars TL TL' : OrderedTimeList . vars R R' R'' R''' R'''' : Time . eq last(nil) = 0 . eq last(R ++ TL) = if TL == nil then R else last(TL) fi . eq R inList nil = false . eq R inList R' ++ TL = if R == R' then true else (if R lt R' then false else R inList TL fi) fi . eq add(R, nil) = R . eq add(R, R' ++ TL) = if R == R' then (R' ++ TL) else (if R lt R' then (R ++ (R' ++ TL)) else (R' ++ add(R, TL)) fi) fi . endfm) *** We now define the functions mte and delta to distribute over the elements *** in a configuration. *** Note that delta and mte are frozen operators: (omod OID-SET is including QID . *** We define the object identifiers, which are normally Qid's, *** and a "default/error" value noOid, and then sets of Oid's: subsort Qid < Oid . *** Oid's are just quoted identifiers. sort DefOid . *** Oid's with a default value, namely noOid. subsort Oid < DefOid . op noOid : -> DefOid . sort OidSet . subsort Oid < OidSet . op none : -> OidSet . op __ : OidSet OidSet -> OidSet [assoc comm id: none prec 15] . endom) (tomod TIMED-OO-SYSTEM is including LTIME-INF . vars NECF NECF' : NEConfiguration . var R : Time . op delta : Configuration Time -> Configuration [frozen (1)] . eq delta(none, R) = none . eq delta(NECF NECF', R) = delta(NECF, R) delta(NECF', R) . op mte : Configuration -> TimeInf [frozen (1)] . eq mte(none) = INF . eq mte(NECF NECF') = min(mte(NECF), mte(NECF')) . endtom) *** All the protocols have the same tick rule: *** Time only advances when no messages are present, *** of course messages may be inside objects such as channels, etc. (tomod TICK-RULE is including TIMED-OO-SYSTEM . protecting AER-TIME-DOMAIN . var OC : NEObjectConfiguration . var R : Time . crl [tick] : {OC} => {delta(OC, R)} in time R if R <= mte(OC) [nonexec] . endtom) *** There are no instantaneous rules which occurs at times which *** are not visited by a "maximal" time sampling strategy, so we *** set the time sampling strategy to be "max" FOR EFFICIENCY purposes. *** The "standard" way to treat discrete time domain, as in our case, *** is of course to increment time by 1. (set tick max .) *** Modeling of links: (tomod LINK is including TIMED-OO-SYSTEM . including AER-TIME-DOMAIN . including OID-SET . *** A buffer may be full when a message wants to be sent, while *** at the same time, a message in the channel may have delay 0 and is *** on his way out. Should the the channel first relaese the ripe message, *** thereby avoiding the loss of the message, or should this case be *** treated non-deterministically, with the possibility of loss of message *** in this case? As seen from the rules taking in a message *** to a channel, I choose the former version. *** Lists of messages may be the most appropriate way of storing *** the messages: sort MsgList . subsort Msg < MsgList . op nil : -> MsgList . op _+_ : MsgList MsgList -> MsgList [assoc id: nil] . *** I choose to see the leftmost element in a channel as the "oldest" *** element. Elements must therefore be input on the right *** and taken out from the left! class Link | up : Oid, *** "Upnode" down : Oid, *** "DownNode" bound : NzNat, *** Maximal size of buffer in link propDelay : NzTime, *** Propagation delay. Constant. linkSpeed : NzNat, *** in megabits per sec. downMsgs : MsgList, *** Buffer of messages going downstream downSize : Nat, *** size of above upMsgs : MsgList, *** Buffer of messages going upstream upSize : Nat . *** size of above *** Messages to the links are of the form *** send("original message", senderOid, recvrOid). In the link, they are *** of the form dly("original message", time-until-delivered): msg send : Msg Oid Oid -> Msg . msg dly : Msg Time -> Msg . var M : Msg . vars R R' R'' : Time . vars NZR : NzTime . vars ML ML' : MsgList . vars Q Q' Q'' : Oid . vars N N' : Nat . var NZN : NzNat . vars TI TI' : TimeInf . var CF : Configuration . var OS : OidSet . *** To be sure that there is an address to the receiver of a message that is *** thrown out of a link, the sender and receiver is added to each message: msg _from_to_ : Msg Oid Oid -> Msg . *** The functions leastDly and greatestDly gives the least and greatest *** delay of a message in the message list: op leastDly : MsgList -> TimeInf . eq leastDly(nil) = INF . eq leastDly(dly(M, R) + ML) = R . op greatestDly : MsgList -> Time . eq greatestDly(nil) = 0 . eq greatestDly(ML + dly(M, R)) = R . *** The transmission delay of a packet is (packetSize) / linkSpeed, so *** that the units coincide, and the delay of the next packet to enter *** is max(propDelay, greatestDlyInChannel) + transmissionDelay. *** All packets except data packets are of size 64 bytes, while *** data packets are around 1500 bytes. Link speed is around 1/1.5/3/10 (?) *** mbs, bound is usually ((2 to 4) times (linkSpeed times propDelya)) div *** packetSize, although it is not clear what packetsizes to use. *** We have two forms of packets depending on size, as mentioned, *** normal packets of size 64 bytes, and large packets (data packets) of *** around 1500 bytes, and they have their appropriate subsorts, from which *** we can compute the delays according to the formulas above. sorts Packet LargePacket . subsort Packet < Msg . subsort LargePacket < Msg . var SMALLPACKET : Packet . var LARGEPACKET : LargePacket . *** Transmission delay given message and link speed: op transDelay : Msg NzNat -> Time . eq transDelay(SMALLPACKET, NZN) = (64 * 8 + ((NZN * 1000) monus 1)) quo (NZN * 1000) . eq transDelay(LARGEPACKET, NZN) = (1500 * 8 + ((NZN * 1000) monus 1)) quo (NZN * 1000) . *** NZN times 1000 gives bits per millisecond, and we also round off *** to closest integer. *** Sending packets to a link, and sending from a link into the soup: crl [intoLinkDown] : send(M, Q, Q') < Q'' : Link | up : Q, down : Q', bound : N, propDelay : NZR, linkSpeed : NZN, downMsgs : ML, downSize : N' > => if N' < N then < Q'' : Link | downMsgs : ML + dly(M, max(NZR, greatestDly(ML)) + transDelay(M, NZN)), downSize : N' + 1 > else < Q'' : Link | > fi if leastDly(ML) =/= 0 . crl [intoLinkUp] : send(M, Q, Q') < Q'' : Link | down : Q, up : Q', bound : N, propDelay : NZR, linkSpeed : NZN, upMsgs : ML, upSize : N' > => if N' < N then < Q'' : Link | upMsgs : ML + dly(M, max(NZR, greatestDly(ML)) + transDelay(M, NZN)), upSize : N' + 1 > else < Q'' : Link | > fi if leastDly(ML) =/= 0 . *** A message is ripe to get out of the link when its dly is 0: rl [outOfUpLink] : < Q : Link | down : Q', up : Q'', upMsgs : dly(M, 0) + ML, upSize : s N > => (M from Q' to Q'') < Q : Link | upMsgs : ML, upSize : N > . rl [outOfDownLink] : < Q : Link | down : Q', up : Q'', downMsgs : dly(M, 0) + ML, downSize : s N > => (M from Q'' to Q') < Q : Link | downMsgs : ML, downSize : N > . *** The timed behavior of a link is as follows: *** I assume that these classes will never have subclasses, otherwise *** the major extension with all subclass-checking must be done: eq delta(< Q : Link | downMsgs : ML, upMsgs : ML' >, R) = < Q : Link | downMsgs : ML minus R, upMsgs : ML' minus R > . op _minus_ : MsgList Time -> MsgList . --- decrease delay of messages eq nil minus R = nil . ceq (ML + ML') minus R = (ML minus R) + (ML' minus R) if ML =/= nil and ML' =/= nil . eq (dly(M, R) minus R') = dly(M, R monus R') . eq mte(< Q : Link | downMsgs : ML, upMsgs : ML' >) = min(leastDly(ML), leastDly(ML')) . *** Multimessages. Messages send to an OidSet of objects. msg multiSend : Msg Oid OidSet -> Configuration . eq multiSend(M, Q, (Q' OS)) = send(M, Q, Q') multiSend(M, Q, OS - Q') . eq multiSend(M, Q, none) = none . op _-_ : OidSet Oid -> OidSet . eq (Q OS) - Q' = if Q == Q' then OS - Q' else Q (OS - Q') fi . eq none - Q = none . eq Q Q = Q . *** removes duplicates endtom) *** ENVIRONMENT. *** When running the protocols separately, we may want to get *** messages from other *** parts of the protocol, that is, the environment. We could therefore *** have a special environment object which generates *** such messages. For a more restrictive first *** prototyping, I use a simpler setting, where the environment *** is just a container of (delayed) messages to be spread out *** in the soup. That is, the initial state must contain all the messages *** to be sent from the environment. (tomod ENVIRONMENT is including LINK . var Q : Oid . var MC : MsgConfiguration . vars NEMC NEMC' : NEMsgConfiguration . var CF : Configuration . var M : Msg . vars R R' : Time . class Env | msgsFromEnv : MsgConfiguration . rl [env1] : { < Q : Env | msgsFromEnv : dly(M, 0) MC > CF } => { < Q : Env | msgsFromEnv : MC > M CF } . eq mte(< Q : Env | msgsFromEnv : MC >) = leastDly(MC) . op leastDly : MsgConfiguration -> TimeInf . eq leastDly(dly(M, R)) = R . eq leastDly(none) = INF . eq leastDly(NEMC NEMC') = min(leastDly(NEMC), leastDly(NEMC')) . eq delta(< Q : Env | msgsFromEnv : MC >, R) = < Q : Env | msgsFromEnv : delta(MC, R) > . eq delta(NEMC NEMC', R) = delta(NEMC, R) delta(NEMC', R) . eq delta(none, R) = none . eq delta(dly(M, R), R') = dly(M, R monus R') . endtom) *** The last module introduces the random number generator, *** which is used by most protocols: (omod RANDOM is including NAT . class RandomNGen | seed : Nat . op random : Nat -> Nat . *** random(x) generates the next random number vars N N' : Nat . eq random(N) = ((104 * N) + 7921) rem 10609 . *** Obeys Knuths criteria for a "good" random function *** The seed may be modified by applying the random function many times: op repeatRandom : Nat Nat -> Nat . *** repeatRandom(seed, noOfReps) eq repeatRandom(N, s N') = repeatRandom(random(N), N') . eq repeatRandom(N, 0) = N . endom) *** The next module defines the behavior of a RandomNGen object in time. *** There are possibilities to let the seed also be changed *** by time, but we skip it so far. *** Furthermore, I assume that we needn't worry about this object's subclasses. (tomod TIMED-RANDOM is protecting RANDOM . including TIMED-OO-SYSTEM . var Q : Oid . var R : Time . eq delta(< Q : RandomNGen | >, R) = < Q : RandomNGen | > . eq mte(< Q : RandomNGen | >) = INF . endtom)