**** distiributed object model

fmod CONFIG is
  sorts Attribute AttributeSet .
  subsort Attribute < AttributeSet .
  op none : -> AttributeSet .
  op _,_ : AttributeSet AttributeSet -> AttributeSet 
             [ctor assoc comm id: none] .
  sorts Oid Cid Object Msg .
  sorts EmptyConf OConf MConf Configuration .
  subsorts EmptyConf < OConf MConf .
  subsorts Object < OConf < Configuration .
  subsorts Msg < MConf < Configuration .
  op <_:_|_> : Oid Cid AttributeSet -> Object [format (n d d d d d d d)] .
  op none : -> EmptyConf .
  op __ : Configuration Configuration -> Configuration 
          [ctor assoc comm id: none] .
  op __ : EmptyConf EmptyConf -> EmptyConf  [ditto] .
  op __ : OConf OConf -> OConf  [ditto] .
  op __ : MConf MConf -> MConf  [ditto] .

endfm


fmod DATA is
  sorts Data DataX .
  subsort  Data < DataX .
  op badData : -> DataX .

endfm

*** specialize CONFIG to rmi and secure channel messages
*** rmi modelled by request/reply message contents

fmod JCONF is
  inc CONFIG .
  inc NAT .
***  inc QID .
***  inc DATA .

*** located Ids  Each JVM has a name and generates its own object ids
  op o : Nat -> Oid .  
  op _._ : Oid Oid -> Oid .

  sort MsgBody . 


*** Abstracting away the secure session setup. 
*** Two kinds of message for client/server objects : plain and secure
*** plain messages can be seen / modified (in the ether) by anyone
*** secure messages can only be seen / delivered to the intended target
*** One kind of message for communication between JVM -- delivery request

  ops msg smsg  : Oid Oid MsgBody -> Msg   [format (n d)] .
  op  deliver : Oid Msg -> Msg .

*** Determining the location of an object from its oid.
  op  loctgt : Msg -> [Oid] .
  op  loctgt : Oid -> [Oid] .
  eq  loctgt(msg(tgt:Oid, s:Oid, mb:MsgBody)) = loctgt(tgt:Oid) .
  eq  loctgt(smsg(tgt:Oid, s:Oid, mb:MsgBody)) = loctgt(tgt:Oid) .
  eq  loctgt(j:Oid . o:Oid) = j:Oid .


*** implement RMI  blocking by a waitfor attribute
  op idle : -> Attribute .
  op waitfor : Oid Oid MsgBody -> Attribute .
  op waitfor : Oid  -> Attribute .

endfm

*** proxy description 
fmod PROXY-DESCRIPTION is
  inc CONFIG .
  inc DATA .
  op proxyD : Cid AttributeSet -> Data .
  op isProxyDX : Data -> [Bool] .
  op isProxyD : Data -> Bool .
  eq isProxyDX(proxyD(cl:Cid, atts:AttributeSet)) = true .
  eq isProxyD(d:Data) = isProxyDX(d:Data) :: Bool .
endfm

*** abstract class modeling the communication medium

fmod ETHER-CLASS is
  inc JCONF .
  sort EtherCid .
  subsort EtherCid < Cid .
  ops inQ outQ : MConf -> Attribute .
endfm

*** implementation of ETHER that just transmits messages 

mod TRANSMITTER is
  inc ETHER-CLASS .
  op Transmitter : -> EtherCid .

  rl[xmit]:
    < T:Oid : Transmitter | inQ(deliver(J:Oid, rmsg:Msg) imc:MConf), 
                            outQ(omc:MConf) >
    =>
    < T:Oid : Transmitter | inQ(imc:MConf), 
                            outQ(deliver(J:Oid, rmsg:Msg) omc:MConf) >
  .
endm



*** JVM object class representing running JVM
*** holds object conf and messages as soup
*** manages id generation using oid counter


fmod JVM-IFACE is
  inc JCONF .
  op myJVM : -> Oid .                *** used to refer to enclosing JVM
  op newIdReq : -> MsgBody .
  op newIdReply : Oid  -> MsgBody .
endfm

fmod JVM-CLASS is
  inc JVM-IFACE .
  op JVM : -> Cid .
  op oCtr : Nat -> Attribute .
  op `{_`} : Configuration -> Attribute [format (ns d d d)] .
  op ether : Oid -> Attribute .
endfm

mod JVM is
  inc JVM-CLASS .
  inc ETHER-CLASS .

  rl[jvm.new]:
    < J:Oid : JVM | oCtr(oc:Nat), ether(e:Oid),
                    {msg(myJVM, O:Oid, newIdReq) c:Configuration} >
  =>
    < J:Oid : JVM | oCtr(s(oc:Nat)), ether(e:Oid),
       {msg(O:Oid, myJVM, newIdReply(J:Oid . o(oc:Nat))) c:Configuration } >
  .

  rl[jvm.deliver]:
    < J:Oid : JVM | oCtr(oc:Nat), ether(e:Oid), {c:Configuration} > 
    < e:Oid : ec:EtherCid | atts:AttributeSet, 
                            outQ(deliver(J:Oid, rmsg:Msg) mc:MConf) >
  =>
    < J:Oid : JVM | oCtr(oc:Nat),  ether(e:Oid),  {c:Configuration rmsg:Msg} > 
    < e:Oid : ec:EtherCid | atts:AttributeSet, outQ(mc:MConf) >
  .

  crl[jvm.dispatch]:
    < J:Oid : JVM | oCtr(oc:Nat),  ether(e:Oid), {c:Configuration rmsg:Msg} >
    < e:Oid : ec:EtherCid | atts:AttributeSet, inQ(mc:MConf) >
  =>
    < J:Oid : JVM | oCtr(oc:Nat),  ether(e:Oid),  {c:Configuration} >
    < e:Oid : ec:EtherCid | atts:AttributeSet, 
                      inQ(deliver(J':Oid, rmsg:Msg) mc:MConf) >
    if J':Oid := loctgt(rmsg:Msg) /\ J':Oid =/= J:Oid 
  .
endm
