type Message is MessageConstructors
   sorts MesFrame
   opns
 _==_ : Message2, Message2 -> Bool
 _<>_ : Message2, Message2 -> Bool

 consm (*! constructor *) : Message2, Nat, Bool -> MesFrame
 mes   : MesFrame -> Message2
 id    : MesFrame -> Nat
 UrlCapable : MesFrame -> Bool

   eqns forall   m,m1,m2: Message2, n:Nat, b:Bool

    ofsort Message2
       mes(consm(m,n,b)) = m
    ofsort Nat
       id(consm(m,n,b)) = n
    ofsort Bool
       UrlCapable(consm(m,n,b)) = b;
       DMInitRequest == DMInitRequest = true;
       DMInitReply == DMInitReply = true;
       DMInitReply == DMInitRequest = false;
       DMInitRequest == DMInitReply = false;
       m1 <> m2 = not(m1 == m2)
endtype

type MessageList is Message
  sorts Buffer
  opns
emptyb  (*! constructor *) : -> Buffer
addb    (*! constructor *) : MesFrame, Buffer -> Buffer
headb   : Buffer -> MesFrame
tailb   : Buffer -> Buffer

  eqns forall   l : Buffer,
            e : MesFrame

   ofsort MesFrame
      headb(addb(e,l))  = e

   ofsort Buffer
      tailb(emptyb)     = emptyb;
      tailb(addb(e,l))  = l

endtype

type EnrichedMessageList is MessageList
   opns
 append: MesFrame, Buffer -> Buffer
 length: Buffer -> Nat
 MaxBuf: -> Nat
   eqns forall m,m1,m2: MesFrame, buf:Buffer
    ofsort Buffer
       append(m,emptyb) = addb(m,emptyb);
       append(m1,addb(m2,buf)) = addb(m2,append(m1,buf))
    ofsort Nat
       length(emptyb) = 0;
       length(addb(m,buf))= 1 + length(buf);
       MaxBuf = 1
endtype

process MS[ gUpDown, gBusReset, gin, gout ]
        ( Id: Nat ) 
  : noexit :=

  MSDown[gUpDown,gBusReset,gin,gout](Id)

where

  process MSDown[ gUpDown, gBusReset, gin, gout ]
          ( Id: Nat ) 
    : noexit :=

    FlushBusReset[gBusReset]
    [> ( gUpDown ! Id ! power_change
         ; MsUp[gUpDown,gBusReset,gin,gout](Id,emptyb) )

  endproc (* MSDown *)

  process MSUp[ gUpDown, gBusReset, gin, gout ]
          ( Id: Nat, buf: Buffer ) 
    : noexit :=

    MSSuspend[gUpDown,gBusReset,gin,gout](Id,buf)
    [> gUpDown ! Id ! power_change
         ; MSDown[gUpDown,gBusReset,gin,gout](Id)

    where

    process MSSuspend[ gUpDown, gBusReset, gin, gout ]
            ( Id: Nat, buf: Buffer ) 
      : noexit :=

      ( gin ! Id ! empty
        ; MSSuspend[gUpDown,gBusReset,gin,gout] (Id,emptyb) )
      []
      ( [length(buf)>0]
         -> ( gout ! Id ! headb(buf)
              ; MSSuspend[gUpDown,gBusReset,gin,gout] (Id,tailb(buf)) ) )
      []
      ( choice b1,b2:Bool
        [] (gBusReset ! bus_reset_end ! consnet(consn(b1),consn(b2))
            ; MSReady[gUpDown,gBusReset,gin,gout](Id,buf)) )

    endproc (* MSSuspend *)

    process MSReady[ gUpDown, gBusReset, gin, gout ]
            ( Id: Nat, buf: Buffer ) 
      : noexit :=

      ( [length(buf)<maxBuf]
        -> ( choice m:Message2,j:Nat,b:Bool
             [] gin ! Id ! consm(m,j,b)
                ; MSReady[gUpDown,gBusReset,gin,gout]
                  (Id,append(consm(m,j,b),buf)) ) )
      []
      ( gin ! Id ! empty
        ; MSReady[gUpDown,gBusReset,gin,gout] (Id,emptyb) )
      []
      ( [length(buf)>0]
        -> ( gout ! Id ! headb(buf)
             ; MSReady[gUpDown,gBusReset,gin,gout] (Id,tailb(buf)) ) )
      []
      ( gBusReset ! bus_reset_start
        ; MSSuspend[gUpDown,gBusReset,gin,gout](Id,buf) )
    endproc (* MSReady *)

  endproc (* MSUp *)

endproc (* MS *)