*****************************************************************************
***                   PosAndHeadStateVariable                             ***
***  has as value a triple (Nat, Nat, Dir) (Location/Direction)           ***
***  knows its estimator, controller                                      ***
*****************************************************************************

mod POSANDHEAD-STATE-VARIABLE is
  inc POSANDHEAD-STATE-VALUE .
  inc STATE-VARIABLE .
  
  sort PosAndHeadSVCid .
  subsort PosAndHeadSVCid < SVCid .

endm

mod POSANDHEAD-STATE-VARIABLE-TEST is
  inc POSANDHEAD-STATE-VARIABLE .

  op PosAndHeadStateVar : -> PosAndHeadSVCid .
  
  op myphsv : -> Object .
  eq myphsv = 
     < o("MyPosAndHeadStateVar") : PosAndHeadStateVar |
               myctrl(o("MyPosAndHeadCtrl")), 
               myest(o("MyPosAndHeadEstimator")), 
               req(o("NoOid")), 
               waitAfter(noMsg), 
               cstr(noCstr), 
               val((0,0 dir(E))) > .
endm