*****************************************************************************
***                   PosAndHeadEstimator                                 ***
***                                                                       ***
***  knows its hwadapter, state-variable                                  ***
*****************************************************************************


mod POSANDHEAD-ESTIMATOR is
  inc ESTIMATOR .
  inc STATE-VARIABLE-ESTIMATOR-INTERFACE .
  inc PHESTIMATOR-PHSENSOR-INTERFACE .
  inc POSANDHEAD-STATE-VALUE . 
  
  sort PosAndHeadEstCid .
  subsort PosAndHeadEstCid < EstimatorCid .

  *** Specification of `verifyState(measurement)'
  vars x, y : Nat .
  eq verifyState((x,y dir (d:Dir))) = (x,y dir (d:Dir)) . 
endm

mod POSANDHEAD-ESTIMATOR-TEST is
  inc POSANDHEAD-ESTIMATOR .

  op PosAndHeadEst : -> PosAndHeadEstCid .
  
  op myphest : -> Object .
  eq myphest = 
     < o("MyPosAndHeadEstimator") : PosAndHeadEst |
                                    mysensor(o("MyPosAndHeadSensor")),
                                    mysv(o("MyPosAndHeadStateVar")),
                                    state(uk),
                                    waitAfter(noMsg) > .
endm