****** 03mar02

rewrite in TEST0-ETHER : eecf sjcf cjcf ljcf .
rewrites: 328 in 30ms cpu (25ms real) (10933 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := proxyD(CSP0, svc(JS . o(0)))),
    "USquote" := proxyD(CSP0, svc(JS . o(1)))) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< 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),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, reply(update(GBPdata, mycall, "sam"), badcall,
    "sam"))) > 
< JC . o(0) : CSP0 | idle,svc(JS . o(0)),clientId("sam") >},ether(eee) >


rewrite in TEST0-ETHER : eecf sjcf ljcf ajcf cjcf .
rewrites: 620 in 50ms cpu (50ms real) (12400 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := proxyD(CSP0, svc(JS . o(0)))),
    "USquote" := proxyD(CSP0, svc(JS . o(1)))) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(update(GBPdata, mycall, "sam"),
    badcall, "sam"), fakeCall, fakeId)) > 
< JS . USsvc : SVC | state(update(USdata, fakeCall, 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),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, reply(update(GBPdata, mycall, "sam"), badcall,
    "sam"))) > 
< JC . o(0) : CSP0 | idle,svc(JS . o(0)),clientId("sam") >},ether(eee) > 
< JA : JVM | oCtr(2),
 {
< JA . csptk : CSPTK0 | idle,lookup(JL . lup),clientId(fakeId) > 
< JA . app : APP | idle,svcFound(b("GBPquote", JA . o(0)) b("USquote", JA . o(
    1))),mytk(JA . csptk),todo(none),done(result("GBPquote", fakeCall, reply(
    update(update(GBPdata, mycall, "sam"), badcall, "sam"), fakeCall, fakeId))
    result("USquote", fakeCall, reply(USdata, fakeCall, fakeId))) > 
< JA . o(0) : CSP0 | idle,svc(JS . o(0)),clientId(fakeId) > 
< JA . o(1) : CSP0 | idle,svc(JS . o(1)),clientId(fakeId) >},ether(eee) >

rewrite in TEST0-ETHER : eacf sjcf cjcf ljcf .
rewrites: 358 in 30ms cpu (24ms real) (11933 rewrites/second)
result OConf: 
< eee : Attacker | inQ(none),outQ(none),clientIds("sam"),clientDs(mycall
    badcall reply(GBPdata, mycall, "sam") reply(update(GBPdata, mycall, "sam"),
    mycall, "sam")),pxDs(proxyD(CSP0, svc(JS . o(0))) proxyD(CSP0, svc(JS . o(
    1)))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), mycall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< 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),
    todo(none),done(result("GBPquote", mycall, mycall) result("GBPquote",
    badcall, mycall)) > 
< JC . o(0) : CSP0 | idle,svc(JS . o(0)),clientId("sam") >},ether(eee) >