mod TEST is
  inc JVM .
  inc SVC .
  inc TRANSMITTER .
  inc SSPTK-IFACE .
  inc CSPTK-IFACE .
  inc APP .

*** APP setup 
  ops mycall badcall fakeCall : -> Data .
*** SVC setup 
  ops GBPdata USdata attackData : -> Data .
  op fakeId : -> String .

  op initData : Data -> Data .
  eq initData(update(d:Data, cd:Data, cn:String)) = initData(d:Data) .
  eq initData(d:Data) = d:Data [owise] .

  ops eee                       *** ether id
      JL JS JC JA               *** JVM ids
      GBPsvc USsvc AttackSvc    *** service ids
      sstm cstm                 *** STM ids
      ssptk csptk               *** toolkit ids
      app                       *** app id
      lup                       *** lookup service id
      fred sam : -> Oid .       *** outside agents

*** Nodes
  ops eecf                      *** good ether
      eacf                      *** attack ether
      ajcf                      *** attack node
      sjcf                      *** server node
      cjcf0                     *** client node -- no app
      cjcf                      *** client node -- one good one bad call
      cjcf1                     *** client node -- one good call
      cjcf2                     *** client node -- good call to each service
      aljcf                     *** attack lookup node
      aljcf0                    *** attack lookup node -- no app
      ljcf                      *** lookup node
        : -> Configuration .    

  ops sptkobs cptkobs aptkobs : -> Configuration .

  ops sptkobs cptkobs acptkobs : -> Configuration .

*** Good ether 
  eq eecf =  < eee : Transmitter | outQ(none), inQ(none)  > .

*** Server node
***  eq sptkobs = < (JS . ssptk) : SSPTK0 | lookup(JL . lup),idle > .
  eq sjcf =
    < JS : JVM | oCtr(0),  ether(eee), 
      { sptkobs
       < (JS .  GBPsvc) : SVC | state(GBPdata) >
       < (JS .  USsvc) : SVC | state(USdata) >
       msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc))
       msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))
      } > .

*** Client node construction
*** eq cptkobs = 
***     < (JC . csptk) : CSPTK0 | lookup(JL . lup), clientId("sam"), idle >
  op mkcjcf : Tasks -> Configuration .
  eq mkcjcf(ts:Tasks) = 
    < JC : JVM | oCtr(0),  ether(eee), 
     {  cptkobs
       < (JC . app) : APP | svcFound(none), mytk(JC . csptk), 
                            todo(ts:Tasks), done(none), idle >
      } > 
  .


  eq cjcf = mkcjcf(task("GBPquote", mycall) task("GBPquote", badcall)) .
  eq cjcf0 = mkcjcf(none) .
  eq cjcf1 = mkcjcf(task("GBPquote", mycall)) .
  eq cjcf2 = mkcjcf(task("GBPquote", mycall) task("USquote", mycall)) .

endm


