*** Real-Time Maude 2.1 specification of "application level" for
*** AER/NCA protocol suite, in particular for the RS component.
*** By Peter Csaba Olveczky


*** This file defines the  application level, ie. the user-level
*** sender and receiver application. The sender application 
*** intends to use the AER/NCA protocol to transmit data blocks to 
*** the receiver application objects.

*** These application objects do very
*** simple things, but should be present for testing purposes.

(tomod AER-APPLICATIONS is
  including AER-RS .

  class SenderApplication | dataBlocksToBeSent : MsgList .

  *** For the sake of simplicity, I assume that all the data blocks 
  *** that the sender application wants to send, is in the dataBlocksToBeSent
  *** attribute, possibly (i.e., preferrably) with various delays.

  vars Q Q' : Oid .
  vars ML ML' : MsgList .
  var MC : MsgConfiguration .
  var R : Time .
  vars M M' : Msg .
  var CF : Configuration .

  rl [appSend] :
     < Q : SenderApplication | dataBlocksToBeSent : dly(M, 0) + ML > 
     =>
       < Q : SenderApplication | dataBlocksToBeSent : ML > M .

  *** For timing purposes, I assume that this class will have no subclasses:

  eq mte(< Q : SenderApplication | dataBlocksToBeSent : ML >) = leastDly(ML) .
  eq delta(< Q : SenderApplication | dataBlocksToBeSent : ML >, R) =
        < Q : SenderApplication | dataBlocksToBeSent : ML minus R > .

  class RecvrApplication | receiver : Oid, dataRead : MsgConfiguration .

  rl [appRecv] :
     toApplication(Q, M) 
     < Q' : RecvrApplication | receiver : Q, dataRead : MC >
     =>
       < Q' : RecvrApplication | receiver : Q, dataRead : MC cat M > .

  *** Again, I assume that this class has no subclasses:
  eq mte(< Q : RecvrApplication | >) = INF .
  eq delta(< Q : RecvrApplication | >, R) = < Q : RecvrApplication | > .
endtom)