mod ROVER is
  inc DEVICE .
  inc PHCONTROLLER-PHACTUATOR-INTERFACE .
  inc ROVER-PHACTUATOR-INTERFACE .
  inc ROVER-PHSENSOR-INTERFACE .
  inc GRID .

  sort RoverCid .
  subsort RoverCid < DeviceCid .
  
  *** Attributes
  op grid : Nat Nat LocSet -> Attribute .
            *** Dimension of Grid:  ht  wd  blocked
  op pos_  : Loc -> Attribute .
  op hd : Nat -> Attribute .     *** degrees clockwise from grid north
  sort Status .
  ops driving turning idle : -> Status .
  op st :  Status -> Attribute .


  vars r a s : Oid .
  vars x y x' y' ht wd h : Nat .
  var blocked : LocSet .
  var rcid : RoverCid .

  rl[drive]:
  < r : rcid | myactuator(a),
               mysensor(s),
               pos (x,y), 
               hd(h),
               st(idle),
               grid(ht,wd,blocked),
               ratts:AttributeSet >
  msg(r,a,drive)
  =>
  ( if (h rem 90) == 0
    then < r : rcid | myactuator(a),
                      mysensor(s),
                      pos (x,y), 
                      hd(h),
                      st(driving),
                      grid(ht,wd,blocked),
                      ratts:AttributeSet >
    else < r : rcid | myactuator(a),
                      mysensor(s),
                      pos (x,y), 
                      hd(h),
                      st(idle),
                      grid(ht,wd,blocked),
                      ratts:AttributeSet >
         msg(s,r,sensorValues(posAndHead((x,y),dir(h))))
   fi ) .

  crl[driving]:
  < r : rcid | mysensor(s),
               pos (x,y), 
               hd(h),
               st(driving),
               grid(ht,wd,blocked),
               ratts:AttributeSet >
  =>
  < r : rcid | mysensor(s),
               pos (x',y'), 
               hd(h),
               st(idle),
               grid(ht,wd,blocked),
               ratts:AttributeSet >
  msg(s,r,sensorValues(posAndHead((x',y'),dir(h))))
  if  (x',y') := newLoc(ht,wd,(x,y), dir(h), blocked) .


  rl[turn]:
  < r : rcid | myactuator(a),
               pos (x,y), 
               hd(h),
               st(idle),
               grid(ht,wd,blocked),
               ratts:AttributeSet >
  msg(r,a,turn)
  =>
  < r : rcid | myactuator(a),
               pos (x,y), 
               hd(h),
               st(turning),
               grid(ht,wd,blocked),
               ratts:AttributeSet >  .

  rl[turning]:
  < r : rcid | mysensor(s),
               pos (x,y), 
               hd(h),
               st(turning),
               grid(ht,wd,blocked),
               ratts:AttributeSet >
  =>
  < r : rcid | mysensor(s),
               pos (x,y), 
               hd((h + 45) rem 360),
               st(idle),
               grid(ht,wd,blocked),
               ratts:AttributeSet >
  msg(s,r,sensorValues(posAndHead((x,y),dir(((h + 45) rem 360))))) .

endm


mod ROVER-TEST is
  inc GRID-TEST .
  inc ROVER .

  op rov : -> Object .
  op Rover : -> RoverCid .

  eq rov = < o("MyRover") : Rover | myactuator(o("MyPosAndHeadActuator")), 
                                    mysensor(o("MyPosAndHeadSensor")), 
                                    pos(0,0), 
                                    hd(90),
                                    st(idle),
                                    grid(5,5,B) > .
endm