

fmod SSPTK0-CLASS is
  inc SSPTK-IFACE .
  inc SPTK-CLASS .     *** the shared lookup attribute
  inc CSP0-CLASS .   *** to create description of CSP0
  inc SSP0-CLASS .   *** to create an instance of SSP0
  op SSPTK0 : -> Cid .
endfm

mod SSPTK0 is
  inc SSPTK0-CLASS .

  rl[ssptk.regreq]:
  < O:Oid : SSPTK0 | lookup(L:Oid), idle >
  msg(O:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid))
   => 
  < O:Oid : SSPTK0 | lookup(L:Oid),
                     waitfor(myJVM, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(myJVM, O:Oid, newIdReq)
.

 rl[ssptk.sapId]:
  < O:Oid : SSPTK0 | lookup(L:Oid),
                     waitfor(myJVM, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(O:Oid, myJVM, newIdReply(N:Oid))
  => 
  < O:Oid : SSPTK0 | lookup(L:Oid),
                     waitfor(L:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  < N:Oid : SSP0 | svc(sid:Oid), sname(sn:String), idle >
  msg(L:Oid, O:Oid, registerReq(sn:String, proxyD(CSP0, svc(N:Oid))))
 .

  rl[ssptk.regreply]:
    < O:Oid : SSPTK0 | lookup(L:Oid),
                 waitfor(L:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
    msg(O:Oid, L:Oid, r:MsgBody)
  =>
   < O:Oid : SSPTK0 | lookup(L:Oid),  idle >
   msg(S:Oid, O:Oid, r:MsgBody) 
  .

endm

