*** SSP CSP
***load new-sp0.m
**** client and server naive proxies


fmod SSP0-CLASS is
  inc SP-CLASS .
  op SSP0  : -> Cid .
endfm


mod SSP0 is
  inc SSP0-CLASS .

  rl[sssp.svcreq]:
    < O:Oid : SSP0 | svc(S:Oid), sname(sn:String), idle >
    msg(O:Oid, C:Oid,  svcReq(d:Data,id:String))
     =>
    < O:Oid : SSP0 | svc(S:Oid), sname(sn:String),
                     waitfor(S:Oid, C:Oid, svcReq(d:Data)) >
    msg(S:Oid, O:Oid, svcReq(d:Data,id:String)) 
  .

  rl[sssp.reply]:
    < O:Oid : SSP0 | svc(S:Oid), sname(sn:String),
                     waitfor(S:Oid, C:Oid, svcReq(dreq:Data)) >
    msg(O:Oid, S:Oid, svcReply(dreply:DataX))
     =>
    < O:Oid : SSP0 | svc(S:Oid), sname(sn:String), idle > 
    msg(C:Oid, O:Oid, svcReply(dreply:DataX))
  .
endm

fmod CSP0-CLASS is
  inc SP-CLASS .
  op CSP0 : -> Cid .
endfm

mod CSP0 is
  inc CSP0-CLASS .

  rl[cssp.svcreq]:
    < O:Oid : CSP0 | svc(S:Oid), clientId(cn:String), atts:AttributeSet, idle >
    msg(O:Oid, A:Oid, svcReq(d:Data))
     =>
    < O:Oid : CSP0 | svc(S:Oid),  clientId(cn:String),  atts:AttributeSet, 
                     waitfor(S:Oid, A:Oid, svcReq(d:Data)) >
    msg(S:Oid, O:Oid, svcReq(d:Data,cn:String))
  .

  rl[cssp.svcreply]:
    < O:Oid : CSP0 | svc(S:Oid), clientId(cn:String),  atts:AttributeSet, 
                     waitfor(S:Oid, A:Oid, svcReq(dreq:Data)) >
    msg(O:Oid, S:Oid, svcReply(dreply:DataX))
     =>
    < O:Oid : CSP0 | svc(S:Oid), clientId(cn:String), atts:AttributeSet, idle >
    msg(A:Oid, O:Oid, svcReply(dreply:DataX))
  .
endm

