*****************************************************************************
***          Position and Heading Sensor                                  ***
*****************************************************************************
fmod POSANDHEAD-SENSOR is
  inc SENSOR .
  inc DEVICE-SENSOR-INTERFACE .
  inc PHESTIMATOR-PHSENSOR-INTERFACE .
  inc ROVER-PHSENSOR-INTERFACE .

  sort PosAndHeadSensorCid .
  subsort PosAndHeadSensorCid < SensorCid .

  *** Specification of createMeasurement(sensorValue)
  var sval : SensorValue . 
  vars x, y : Nat .

  eq createMeasurement(posAndHead((x,y),d:Dir)) =  ((x,y dir (d:Dir))) .  
endfm
		   
mod POSANDHEAD-SENSOR-TEST is
  inc POSANDHEAD-SENSOR .

  op PosAndHeadSensor : -> PosAndHeadSensorCid .

  op myphsensor : -> Object .
  eq myphsensor =
     < o("MyPosAndHeadSensor") : PosAndHeadSensor | 
                                          mydevice(o("MyRover")),
                                          myest(o("MyPosAndHeadEstimator")),
                                          measurement(noMeas) > .
endm