*** level independent
load ../ALL/all-lookup.m
**** level specific
load sp0.m       *** CSP0 SSP0
load sptk0.m     *** CSPTK0  SSPTK0

mod TEST0-LOOKUP is
  inc TEST-LOOKUP .
  inc CSPTK0 .
  inc SSPTK0 .
  inc CSP0 .
  inc SSP0 .

  eq sptkobs = < (JS . ssptk) : SSPTK0 | lookup(JL . lup),idle >  .

  eq cptkobs = 
     < (JC . csptk) : CSPTK0 | lookup(JL . lup), clientId("sam"), idle >  .

  eq acptkobs = 
***     < (JL . csptk) : CSPTK0 | lookup(JL . lup), clientId(fakeId), idle >
     < (JL . csptk) : CSPTK0 | lookup(JL . lup), clientId("sam"), idle >
     < (JL . ssptk) : SSPTK0 | lookup(JL . lup), idle >
       msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc))
 .

endm

***(
  eq icf =  eecf aljcf sjcf cjcf .
  eq icf-a =  eecf aljcf sjcf .
  eq icf-aa =  eecf aljcf0 sjcf cjcf1 .
  eq icf1 =  eecf aljcf sjcf cjcf1 .
  eq icf2 =  eecf aljcf sjcf cjcf2 .
)
***(
rew  eecf aljcf sjcf cjcf .
rew  eecf aljcf sjcf cjcf1 .
rew  eecf aljcf sjcf cjcf2 .
rew  eecf aljcf sjcf .
rew  eecf aljcf0 sjcf cjcf1 .

)

***( 03jan1

rewrite in SPTK0-TEST : icf1 .
rewrites: 950 in 50ms cpu (51ms real) (19000 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(3),
 {
< JL . AttackSvc : SVC | state(update(attackData, mycall, "sam")) > 
< JL . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | lookup(JL . lup),clientId(fakeId),waitfor(JL . lup, JL
    . app, findServiceReq("*")) > 
< JL . app : AttackerApp | myCall(acall),myTK(JL . csptk),waitfor(JL . csptk,
    JL . app, findServiceReq("*")) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP0, svc(JS . o(0))) proxyD(CSP0,
    svc(JS . o(1)))),mySvcSet(proxyD(CSP0, svc(JL . o(0)))),attackeeSet(none),
    myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : SSP0 | idle,svc(JL . AttackSvc),sname("Attack") > 
< JL . o(1) : CSP0 | idle,svc(JS . o(0)),clientId(fakeId) > 
< JL . o(2) : CSP0 | idle,svc(JS . o(1)),clientId(fakeId) > 
msg(JL . app, JL . o(1), svcReply(reply(GBPdata, acall, fakeId))) 
msg(JL . app, JL . o(2), svcReply(reply(USdata, acall, fakeId))) 
msg(JL . lup, JL . csptk, lookupReq("*")) 
msg(JL . fred, JL . ssptk, registerReply)},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, acall, fakeId)) > 
< JS . USsvc : SVC | state(update(USdata, acall, fakeId)) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JS . o(0) : SSP0 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
< JS . o(1) : SSP0 | idle,svc(JS . USsvc),sname("USquote") > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CSP0 | idle,svc(JL . o(0)),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(attackData, mycall, "sam")))},
    ether(eee) >

)


