*** 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)