*****************************************************************************
***                    StateVariable                                      ***
***  has a StateVal                                                       ***
***  knows its estimator, controller                                      ***
*****************************************************************************


mod STATE-VARIABLE is
  inc ATTRIBUTES .
  inc STATE-VARIABLE-ENVIRONMENT-INTERFACE .
  inc STATE-VARIABLE-CONTROLLER-INTERFACE .
  inc STATE-VARIABLE-ESTIMATOR-INTERFACE .

  sort SVCid .
  subsort SVCid < Cid .

  *** Attributes
  op  val : StateValue -> Attribute .
  op  req : Oid -> Attribute .
  op  cstr :  Constraint -> Attribute .

  *** Reasons
  op notReady : -> Reason .

  vars sv o o' ctrl est : Oid .
  var v v2 : StateValue .
  var svcid : SVCid .
  var cstr cstr' : Constraint .
  var b : Bool .
  var r : Reason .

  rl[startConstraintReadyReq]:
  < sv : svcid | myctrl(ctrl), 
                 req(o'),
                 cstr(cstr'), 
                 waitAfter(noMsg),
                 svatts:AttributeSet >
  msg(sv,o,startConstraint(cstr))
  =>
  < sv : svcid | myctrl(ctrl), 
                 req(o), 
                 cstr(cstr), 
                 waitAfter(msg(sv,o,startConstraint(cstr))),
                 svatts:AttributeSet >
  msg(ctrl,sv,readyReq) .

  rl[forwardConstraint]:
  < sv : svcid | myctrl(ctrl),
                 req(o), 
                 cstr(cstr),  
                 waitAfter(msg(sv,o,startConstraint(cstr))),
                 val(v), 
                 svatts:AttributeSet >
  msg(sv,ctrl,readyRep(b))
  =>
  if b
  then < sv : svcid | myctrl(ctrl),
                      req(o), 
                      cstr(cstr),  
                      waitAfter(msg(sv,ctrl,readyRep(b))),
                      val(v), 
                      svatts:AttributeSet >
       msg(ctrl,sv,startCstr(cstr,o,v))
       *** Optimization: SV sends current value with constraint to controller
  else < sv : svcid | myctrl(ctrl), 
                      req(o), 
                      cstr(cstr),  
                      waitAfter(noMsg),
                      val(v), 
                      svatts:AttributeSet >
       msg(o,sv,constraintFailure(cstr,notReady)) 
  fi .

  rl[stateValUpdNotifyCtrlAckEst] :
  < sv : svcid | myctrl(ctrl), 
                 myest(est),  
                 val(v), 
                 svatts:AttributeSet >
  msg(sv,est,updStateReq(v2))
  =>
  < sv : svcid | myctrl(ctrl),
                 myest(est),   
                 val(v2), 
                 svatts:AttributeSet > 
  msg(ctrl,sv,newVal(v2)) 
  msg(est,sv,ackUpdStateReq(v2)) .

  rl[endConstraint] :
  < sv : svcid | myctrl(ctrl),
                 waitAfter(msg(sv,ctrl,readyRep(true))), 
                 svatts:AttributeSet >
  msg(sv,ctrl,endCstr(cstr,o,r))
  =>
  if (r == noReason)
  then < sv : svcid | myctrl(ctrl), 
                      waitAfter(noMsg), 
                      svatts:AttributeSet > 
       msg(o,sv,constraintSuccess(cstr)) 
  else < sv : svcid | myctrl(ctrl),  
                      waitAfter(noMsg),
                      svatts:AttributeSet > 
       msg(o,sv,constraintFailure(cstr,r)) 
  fi .
endm

mod STATE-VARIABLE-TEST is
  inc STATE-VARIABLE .
  
  op StateVar : -> SVCid .

  op mystatevar : -> Object . 
  eq mystatevar = < o("MyStateVar") : StateVar |  myctrl(o("MyCtrl")), 
                                                  myctrl(o("MyEstimator")), 
                                                  req(o("noOid")),  
                                                  cstr(noCstr),
                                                  val(uk) > .
endm