*** SSP CSP
***load sp1.m
**** client and server secure proxies


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


mod SSP1 is
  inc SSP1-CLASS .

  rl[sssp.svcreq]:
    < O:Oid : SSP1 | svc(S:Oid), sname(sn:String), idle >
    smsg(O:Oid, C:Oid,  svcReq(d:Data,id:String))
     =>
    < O:Oid : SSP1 | 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 : SSP1 | svc(S:Oid), sname(sn:String),
                     waitfor(S:Oid, C:Oid, svcReq(dreq:Data)) >
    msg(O:Oid, S:Oid, svcReply(dreply:Data))
     =>
    < O:Oid : SSP1 | svc(S:Oid), sname(sn:String), idle > 
    smsg(C:Oid, O:Oid, svcReply(dreply:Data))
  .
endm

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

mod CSP1 is
  inc CSP1-CLASS .

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

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