************* svc.m  abstraction of generic service ********

fmod SVC-IFACE is
  inc JCONF .
  inc DATA .
  inc STRING .
  op svcReq : Data String -> MsgBody .
  op svcReply : DataX -> MsgBody .
endfm


fmod SVC-CLASS is
  inc SVC-IFACE .
  op state : Data -> Attribute .
  op SVC : -> Cid .
endfm

mod SVC is
  inc SVC-CLASS .
  op update : Data Data String -> Data .
  op reply : Data Data String -> Data .

  rl[svc.svcreq]:
  < svc:Oid : SVC | state(d:Data) >
  msg(svc:Oid, C:Oid, svcReq(dreq:Data,id:String))
  => 
  < svc:Oid : SVC | state(update(d:Data,dreq:Data,id:String)) >
  msg(C:Oid, svc:Oid, svcReply(reply(d:Data,dreq:Data,id:String))) .
endm


