MACHINE
  WaterTank_1Ctrl_1Tank
REFINES
  WaterTank_ode
SEES
  WaterTank_1Tank_Ctx
VARIABLES
  t
  V
  x_s
EVENTS
  INITIALISATION
  THEN
    act1: t := Rzero
    act2: 
      V :|
        V' : RRealPlus --> S &
        solutionOf(RRealPlus,V',ode(NoFlow,V0,Rzero))
    act3: x_s := Stable
  END

  Progress
  REFINES Progress
  THEN
    act1: t :| t' : RRealPlus & (t |-> t' : lt)
  END

  Behave
  REFINES Behave
  ANY
    e
  WHERE
    grd1: e : DE(S)
    grd2: Solvable(Closed2Infinity(t),e)
  THEN
    act1: V :| V' : RRealPlus --> S & AppendSolutionBAP(e,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),V,V')
  END

  ctrl_sense_too_high
  REFINES ctrl_sense_too_high
  WHERE
    grd1: Vhigh |-> V(t) : leq
  THEN
    act1: x_s := Emptying
  END

  ctrl_sense_too_low
  REFINES ctrl_sense_too_low
  WHERE
    grd1: V(t) |-> Vlow : leq
  THEN
    act1: x_s := Filling
  END

  ctrl_transition_emptying
  REFINES ctrl_transition_emptying
  WHERE
    grd1: Vlow |-> V(t) : lt
  THEN
    act1: x_s := Emptying
  END

  ctrl_transition_filling
  REFINES ctrl_transition_filling
  WHERE
    grd1: V(t) |-> Vhigh : lt
  THEN
    act1: x_s := Filling
  END

  ctrl_transition_normal
  REFINES ctrl_transition_normal
  WHERE
    grd1: Vlow |-> V(t) : lt
    grd2: V(t) |-> Vhigh : lt
  THEN
    act1: x_s := Normal
  END

  ctrl_transition_stable
  REFINES ctrl_transition_stable
  WHERE
    grd1: Vlow |-> V(t) : lt
    grd2: V(t) |-> Vhigh : lt
  THEN
    act1: x_s := Stable
  END

  ctrl_actuate_pumps
  REFINES ctrl_actuate_pumps
  ANY
    ss
    io
  WHERE
    grd4: ss : STATES
    grd5: x_s = ss
    grd6: io : SingleTankPolicy(ss)
  WITH
    Phi: Phi = flowIO(Rzero,Vmax,delta_in,delta_out)(io)(t|->V(t))
  THEN
    act1: 
      V :|
        V' : RRealPlus --> S &
        AppendSolutionBAP(
          ode(flowIO(Rzero,Vmax,delta_in,delta_out)(io)(t|->V(t)),V(t),t),
          RRealPlus,
          Closed2Open(Rzero,t),Closed2Infinity(t),
          V,V'
        )
  END

END