******Generic Application

fmod APP-IFACE is
  inc CSPTK-IFACE .
  inc SVC-IFACE .
  inc SP-IFACE .
endfm


fmod APP-CLASS is
  inc APP-IFACE .
  op APP : -> Cid .

  sorts Map Bnd .
  subsort Bnd < Map .
  op b : String Oid -> Bnd .
  op none : -> Map .
  op __ : Map Map -> Map [assoc comm id: none] .

  sort Oid? .
  subsort Oid < Oid? .
  op noOid : -> Oid? .
  op lookup : Map String -> Oid? .
  eq lookup(none, s:String)= noOid .
  eq lookup((b(ss:String,o:Oid) m:Map), s:String) = 
      (if (ss:String == s:String)
       then o:Oid
       else lookup(m:Map, s:String)
       fi)
  .

  sorts Task Result Tasks Results .
  subsort Task < Tasks .
  op task : String Data -> Task .
  op none : -> Tasks .
  op __ : Tasks Tasks -> Tasks [assoc id: none] .

  subsort Result < Results .
  op result : String Data DataX -> Result .
  op none : -> Results .
  op __ : Results Results -> Results [assoc id: none] .
  op noService : -> DataX .  

  op svcFound : Map -> Attribute .
  op mytk : Oid -> Attribute .
  op todo : Tasks -> Attribute .
  op done : Results -> Attribute .
  
endfm

mod APP is
  inc APP-CLASS .

  crl[app.nexttask]:
    < A:Oid : APP | svcFound(sm:Map), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    idle >
      => 
  ( if (sid:Oid? == noOid)
    then
      ( < A:Oid : APP | svcFound(sm:Map), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    waitfor(S:Oid)  >
          msg(S:Oid, A:Oid, findServiceReq(sn:String)))
    else
      ( < A:Oid : APP | svcFound(sm:Map), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    waitfor(sid:Oid?) >
       msg(sid:Oid?, A:Oid, svcReq(d:Data)) )
    fi )
  if   sid:Oid? := lookup(sm:Map,sn:String) 
  .

  rl[app.foundsvc]:
    < A:Oid : APP | svcFound(sm:Map), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    waitfor(S:Oid)  >
    msg(A:Oid, S:Oid, findServiceOk(sn:String, C:Oid))
      =>
    < A:Oid : APP | svcFound(sm:Map b(sn:String,C:Oid)), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    waitfor(C:Oid) >
    msg(C:Oid, A:Oid, svcReq(d:Data))
   .

  rl[app.findfailed]:
    < A:Oid : APP | svcFound(sm:Map), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    waitfor(S:Oid) >
       msg(A:Oid, S:Oid, findServiceFailed(sn:String)) 
     =>
    < A:Oid : APP | svcFound(sm:Map), mytk(S:Oid),
                    todo(ts:Tasks), 
                    done(rs:Results result(sn:String, d:Data, noService) ),
                    idle >
  .

  rl[app.svcans]:
    < A:Oid : APP | svcFound(b(sn:String, sid:Oid) sm:Map), mytk(S:Oid), 
                    todo(task(sn:String, d:Data) ts:Tasks), done(rs:Results),
                    waitfor(sid:Oid)  >
    msg(A:Oid, sid:Oid, svcReply(ans:DataX))
     =>
    < A:Oid : APP | svcFound(b(sn:String, sid:Oid) sm:Map), mytk(S:Oid), 
                    todo(ts:Tasks), 
                    done(rs:Results result(sn:String, d:Data, ans:DataX)),
                    idle >

 .

endm


