***                                                       cell-phone.fm
***                                                      March 14, 2000

***
*** Mobile Phones
***

loop init .

in mobile-maude.fm

(view Oid from TRIV to CONFIGURATION is
  sort Elt to Oid .
 endv)

(view Tuple`[Oid`,Oid`] from TRIV to TUPLE(2)[Oid, Oid] is
  sort Elt to Tuple[Oid, Oid] .
 endv)

(omod CAR is
  pr MOBILE-OBJECT-ADDITIONAL-DEFS .
  pr SET[Oid] * (op __ : Set[Oid] Set[Oid] -> Set[Oid] to _+_) .

  class Car | 
        base : Oid,	            *** base the car is in contact with
	phone-book : Set[Oid] .

  ops talk switch : Oid -> Contents .

  vars O O' O'' : Oid .
  var OS : Set[Oid] .
  var PI : Pid .
  var N : MachineInt .
  var C : Configuration .

  rl [move] : 
    < O : Car | > (to O : switch(o(PI, N))) C & none 
    => < O : Car | base : o(PI, N) > C & go(PI) .
  rl [talk] :
    < O : Car | > (to O : talk(O)) => < O : Car | > .
  rl [talk] :                 
    *** Arbitrarily choose a car to which to send a message.
    *** Note that the message could be sent directly to the 
    *** receiver car mobile object.
    < O : Car | base : O', phone-book : O'' + OS > C & none 
    => < O : Car | > C & (to O' : talk(O'')) .
 endom)

(omod BASE is
  pr MOBILE-OBJECT-ADDITIONAL-DEFS .
  pr SET[Oid] * (op __ : Set[Oid] Set[Oid] -> Set[Oid] to _+_) .

  class Base | 
	cars : Set[Oid], 	 *** set of cars in contact with a base
	center : Oid .

  ops talk alert switch : Oid -> Contents .
  op release_to_ : Oid Oid -> Contents .

  vars O O' O'' : Oid .
  var C : Configuration .
  var OS : Set[Oid] .

  rl [release] :
    < O : Base | cars : O' + OS > (to O : release O' to O'') C & none
    => < O : Base | cars : OS > C & (to O' : switch(O'')) .
  rl [alert] : 
    < O : Base | cars : OS > (to O : alert(O')) 
    => < O : Base | cars : O' + OS > .
  rl [talk] :
    < O : Base | cars : OS, center : O' > (to O : talk(O'')) C & none
    *** A base can receive a message from one of the cars connected 
    *** to it or from the center. Depending on whether the car to 
    *** which the message is addressed is connected to the base or 
    *** not the message is sent directly to the car itself or to 
    *** the center so it can forward it appropriately.
    => < O : Base | > C &
       if O'' in OS 
       then to O'' : talk(O'') 
       else to O' : talk(O'')
       fi .
 endom)

(omod CENTER is
  pr MOBILE-OBJECT-ADDITIONAL-DEFS .
  pr PFUN[Oid, Oid] 
     * (op __ : PFun[Oid, Oid] PFun[Oid, Oid] -> PFun[Oid, Oid] to _&_,
        op __ : Set[Oid] Set[Oid] -> Set[Oid] to _+_) .
  pr SET[Oid] * (op __ : Set[Oid] Set[Oid] -> Set[Oid] to _+_) .

  class Center | 
	control : PFun[Oid, Oid],  *** connection scheme
	bases : Set[Oid],          *** set of all bases
        cars : Set[Oid] .          *** set of all cars 

  ops talk alert : Oid -> Contents .
  op release_to_ : Oid Oid -> Contents .

  vars O O' O'' O''' : Oid .
  var C : Configuration .
  vars OS OS' : Set[Oid] .
  var PF : PFun[Oid, Oid] .

  crl [talk] :
    < O : Center | control : PF > (to O : talk(O')) C & none
    => < O : Center | > C
       & (to PF[O'] : talk(O'))
       if PF[O'] =/= null .
  crl [switch] :
    < O : Center | 
            control : PF, bases : O' + O''' + OS, cars : O'' + OS' >  
    C & none
    => < O : Center | control : PF[O'' -> O'] > C
       & (to O' : alert(O'')) (to O''' : release O'' to O') 
       if PF[O''] == O''' .
  endom)

(omod CELL-PHONES is
  inc MOBILE-MAUDE .

  op initial : -> Configuration .

  rl [initial-state] :
    initial			   *** conf. with one car and two bases
    => < 'l0 : R | cnt : 3 >
       < p('l0, 0) : P |
           cnt : 1,
           cf : < o(p('l0, 0), 0) : MO | 
                     mod : up(CENTER),
                     s : up(CENTER, 
                            < o(p('l0, 0), 0) : Center | 
                                hidden-gas : 10,
                                cars : 
                                   o(p('l0, 1), 1) + o(p('l0, 2), 1),
                                bases : 
                                   o(p('l0, 1), 0) + o(p('l0, 2), 0),
                                control : 
                                   (o(p('l0, 1), 1), o(p('l0, 1), 0)) &
                                   (o(p('l0, 2), 1), o(p('l0, 2), 0)) >
                            & none),
                     p : p('l0, 0),
                     gas : 10,
                     hops : 0,
                     mode : active >,
           guests : o(p('l0, 0), 0),
           forward : (0, (p('l0, 0), 0)) > 
       < p('l0, 1) : P |
           cnt : 2,
           cf : < o(p('l0, 1), 0) : MO | 
                     mod : up(BASE),
                     s : up(BASE, 
                            < o(p('l0, 1), 0) : Base | 
                                hidden-gas : 10,
                                cars : o(p('l0, 1), 1),
                                center : o(p('l0, 0), 0) >
                            & none),
                     p : p('l0, 1),
                     gas : 10,
                     hops : 0, 
                     mode : active >
                < o(p('l0, 1), 1) : MO | 
                     mod : up(CAR),
                     s : up(CAR, 
                            < o(p('l0, 1), 1) : Car | 
                                hidden-gas : 10,
                                base : o(p('l0, 1), 0),
                                phone-book : o(p('l0, 2), 1) >
                            & none),
                     p : p('l0, 1),
                     gas : 10,
                     hops : 0,
                     mode : active >, 
           guests : o(p('l0, 1), 0) . o(p('l0, 1), 1),
           forward : (0, (p('l0, 1), 0)) (1, (p('l0, 1), 0)) >
       < p('l0, 2) : P |
           cnt : 2,
           cf : < o(p('l0, 2), 0) : MO | 
                     mod : up(BASE),
                     s : up(BASE, 
                            < o(p('l0, 2), 0) : Base | 
                                hidden-gas : 10,
                                cars : o(p('l0, 2), 1),
                                center : o(p('l0, 0), 0) >
                            & none),
                     p : p('l0, 2),
                     gas : 10,
                     hops : 0,
                     mode : active >
                < o(p('l0, 2), 1) : MO | 
                     mod : up(CAR),
                     s : up(CAR, 
                            < o(p('l0, 2), 1) : Car | 
                                hidden-gas : 10,
                                base : o(p('l0, 2), 0),
                                phone-book : o(p('l0, 1), 1) >
                            & none),
                     p : p('l0, 2),
                     gas : 10,
                     hops : 0,
                     mode : active >,
           guests : o(p('l0, 2), 0) . o(p('l0, 2), 1),
           forward : (0, (p('l0, 2), 0)) (1, (p('l0, 2), 0)) > .

 endom)

eof

(grew [10][10] initial .)