*****************************************************************************
***               Special PosAndHead Interfaces                           ***
***                                                                       ***
*****************************************************************************

*****************************************************************************
***           PosHeadController-PosHeadActuator-Interface                 ***
***                                                                       ***
*****************************************************************************

fmod PHCONTROLLER-PHACTUATOR-INTERFACE is   
  inc CONTROLLER-ACTUATOR-INTERFACE .

  ops drive turn : -> Command .
endfm 


*****************************************************************************
***           Rover-PosHeadActuator-Interface                             ***
***                                                                       ***
*****************************************************************************

fmod ROVER-PHACTUATOR-INTERFACE is  
  inc DEVICE-ACTUATOR-INTERFACE .

  ops drive turn : -> MsgBody .
endfm 

*****************************************************************************
***            Rover-PosHeadSensor-PosHeadSensor-Interface                ***
***                                                                       ***
*****************************************************************************

fmod ROVER-PHSENSOR-INTERFACE is   
  inc DEVICE-SENSOR-INTERFACE .
  inc GRID .

  op posAndHead : Loc Dir -> SensorValue . 
endfm 



*****************************************************************************
***         PosHeadEstimator-PosHeadSensor-Interface                      ***
***                                                                       ***
*****************************************************************************

fmod PHESTIMATOR-PHSENSOR-INTERFACE is
  inc ESTIMATOR-SENSOR-INTERFACE .
  inc GRID .

  sort PosAndHeadMeasurement .
  subsort PosAndHeadMeasurement < Measurement .
 
  *** For simplicity same as  PosAndHeadStateValue 
  op _`,_dir_ : Nat Nat Dir  -> PosAndHeadMeasurement .
endfm 

*****************************************************************************
***   Special PosAndHead State Value                                      ***
***                                                                       ***
*****************************************************************************

*** used in POSANDHEAD-ESTIMATOR 
***         POSANDHEAD-STATE-VARIABLE
***         POSANDHEAD-CONTROLLER
***         POSANDHEAD-ESTIMATOR
fmod POSANDHEAD-STATE-VALUE is
  inc GRID .
  inc STATE-VALUE .

  sort PosAndHeadStateValue .  
  subsort PosAndHeadStateValue < StateValue .

  op  _`,_dir_ : Nat Nat Dir  -> PosAndHeadStateValue .

  op _@x : PosAndHeadStateValue -> Nat .
  op _@y : PosAndHeadStateValue -> Nat .
  op _@d : PosAndHeadStateValue -> Dir .

  vars x y : Nat .
  var d : Dir .

  eq (x,y dir d)@x = x .
  eq (x,y dir d)@y = y .
  eq (x,y dir d)@d = d .
endfm