load test0-ether.m
load model-checker
load ../ALL/simple.m

mod MC0 is
  inc SIMPLE .
  inc TEST0-ETHER .

  op st : Configuration -> State .

  op prop1 : -> Prop .
  eq  st(C:Configuration 
         < JC : JVM | jatts:AttributeSet,
           { jconf:Configuration
             msg(JC . sam, JC . app, svcAns(sn1:String, d1:Data)) 
             msg(JC . sam, JC . app, svcAns(sn2:String, d2:Data)) } > )
      sat prop1 = true .
endm

***(

red findPath(st(eecf sjcf ljcf cjcf), prop1 ) .
reduce in MC0 : findPath(st(eecf sjcf cjcf ljcf), prop1) .
rewrites: 636 in 70ms cpu (68ms real) (9085 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver
    'lookup.register 'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply
    'ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.register
    'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply 'app.findsvc
    'csptk.findServiceReq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.lookup
    'jvm.dispatch 'xmit 'jvm.deliver 'csptk.lookupOk 'jvm.new 'csptk.newidreply
    'app.foundsvc 'cssp.svcreq 'jvm.dispatch 'xmit 'jvm.deliver 'svc.svcreq
    'jvm.dispatch 'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans 'app.findsvc
    'cssp.svcreq 'jvm.dispatch 'xmit 'jvm.deliver 'svc.svcreq 'jvm.dispatch
    'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans, st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := proxyD(CP0, svc(JS . GBPsvc))),
    "USquote" := proxyD(CP0, svc(JS . USsvc))) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CP0 | idle,svc(JS . GBPsvc),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(GBPdata, mycall, "sam"))) 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(update(GBPdata, mycall,
    "sam"), badcall, "sam")))},ether(eee) >))

======================================================================
red findPath(st(eacf sjcf ljcf cjcf), prop1) .
reduce in MC0 : findPath(st(eacf sjcf cjcf ljcf), prop1) .
rewrites: 585 in 30ms cpu (28ms real) (19500 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.dispatch 'attack.registerReq
    'jvm.deliver 'ssptk.regreply 'ssptk.regreq 'jvm.dispatch
    'attack.registerReq 'jvm.deliver 'ssptk.regreply 'app.findsvc
    'csptk.findServiceReq 'jvm.dispatch 'attack.lookupReq 'jvm.deliver
    'csptk.lookupOk 'jvm.new 'csptk.newidreply 'app.foundsvc 'cssp.svcreq
    'jvm.dispatch 'attack.svcReq 'jvm.deliver 'svc.svcreq 'jvm.dispatch
    'attack.svcReply 'jvm.deliver 'cssp.svcreply 'app.svcans 'app.findsvc
    'cssp.svcreq 'jvm.dispatch 'attack.svcReq 'jvm.deliver 'svc.svcreq
    'jvm.dispatch 'attack.svcReply 'jvm.deliver 'cssp.svcreply 'app.svcans, st(
< eee : Attacker | inQ(none),outQ(none),clientIds("sam"),clientDs(mycall
    badcall reply(GBPdata, mycall, "sam") reply(update(GBPdata, mycall, "sam"),
    mycall, "sam")),pxDs(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0, svc(JS .
    USsvc))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), mycall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CP0 | idle,svc(JS . GBPsvc),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", mycall)) 
msg(JC . sam, JC . app, svcAns("GBPquote", mycall))},ether(eee) >))

*** red findPath(st(eecf sjcf ljcf cjcf ajcf), prop1) .

*** red findPath(st(eacf sjcf ljcf cjcf ajcf), prop1) .

)