*** mobile-maude.fm
*** January 3, 2000
***
*** Mobile Maude
***
*** There is something that still worries me.
*** I suspect that the do-something rule is still being applied when
*** there is no rule to be applied, what makes the objects to
*** loose gas doing nothing. I guest that the specification works
*** because the amount of gas given to the objects is high (100) and
*** because the do-something rule is late in the spec.
*** I'll try to continue studying it.
*** I believe that the problem comes from the fact that there are
*** hidden-gas attributes in the objects in the configuration trying to
*** be rewritten.
(omod OID is
pr MACHINE-INT .
pr QID .
sorts Loc Pid Mid .
subsorts Loc Pid Mid < Oid . *** Loc are location Oids
*** move-down can only be defined on terms of a particular form.
*** We must assume that location ids are Qids or MachineInts, since
*** these are the only ones for which move-down can be defined.
*** I'm assuming here that they are Qids.
*** Of course any operator of sort Loc could be defined if the
*** appropriate equations for moving it up and down are added.
subsort Qid < Loc .
op p : Loc MachineInt -> Pid . *** Process Oid
op o : Pid MachineInt -> Mid . *** Mobile-Object Oid
endom)
(fmod LIST[X :: TRIV] is
sort List[X] .
subsort Elt.X < List[X] .
op nil : -> List[X] .
op __ : List[X] List[X] -> List[X] [assoc id: nil] .
endfm)
(fmod SET[X :: TRIV] is
sorts Set[X] .
subsorts Elt.X < Set[X] .
op mt : -> Set[X] .
op __ : Set[X] Set[X] -> Set[X] [assoc comm id: mt] .
op _in_ : Elt.X Set[X] -> Bool .
vars E E' : Elt.X .
var S : Set[X] .
eq E E = E .
eq E in mt = false .
eq E in (E' S) = E == E' or (E in S) .
endfm)
(fmod DEFAULT[X :: TRIV] is
sort Default[X] .
subsort Elt.X < Default[X] .
op null : -> Default[X] .
endfm)
(fth FUNCTION is
sorts Domain Codomain .
op f : Domain -> Codomain .
endfth)
(view Domain from TRIV to FUNCTION is
sort Elt to Domain .
endv)
(view Codomain from TRIV to FUNCTION is
sort Elt to Codomain .
endv)
(fmod MAP[F :: FUNCTION] is
protecting (SET[Domain] * (op __ to _;_))[F] .
protecting SET[Codomain][F] .
op map : Set[Domain][F] -> Set[Codomain][F] .
var A : Domain.F .
var S : Set[Domain][F] .
eq map(mt) = mt .
eq map(A ; S) = f(A) map(S) .
endfm)
(fmod PFUN[U :: TRIV, V :: TRIV] is
*** PFUN has been changed with respect to the previous version.
*** In the current version the second element of a pair cannot
*** be null.
protecting TUPLE(2)[U, V] .
*** protecting SET[Tuple[U, V]] not supported.
*** We would like to be able to write
*** pr SET[Tuple[U, V]] * (sort Set[Tuple[U, V]] to TupleSet[U, V]) .
sorts TupleSet[U, V] .
subsorts Tuple[U, V] < TupleSet[U, V] .
op mt : -> TupleSet[U, V] .
op __ : TupleSet[U, V] TupleSet[U, V] -> TupleSet[U, V]
[assoc comm id: mt] .
op _in_ : Tuple[U, V] TupleSet[U, V] -> Bool .
vars E E' : Tuple[U, V] .
var S : TupleSet[U, V] .
eq E E = E .
eq E in mt = false .
eq E in (E' S) = (E == E') or (E in S) .
*** We would like to be able to write
***
*** pr MAP[view to TUPLE(2)[U, V] is
*** sort Domain to Tuple[U, V] .
*** sort Codomain to Elt.U .
*** op f to p1 .
*** endv]
*** * (sort Set[Domain][U] to TupleSet[U, V],
*** sort Set[Codomain][V] to Set[U],
*** op map to dom) .
***
*** and
***
*** pr MAP[view to TUPLE(2)[U, V] is
*** sort Domain to Tuple[U, V] .
*** sort Codomain to V .
*** op f to p2 .
*** endv]
*** * (sort Set[Domain][U] to TupleSet[U, V],
*** sort Set[Codomain][V] to Set[V],
*** op map to im) .
***
protecting SET[U] .
protecting SET[V] .
protecting DEFAULT[V] .
sort PFun[U, V] .
subsorts Tuple[U, V] < PFun[U, V] < TupleSet[U, V] .
op _`[_`] : PFun[U, V] Elt.U -> Default[V] .
op _`[_->_`] : PFun[U, V] Elt.U Elt.V -> PFun[U, V] .
vars C : Elt.V .
var F : PFun[U, V] .
op dom : TupleSet[U, V] -> Set[U] . *** domain
eq dom(mt) = mt .
eq dom((A, B) S) = A dom(S) .
op im : TupleSet[U, V] -> Set[V] . *** image
eq im(mt) = mt .
eq im((A, B) S) = B im(S) .
vars A D : Elt.U .
var B : Elt.V .
mb (mt).TupleSet`[U`,V`] : PFun[U, V] .
cmb (A, B) F : PFun[U, V] if not A in dom(F) .
eq ((A, B) F) [ A ] = B .
ceq F [ A ]
= null
if not(A in dom(F)) .
eq ((A, B) F) [ A -> C ] = (A, C) F .
ceq F [ A -> C ]
= (A, C) F
if not(A in dom(F)) .
endfm)
(view Pid from TRIV to OID is
sort Elt to Pid .
endv)
(view Mid from TRIV to OID is
sort Elt to Mid .
endv)
(view MachineInt from TRIV to MACHINE-INT is
sort Elt to MachineInt .
endv)
(view Term from TRIV to META-LEVEL is
sort Elt to Term .
endv)
(view Tuple`[Pid`,MachineInt`]
from TRIV to TUPLE(2)[Pid, MachineInt] is
sort Elt to Tuple[Pid, MachineInt] .
endv)
(fmod MOVE-DOWN is
*** The down functions are "partial functions". We cannot define
*** a down function on any term. They are named according to the
*** sort of the term they return.
pr META-LEVEL .
pr OID .
op downTerm : Term -> Term .
op downModule : Term -> Module .
op downQid : Term -> Qid .
op downQidList : Term -> QidList .
op downQidSet : Term -> QidSet .
op downMachineInt : Term -> MachineInt .
op downQidList : TermList -> QidList .
op downQidSet : TermList -> QidSet .
op downTerm : TermList -> Term .
op downImportList : TermList -> ImportList .
op downSortDecl : Term -> SortDecl .
op downSubsortDeclSet : TermList -> SubsortDeclSet .
op downOpDeclSet : TermList -> OpDeclSet .
op downVarDeclSet : TermList -> VarDeclSet .
op downMembAxSet : TermList -> MembAxSet .
op downEquationSet : TermList -> EquationSet .
op downRuleSet : TermList -> RuleSet .
op downAttrSet : TermList -> AttrSet .
op downAttr : Term -> Attr .
op downHookList : TermList -> HookList .
op downMetaMachineInt : Term -> Term .
op downMachineInt : TermList -> MachineIntList .
vars T T' T'' T''' T1 T2 T3 T4 T5 T6 T7 T8 T9 : Term .
vars TL TL' : TermList .
vars Q Q' QI QI' F V L : Qid .
eq downModule('fmod_is_______endfm[T1, T2, T3, T4, T5, T6, T7, T8])
= fmod downQid(T1) is
downImportList(T2) downSortDecl(T3)
downSubsortDeclSet(T4) downOpDeclSet(T5)
downVarDeclSet(T6) downMembAxSet(T7) downEquationSet(T8)
endfm .
eq downModule(
'mod_is________endm[T1, T2, T3, T4, T5, T6, T7, T8, T9])
= mod downQid(T1) is
downImportList(T2) downSortDecl(T3)
downSubsortDeclSet(T4) downOpDeclSet(T5)
downVarDeclSet(T6) downMembAxSet(T7)
downEquationSet(T8) downRuleSet(T9)
endm .
eq downImportList({'nil}'ImportList) = nil .
eq downImportList('__[TL]) = downImportList(TL) .
eq downImportList((TL, TL'))
= (downImportList(TL) downImportList(TL')) .
eq downImportList('including_.[T])
= (including downQid(T) .) .
eq downSortDecl('sorts_.[T]) = (sorts downQidSet(T) .) .
eq downSubsortDeclSet({'none}'SubsortDeclSet) = none .
eq downSubsortDeclSet('__[TL]) = downSubsortDeclSet(TL) .
eq downSubsortDeclSet((TL, TL'))
= (downSubsortDeclSet(TL) downSubsortDeclSet(TL')) .
eq downSubsortDeclSet('subsort_<_.[T, T'])
= (subsort downQid(T) < downQid(T') .) .
eq downOpDeclSet({'none}'OpDeclSet) = none .
eq downOpDeclSet('__[TL]) = downOpDeclSet(TL) .
eq downOpDeclSet((TL, TL'))
= (downOpDeclSet(TL) downOpDeclSet(TL')) .
eq downOpDeclSet('op_:_->_`[_`].[{F}'Qid, T, T', T''])
= (op downQid(F) : downQidList(T) -> downQid(T')
[downAttrSet(T'')] .) .
eq downAttrSet({'none}'AttrSet) = none .
eq downAttrSet('__[TL]) = downAttrSet(TL) .
eq downAttrSet((TL, TL')) = (downAttr(TL) downAttrSet(TL')) .
ceq downAttrSet(T)
= downAttr(T)
if T =/= {'none}'AttrSet .
eq downAttr({'assoc}'Attr) = assoc .
eq downAttr({'comm}'Attr) = comm .
eq downAttr({'idem}'Attr) = idem .
eq downAttr('id[T]) = id(downTerm(T)) .
eq downAttr('left-id[T]) = left-id(downTerm(T)) .
eq downAttr('right-id[T]) = right-id(downTerm(T)) .
eq downAttr('strat[T]) = strat(downMachineInt(T)) .
eq downAttr('prec[T]) = prec(downMachineInt(T)) .
eq downAttr('gather[T]) = gather(downQidList(T)) .
eq downAttr('special[T]) = special(downHookList(T)) .
eq downHookList('__[TL]) = downHookList(TL) .
eq downHookList((TL, TL')) = downHookList(TL) downHookList(TL') .
eq downHookList('id-hook[T, T'])
= id-hook(downQid(T), downQidList(T')) .
eq downHookList('op-hook[T, T', T'', T'''])
= op-hook(downQid(T), downQid(T'),
downQidList(T''), downQid(T''')) .
eq downHookList('term-hook[T, T'])
= term-hook(downQid(T), downTerm(T')) .
eq downTerm({F}QI) = downQid(F) .
eq downTerm('`{_`}_[T, T']) = {downTerm(T)}downTerm(T') .
eq downTerm('_:_[T, T']) = downTerm(T) : downQid(T') .
eq downTerm('_::_[T, T']) = downTerm(T) :: downQid(T') .
eq downTerm('_`[_`][T, T']) = downTerm(T)[downTerm(T')] .
eq downTerm('_`,_[T, TL]) = (downTerm(T), downTerm(TL)) .
eq downTerm((T, TL)) = (downTerm(T), downTerm(TL)) .
eq downTerm(error*) = error* .
eq downVarDeclSet({'none}'VarDeclSet) = none .
eq downVarDeclSet('__[TL]) = downVarDeclSet(TL) .
eq downVarDeclSet((TL, TL'))
= (downVarDeclSet(TL) downVarDeclSet(TL')) .
eq downVarDeclSet('var_:_.[{V}'Qid, T])
= (var downQid(V) : downQid(T) .) .
eq downMembAxSet({'none}'MembAxSet) = none .
eq downMembAxSet('__[TL]) = downMembAxSet(TL) .
eq downMembAxSet((TL, TL'))
= (downMembAxSet(TL) downMembAxSet(TL')) .
eq downMembAxSet('mb_:_.[T, T'])
= (mb downTerm(T) : downQid(T') .) .
eq downMembAxSet('cmb_:_if_=_.[T, T', T'', T'''])
= (cmb downTerm(T) : downQid(T')
if downTerm(T'') = downTerm(T''') .) .
eq downEquationSet({'none}'EquationSet) = none .
eq downEquationSet('__[TL]) = downEquationSet(TL) .
eq downEquationSet((TL, TL'))
= (downEquationSet(TL) downEquationSet(TL')) .
eq downEquationSet('eq_=_.[T, T'])
= (eq downTerm(T) = downTerm(T') .) .
eq downEquationSet('ceq_=_if_=_.[T, T', T'', T'''])
= (ceq downTerm(T) = downTerm(T')
if downTerm(T'') = downTerm(T''') .) .
eq downRuleSet({'none}'RuleSet) = none .
eq downRuleSet('__[TL]) = downRuleSet(TL) .
eq downRuleSet((TL, TL')) = (downRuleSet(TL) downRuleSet(TL')) .
eq downRuleSet('rl`[_`]:_=>_.[{L}'Qid, T, T'])
= (rl [downQid(L)] : downTerm(T) => downTerm(T') .) .
eq downRuleSet('crl`[_`]:_=>_if_=_.[{L}'Qid, T, T', T'', T'''])
= (crl [downQid(L)] : downTerm(T)
=> downTerm(T') if downTerm(T'') = downTerm(T''') .) .
eq downQidSet({'none}'QidSet') = none .
eq downQidSet('_;_[TL]) = downQidSet(TL) .
eq downQidSet((TL, TL')) = (downQidSet(TL) ; downQidSet(TL')) .
eq downQidSet({QI}'Qid) = downQid(QI) .
eq downQidList({'nil}'QidList) = nil .
eq downQidList('__[TL]) = downQidList(TL) .
eq downQidList((TL, TL')) = (downQidList(TL) downQidList(TL')) .
eq downQidList({QI}'Qid) = downQid(QI) .
eq downQidList('`(_`)[{QI}'Qid]) = downQid(QI) .
eq downQid(QI) = strip(QI) .
eq downQid('`(_`)[QI]) = strip(QI) .
eq downQid({QI}QI') = strip(QI) .
eq downMetaMachineInt({QI}'Qid)
= {strip(QI)}'MachineInt .
eq downMachineInt({QI}'NzMachineInt)
= downMachineInt({QI}'MachineInt) .
eq downMachineInt({QI}'MachineInt)
= convert(QI) .
eq downMachineInt('__[TL])
= downMachineInt(TL) .
eq downMachineInt((TL, TL'))
= (downMachineInt(TL) downMachineInt(TL')) .
eq downMachineInt({'nil}'MachineIntList) = nil .
op downMid : Term -> Mid .
op downPid : Term -> Pid .
eq downMid('o[T, {Q}'MachineInt])
= o(downPid(T), convert(Q)) .
eq downMid('o[T, {Q}'NzMachineInt])
= o(downPid(T), convert(Q)) .
eq downPid('p[{Q}'Qid, {Q'}'MachineInt])
= p(strip(Q), convert(Q')) .
eq downPid('p[{Q}'Qid, {Q'}'NzMachineInt])
= p(strip(Q), convert(Q')) .
endfm)
(fmod MOVE-UP is
pr META-LEVEL .
pr OID .
op up : MachineInt -> Term .
op up : Mid -> Term .
vars N N' : MachineInt .
var Q : Qid .
eq up(N) = {index(' , N)}'MachineInt .
eq up(o(p(Q, N), N'))
= 'o['p[{conc('' , Q)}'Qid, {index(' , N)}'MachineInt],
{index(' , N')}'MachineInt] .
endfm)
(fmod GMETA-REWRITE is
pr META-LEVEL .
pr MOVE-UP .
op gmeta-rewrite : Module Term MachineInt MachineInt -> Term .
op gmeta-rewrite-aux : Module Term MachineInt MachineInt -> Term .
op initializeGas : Term -> Term .
op refill : Term MachineInt -> Term .
var M : Module .
vars T O : Term .
var TL : TermList .
vars I I' : MachineInt .
vars QI V F S : Qid .
eq gmeta-rewrite(M, T, I, I')
*** I number of refills (if 0 no limit)
*** I' amount of gas in each refill
= if I == 1
then meta-rewrite(M, refill(T, I'), 0)
else if meta-rewrite(M, refill(T, I'), 0) == refill(T, I')
then T
else gmeta-rewrite(M,
meta-rewrite(M, refill(T, I'), 0), _-_(I, 1), I')
fi
fi .
op initializeGas : TermList -> TermList .
eq initializeGas(error*) = error* .
eq initializeGas(V) = V .
eq initializeGas({F}S) = {F}S .
ceq initializeGas(F[TL])
= F[initializeGas(TL)]
if (F =/= '<_:_|_>) and (F =/= '<_:_|`>) .
eq initializeGas('<_:_|_>[O, {QI}S, T])
= '<_:_|_>[O, {QI}S,
'_`,_['hidden-gas`:_[{'0}'MachineInt], initializeGas(T)]] .
eq initializeGas('<_:_|`>[O, {QI}S])
= '<_:_|_>[O, {QI}S, 'hidden-gas`:_[{'0}'MachineInt]] .
eq initializeGas((T, TL))
= (initializeGas(T), initializeGas(TL)) .
op refill : TermList MachineInt -> TermList .
op refillAttr : Term MachineInt -> Term .
op refillAttrAux : TermList MachineInt -> TermList .
eq refill(error*, I) = error* .
eq refill(V, I) = V .
eq refill({F}S, I) = {F}S .
ceq refill(F[TL], I)
= F[refill(TL, I)]
if (F =/= '<_:_|_>) .
eq refill('<_:_|_>[O, {QI}S, T], I)
= '<_:_|_>[O, {QI}S, refillAttr(T, I)] .
eq refill((T, TL), I)
= (refill(T, I), refill(TL, I)) .
eq refillAttr('hidden-gas`:_[T], I)
= 'hidden-gas`:_[up(I)] .
*** should we add I gas or just refill up to I?
eq refillAttr('_`,_[TL], I)
= '_`,_[refillAttrAux(TL, I)] .
eq refillAttrAux(F[T], I)
= if F == 'hidden-gas`:_
then F[up(I)]
else F[refill(T, I)]
fi .
eq refillAttrAux((F[T], TL), I)
= if F == 'hidden-gas`:_
then (F[up(I)], refill(TL, I))
else (F[refill(T, I)], refill(TL, I))
fi .
endfm)
*** We assume some requirements on the modules and the states on
*** the mobile objects. Specifically, we assume an object-oriented
*** module as the module in which are contained the rules describing
*** the behavior of the mobile object and a pair with a _&_ at the
*** top, with a configuration and a set of messages as arguments
*** giving its state.
*** Messages in the configuration and in the module may be of
*** any form, but those being pulled in or out of the mobile object
*** must have a specific form. In particular, messages getting in an
*** out of the mobile object must be of the form to_:_, go, or newo.
*** The message to_:_ takes a Mid and a term of sort Contents as
*** arguments; go takes a Pid as argument, and newo takes a term
*** of sort module, a configuration, and a Mid.
*** The Mobile Maude specification assumes that any specification
*** describing the behavior of mobile objects we'll include the
*** following module MOBILE-OBJECT-ADDITIONAL-DEFS and that it
*** will satisfy the previous requirements.
(omod MOBILE-OBJECT-ADDITIONAL-DEFS is
pr META-LEVEL .
inc OID .
*** Messages being pulled in or out of a mobile object must be of the
*** form go(O), newo(Mod, Conf, O'), or (to O : C) for O and O' Mids,
*** C a term of sort Contents, Mod a term of sort Module, and Conf
*** a term of sort Configuration.
sort Contents .
op go : Oid -> Msg .
op to_:_ : Mid Contents -> Msg [gather (& &)] .
op newo : Module Configuration Oid -> Msg .
*** To be able to take messages out of the state of the mobile objects
*** there are several possibilities, for example:
*** - not distinguishing between messages sent to objects in the
*** state of the same mobile object (which do not need to be
*** taken out) and messages being sent to other objects (which
*** need to be taken out);
*** - distinguishing between them, and taking out only those being
*** sent to objects in other mobile objects, but we can still
*** have two possibilities:
*** - checking for the name of the object to which the message
*** is sent, or
*** - keeping then separated.
*** As a first attempt we are going to keep them separated. Instead
*** of having (the metarepresentation of) a configuration, we will
*** keep (the metarepresentation of) a pair _&_ of configurations (in
*** fact, a configuration and a set of messages).
*** Note that this new operator has to be declared in the module
*** stored in the mod attribute; if desired, this module could be
*** added to the module CONFIGURATION. The rules in mobile-maude.mma
*** will have to assume this operator in order to put messages inside
*** the configuration of a mobile object and to take messages out of
*** it, but operating on its metarepresentation only. The rules in
*** the module in the mobile object will have to take care of this.
*** The state of a mobile object is given by a pair C & Ms where C is
*** a configuration and Ms is a set of messages being sent out of the
*** mobile object.
sort MsgSet .
subsorts Msg < MsgSet < Configuration .
var Mg : Msg .
var MgS : MsgSet .
mb (none).Configuration : MsgSet .
mb Mg MgS : MsgSet .
sort MobObjState .
op _&_ : Configuration MsgSet -> MobObjState .
endom)
(omod MOBILE-MAUDE is
pr META-LEVEL .
pr MOVE-DOWN .
pr MOVE-UP .
pr GMETA-REWRITE . *** Temporary implementation of gmeta-rewrite.
pr OID
+ SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._)
+ TUPLE(2)[Pid, MachineInt] .
pr PFUN[MachineInt, Tuple`[Pid`,MachineInt`]]
* (op __ : Set[MachineInt] Set[MachineInt] -> Set[MachineInt]
to _#_) .
*** __ is used as constructor of MachineInt lists in META-LEVEL
pr DEFAULT[MachineInt] .
class R | *** Root Objects (one per location)
cnt : MachineInt . *** number of processes in the location
class P | *** Processes
cnt : MachineInt, *** counter to generate new mobile
*** object names
cf : Configuration, *** configuration in the process
*** (its belly)
guests : Set[Mid], *** objects in its belly
forward : PFun[MachineInt, Tuple`[Pid`,MachineInt`]] .
*** forwarding information
class MO | *** Mobile Objects
mod : Module, *** rewrite rules of the mobile object
s : Term, *** current state
p : Pid, *** current location
gas : MachineInt, *** bound on resources
hops : MachineInt, *** number of hops
mode : Mode . *** mode of the mobile object
*** (idle/active)
*** Objects in motion cannot be active
sort Mode .
ops idle active : -> Mode .
var MOM : Mode .
var L : Loc .
vars N N' N'' : MachineInt .
var C : Configuration .
vars PI PI' : Pid .
var M : Mid .
vars SMO : Set[Mid] .
var MOD : Module .
vars T T' T'' T''' T'''' : Term .
var TL : TermList .
vars Q Q' Q'' : Qid .
var F : PFun[MachineInt, Tuple`[Pid`,MachineInt`]] .
var H : Default[MachineInt] .
*** In the current version of Full Maude there are no sorts
*** classifying objects. They and the corresponding membership axioms
*** must be defined explicitly.
sort MobObject .
subsort MobObject < Object .
mb (< M : MO |
mod : MOD, s : T, p : PI, gas : N, hops : N', mode : MOM >)
: MobObject .
*** Object motion to a location.
msg go : Loc MobObject -> Msg .
*** Change of address notified by a mobile object to its "parent
*** process" by indicating the pair of the current host process and
*** the current number of hops, and indicating the mobile object's
*** identity by the last machine integer in the message.
msg to_@_`{_`} : Pid Tuple[Pid, MachineInt] MachineInt -> Msg .
*** Object motion to a process.
msg go : Pid MobObject -> Msg .
*** Mobile object creation.
msg newo : Module Term -> Msg .
*** Inter-object message in transit between processes.
*** The second argument indicates the number of hops registered for a
*** mobile object in its parent process so that the processing of
*** messages addressed to in-transit objects is postponed until the
*** forwarding information corresponding to such objects is updated.
msg to_hops_in_`{_`} : Mid Default[MachineInt] Pid Term -> Msg .
*** Inter-object message inside a process configuration.
msg to_`{_`} : Mid Term -> Msg .
*** Mobile object goes to a location.
*** Note that the forwarding info is updated when the mobile object
*** arrives to its destination; meanwhile, there could be messages
*** being sent to this process, supposing that the object is in it.
rl [go-loc] :
< PI : P | cf : C go(L, < M : MO | >), guests : M . SMO >
=> < PI : P | cf : C, guests : SMO >
go(L, < M : MO | >) .
*** Object arrival to a location and creation of a new process in
*** which to place the object.
rl [arrive-loc] :
go(L, < o(PI, N) : MO | hops : N' >)
< L : R | cnt : N'' >
=> < L : R | cnt : N'' + 1 >
< p(L, N'') : P | cnt : 0,
cf : < o(PI, N) : MO | hops : N' + 1, mode : active >,
guests : o(PI, N) >
to PI @ (p(L, N''), N' + 1) { N } .
*** Parent process updates a mobile object's forwarding address.
*** We must make sure that the situation in which an object is in
*** transit is handled correctly.
*** Note that since the forwarding info is updated when the object
*** arrives to its destination process, the forwarding info is
*** not valid during the transit of the mobile objects. However,
*** since we have the guests list we still have enough info to guide
*** the messages appropriately.
rl [forwarding-update] :
to PI @ (PI', N') { N }
< PI : P | forward : F >
=> if p2(F [ N ]) < N'
then < PI : P | forward : F [ N -> (PI', N') ] >
else < PI : P | forward : F >
fi .
*** Go to a process.
rl [go-proc] :
< PI : P | cf : C go(PI', < M : MO | >), guests : M . SMO >
=> if PI =/= PI'
then < PI : P | cf : C, guests : SMO >
go(PI', < M : MO | >)
else < PI : P | cf : C < M : MO | p : PI, mode : active > >
fi .
*** Arrival at a process.
rl [arrive-proc] :
go(PI, < o(PI', N) : MO | hops : N' >)
< PI : P | cf : C, guests : SMO, forward : F >
=> if PI == PI'
then < PI : P | cf : C < o(PI', N) : MO | p : PI,
hops : N' + 1,
mode : active >,
guests : o(PI', N) . SMO,
forward : F [ N -> (PI, N' + 1) ] >
else < PI : P | cf : C < o(PI', N) : MO | p : PI,
hops : N' + 1,
mode : active >,
guests : o(PI', N) . SMO >
to PI' @ (PI, N' + 1) { N }
fi .
*** Create new object.
*** When a mobile object is created, its number of hops is set to
*** zero and the forwarding info in its parent process in initialized
*** as expected, with the process in which it's located ---the parent
*** itself--- and its number of hops ---zero.
*** Note that the gas intially given is 100. Perhaps the initial
*** amount of gas should be specified in the newo command.
rl [create-object] :
< PI : P | cf : C newo(MOD, T), cnt : N', guests : SMO >
=> < PI : P | cf : C < o(PI, N') : MO | mod : MOD,
s : T,
p : PI,
gas : 100,
mode : active,
hops : 0 >,
cnt : N' + 1,
guests : o(PI, N') . SMO,
forward : F [ N -> (PI, 0) ] > .
*** Message redirected to the right process.
*** Messages which are sent to mobile objects in a different process
*** must be appropriately redirected. Note that the condition makes
*** sure not only that the object is not in the process' belly, but
*** also that the forwarding info does not point to the process
*** itself, which would mean that the process has not arrived to its
*** destination yet. If the process in which the message is generated
*** is the parent process of the mobile object the message is
*** addressed to, then the message is forwarded to the process
*** indicated by the forwarding info with the corresponding number of
*** hops; in other case the message is forwarded to the parent
*** process with the number of hops set to null. This hops
*** information is used in the msg-arrive-to-proc rule to avoid
*** unnecessary forwarding of messages when the destination object is
*** in transit.
crl [msg-send] :
< PI : P | cf : C (to o(PI, N) { T }), guests : SMO, forward : F >
=> < PI : P | cf : C >
to o(PI, N) hops p2(F[N]) in p1(F[N]) { T }
if (not o(PI, N) in SMO) and p1(F[N]) =/= PI .
crl [msg-send] :
< PI : P | cf : C (to o(PI', N) { T }), guests : SMO, forward : F >
=> < PI : P | cf : C >
to o(PI', N) hops null in PI' { T }
if (not o(PI', N) in SMO) and PI =/= PI' .
*** Arrival of an inter-object message to a process.
*** There are four rules dealing with the different cases.
*** If the object is in the process then the message is just put
*** in the belly of the process so the object can get it.
crl [msg-arrive-to-proc] :
to o(PI, N) hops H in PI' { T' }
< PI' : P | cf : C, guests : SMO >
=> < PI' : P | cf : C (to o(PI, N) { T' }) >
if o(PI, N) in SMO .
*** If the object is not in the process and the number of hops is
*** null then the message is being sent to the mobile object's parent
*** process. If the forwarding info is pointing to the parent process
*** itself then the object is in transit and the forwarding info has
*** not been updated with its new process, so the message is not
*** handled; otherwise, the message is sent to the process indicated
*** by the forwarding info with the corresponding number of hops.
crl [msg-arrive-to-proc] :
to o(PI, N) hops null in PI { T }
< PI : P | guests : SMO, forward : F >
=> < PI : P | >
to o(PI, N) hops p2(F[N]) in p1(F[N]) { T }
if (not o(PI, N) in SMO) and (p1(F[N]) =/= PI) .
*** If the object is not in the process and the process is not the
*** parent then the message is forwarded back to the parent process
*** with the same hops number. Note that since PI =/= PI' the number
*** of hops is not null, that is, it is a machine integer.
*** Note that, since the forwarding info is updated once the object
*** has arrived to a process, it cannot be the case that the message
*** has arrived before the object. If the object to which the message
*** is addressed is not in the process registered in the forwarding
*** info it is because the object has already left the process and
*** the message must be returned to the parent process.
crl [msg-arrive-to-proc] :
to o(PI, N) hops N' in PI' { T }
< PI' : P | guests : SMO >
=> < PI' : P | >
to o(PI, N) hops N' in PI { T }
if (not o(PI, N) in SMO) and (PI =/= PI') .
*** Finally, if the message is being returned from a process to which
*** the message was forwarded from the parent process because the
*** object already left it, then the message
*** will be forwarded again by the parent process only if its
*** forwarding info has been updated since the message was forwarded
*** by the first time, that is, if the number of hops in the message
*** is smaller than the number of hops in the forwarding info in the
*** parent process.
*** Note that we don't check whether the forwarding info points to
*** the parent process itself anymore, since in this case the hops
*** would have been appropriately incremented. In the previos version
*** we had to check for this case because this would mean that the
*** object has been in it but has already left and is in transit.
crl [msg-arrive-to-proc] :
to o(PI, N) hops N' in PI { T' }
< PI : P | guests : SMO, forward : F >
=> < PI : P | >
to o(PI, N) hops p2(F[N]) in p1(F[N]) { T' }
if (not o(PI, N) in SMO) and (N' < p2(F[N])) .
*** gmeta-rewrite is not available yet.
*** It will be as meta-rewrite but will also return the amount of gas
*** not consumed in the rewriting process.
***
*** pr TUPLE(2)[Term, MachineInt] .
***
*** op gmeta-rewrite :
*** Module Term MachineInt -> Tuple[Term, MachineInt] .
***
*** rl [do-something] :
*** < M : MO | mod : MOD, s : T, gas : N >
*** => < M : MO | mod : MOD,
*** s : p1(gmeta-rewrite(MOD, T, N)),
*** gas : p2(gmeta-rewrite(MOD, T, N)) > .
*** I'm going to use the gas value
*** both as maximum number of rewrites when calling meta-rewrite and
*** as the number of times that meta-rewrite is called. Note that the
*** gas value is decremented each time meta-rewrite is called.
*** In order to make sure that no gas is consumed when an object
*** cannot do anything we check that the result of executing meta-
*** rewrite on a term is different from the original term. Note that
*** it could happen that although some rules are applied there is a
*** loop and the final term is equal to the original one.
***
*** crl [do-something] :
*** < M : MO | mod : MOD, s : T, gas : N, mode : active >
*** => < M : MO | s : meta-rewrite(MOD, T, N), gas : _-_(N, 1) >
*** if (N > 0) and (T =/= meta-rewrite(MOD, T, N)) .
*** It doesn't work just with meta-rewrite because there are
*** hidden-gas attributes in the objects in the state, which are
*** never refilled.
*** Note that gmeta-rewrite starts refilling the hidden gas in the
*** objects.
crl [do-something] :
< M : MO | mod : MOD, s : T, gas : N, mode : active >
=> < M : MO | s : meta-rewrite(MOD, refill(T, N), 1),
gas : _-_(N, 1) >
if (N > 0) and
(refill(T, N) =/= meta-rewrite(MOD, refill(T, N), 1)) .
*** note signature is not global
*** We assume some requirements on the modules and the states on the
*** mobile objects. Specifically, we assume a object-oriented module
*** as the module in which the rules describing the behavior of the
*** mobile object and a pair with a _&_ at the top, with a
*** configuration and a set of messages as arguments giving its
*** state.
*** Messages in the configuration and in the module may be of any
*** form, but those being pulled in or out of the mobile object must
*** have a specific form. In particular, messages getting in an out
*** of the mobile object must be of the form to_:_, go, or newo.
*** The message to_:_ takes a Mid and a term of sort Contents as
*** arguments; go takes a Pid as argument, and newo takes a term
*** of sort module, a configuration, and a Mid.
*** Pulling in of messages into mobile objects
*** In the previous version of Mobile Maude we were checking that the
*** term resulting from adding the message being pulled in to the
*** current configuration resulted in a configuration. To allow the
*** possibility of having a term in an error supersort which could go
*** down in a rewriting, we check not that the lest sort of the term
*** is smaller or equal than the Configuration sort, but that one is
*** smaller than the other one. Note that we could just
*** check that they are in the same component, but, since we can add
*** new sorts to this connected component complicating the sort
*** structure, this checking is, in principle, safer.
***
*** rl [message-in] :
*** to M { T }
*** < M : MO | mod : MOD, s : '_&_[T', T''] >
*** => if sortLeq(MOD,
*** leastSort(MOD, '__['to_:_[up(M), T], T']),
*** 'Configuration)
*** or
*** sortLeq(MOD,
*** 'Configuration,
*** leastSort(MOD, '__['to_:_[up(M), T], T))
*** then < M : MO | mod : MOD,
*** s : '_&_['__['to_:_[up(M), T], T'], T''] >
*** else < M : MO | mod : MOD, s : '_&_[T', T''] >
*** fi .
*** We have further simplified the checking. Instead of checking that
*** the result of introducing the current message to the
*** configuration representing the current state of the mobile object
*** is a valid configuration we just check that it is a valid message
*** in the module of the object. We can assume that, since the
*** previos state was a valid one, adding a valid message will result
*** in a new valid state.
rl [msg-in] :
to M { T }
< M : MO | mod : MOD, s : '_&_[T', T''] >
=> if sortLeq(MOD, leastSort(MOD, 'to_:_[up(M), T]), 'Msg)
or
sortLeq(MOD, 'Msg, leastSort(MOD, 'to_:_[up(M), T]))
then < M : MO | s : '_&_['__['to_:_[up(M), T], T'], T''] >
else < M : MO | s : '_&_[T', T''] >
fi .
*** Pulling out of messages from mobile objects.
*** Note that we must have three rules to deal with all the possible
*** cases. Although in general it is enough with two cases to deal
*** with associative lists (one element and more than one element),
*** at the metalevel, since the engine is giving the list in
*** flattened form and expect it in flattened form, we must make sure
*** that when we have more than one element the top operator is __.
rl [message-out-to] :
< M : MO | mod : MOD, s : '_&_[T, 'to_:_[T', T'']], mode : active >
=> < M : MO | mod : MOD, s : '_&_[T, {'none}'MsgSet] >
(to downMid(T') { T'' }) .
rl [message-out-to] :
< M : MO |
mod : MOD, s : '_&_[T, '__['to_:_[T', T''], T''']],
mode : active >
=> < M : MO | mod : MOD, s : '_&_[T, T'''] >
(to downMid(T') { T'' }) .
rl [message-out-to] :
< M : MO |
mod : MOD, s : '_&_[T, '__['to_:_[T', T''], T''', TL]],
mode : active >
=> < M : MO | mod : MOD, s : '_&_[T, '__[T''', TL]] >
(to downMid(T') { T'' }) .
*** If there is a go command inside the mobile object indicating
*** where it should move then there shouldn't be any other message.
*** Perhaps we should control this situation and act in consequence.
rl [message-out-move] :
< M : MO | s : '_&_[T, 'go[T']], mode : active >
=> go(downPid(T'),
< M : MO | s : '_&_[T, {'none}'MsgSet], mode : idle >) .
*** Pulling out a newo command (new-mobile-object message).
*** newo is defined in the MOBILE-OBJECT-ADDITIONAL-DEFS module
*** as follows:
*** op newo : Module Configuration Oid -> Msg .
*** newo takes a module (a term of sort Module metarepresenting a
*** module), a configuration (which will be the initial configuration
*** in the belly of the mobile object to create), and the provisional
*** id of the main object in the configuration given as second
*** argument. The first action accomplished by a mobile object when
*** it detects the newo command is creating a new mobile object with
*** the configuration given as second argument of the newo message in
*** it, and then sending a start-up message to the main object with
*** its new name, so it coincides with the name of the mobile object
*** it is in. Note that as for the to_:_ message we need three rules
*** to cover all the cases.
*** Before creating the mobile object we check that the initial state
*** given to the newo command as second argument together with the
*** start-up message is a valid configuration.
rl [message-out-newo] :
< PI : P |
cf : C < M : MO | s : '_&_[T, 'newo[T', T'', T''']],
mode : active >,
cnt : N,
guests : SMO,
forward : F >
=> if sortLeq(downModule(T'),
leastSort(downModule(T'),
'__[T'', 'to_:_[T''', 'start-up[up(o(PI, N))]]]),
'Configuration)
or
sortLeq(downModule(T'),
'Configuration,
leastSort(downModule(T'),
'__[T'', 'to_:_[T''', 'start-up[up(o(PI, N))]]]))
then < PI : P |
cf : C < M : MO | s : '_&_[T, {'none}'MsgSet] >
< o(PI, N) : MO | mod : downModule(T'),
s : '_&_['__[T'',
'to_:_[T''',
'start-up[up(o(PI, N))]]],
{'none}'MsgSet],
p : PI,
gas : 100,
hops : 0,
mode : active >,
cnt : N + 1,
guests : o(PI, N) . SMO,
forward : F[N -> (PI, 0)] >
else < PI : P |
cf : C < M : MO | s : '_&_[T, {'none}'MsgSet] > >
fi .
rl [message-out-newo] :
< PI : P |
cf : C < M : MO |
s : '_&_[T, '__['newo[T', T'', T'''], T'''']],
mode : active >,
cnt : N,
guests : SMO,
forward : F >
=> if sortLeq(downModule(T'),
leastSort(downModule(T'),
'__[T'', 'to_:_[T''', 'start-up[up(o(PI, N))]]]),
'Configuration)
or
sortLeq(downModule(T'),
'Configuration,
leastSort(downModule(T'),
'__[T'', 'to_:_[T''', 'start-up[up(o(PI, N))]]]))
then < PI : P |
cf : C < M : MO | s : '_&_[T, T''''] >
< o(PI, N) : MO | mod : downModule(T'),
s : '_&_['__[T'',
'to_:_[T''',
'start-up[up(o(PI, N))]]],
{'none}'MsgSet],
p : PI,
gas : 100,
hops : 0,
mode : active >,
cnt : N + 1,
guests : o(PI, N) . SMO,
forward : F[N -> (PI, 0)] >
else < PI : P | cf : C < M : MO | s : '_&_[T, T''''] > >
fi .
rl [message-out-newo] :
< PI : P |
cf : C < M : MO |
s : '_&_[T, '__['newo[T', T'', T'''], T'''', TL]],
mode : active >,
cnt : N,
guests : SMO,
forward : F >
=> if sortLeq(downModule(T'),
leastSort(downModule(T'),
'__[T'', 'to_:_[T''', 'start-up[up(o(PI, N))]]]),
'Configuration)
or
sortLeq(downModule(T'),
'Configuration,
leastSort(downModule(T'),
'__[T'', 'to_:_[T''', 'start-up[up(o(PI, N))]]]))
then < PI : P |
cf : C < M : MO | s : '_&_[T, '__[T'''', TL]] >
< o(PI, N) : MO | mod : downModule(T'),
s : '_&_['__[T'',
'to_:_[T''',
'start-up[up(o(PI, N))]]],
{'none}'MsgSet],
p : PI,
gas : 100,
hops : 0,
mode : active >,
cnt : N + 1,
guests : o(PI, N) . SMO,
forward : F[N -> (PI, 0)] >
else < PI : P |
cf : C < M : MO | s : '_&_[T, '__[T'''', TL]] > >
fi .
*** Note that:
*** - in addition to creating the mobile object with the given
*** configuration in it, we must send the start-up message to
*** initialize the main object in the configuration with the
*** name of the newly created mobile object. We must make sure
*** that the new configuration, with this message in it is a
*** valid configuration.
*** - It is necessary to consider in this rule, not only the mobile
*** object in which the new message appears, but the whole process
*** in which this object is located. This is needed to be able to
*** generate the right name for it.
*** - It is not possible to generate a newo message to be handled by
*** the generate-object rule because then the start-up message can
*** not be sent. Perhaps we could have added this message in the
*** newo message.
*** - The module given as first argument to the newo message is
*** meta-metarepresented, it was already at the metalevel when
*** it's sent by the object in the belly of the mobile object.
*** Therefore, it has to be moved down one level to be used.
endom)