*****************************************************************************
***                        Estimator                                      ***
***                                                                       ***
***                                                                       ***
*****************************************************************************

mod ESTIMATOR is 
  inc ATTRIBUTES .
  inc ESTIMATOR-SENSOR-INTERFACE .
  inc STATE-VARIABLE-ESTIMATOR-INTERFACE .

  sort EstimatorCid .
  subsort EstimatorCid < Cid .

  *** Attributes
  op state : StateValue -> Attribute .

  *** converts a measurement into a state value 
  op verifyState : Measurement  -> StateValue .

  vars sens est sv : Oid .
  var estcid  : EstimatorCid .
  var m : Measurement .
  var v : StateValue .

  rl[receiveMeasurementUpdStateReq]:
  < est : estcid | mysensor(sens),
                   mysv(sv), 
                   waitAfter(noMsg),   
                   state(v),
                   estatts:AttributeSet >
  msg(est, sens, newMeasurement(m))
  => 
  < est : estcid | mysensor(sens),
                   mysv(sv), 
                   waitAfter(msg(est,sens,newMeasurement(m))),
                   state(verifyState(m)),
                   estatts:AttributeSet > 
  msg(sv,est,updStateReq(verifyState(m))) .


  rl[receiveAckUpdateStateVar]:
  < est : estcid | mysv(sv), 
                   waitAfter(msg(est,sens,newMeasurement(m))),
                   estatts:AttributeSet >
  msg(est,sv,ackUpdStateReq(v))
  => 
  < est : estcid | mysv(sv),
                   waitAfter(noMsg),
                   estatts:AttributeSet > .
			       
endm


mod ESTIMATOR-TEST is
  inc ESTIMATOR .

  op Estimator : -> EstimatorCid .

  op myestimator : -> Object .

  eq myestimator = 
     < o("MyEstimator") : Estimator | mysv(o("MyStateVar")),
                                      mysensor(o("MySensor")),
                                      state(uk),
                       		      waitAfter(noMsg) > .
endm