MACHINE
  WaterTank_base
REFINES
  Generic
SEES
  WaterTank_base_Ctx
VARIABLES
  t
  V
  x_s
INVARIANTS
  inv1: V : RRealPlus --> S
  inv2: V = x_p
  inv3: V : D1(Closed2Infinity(t),RReal) & boundedBy(Closed2Infinity(t),Der(Closed2Infinity(t),RReal,V),dv_min,dv_max)
  inv4: boundedBy(RRealPlus,V,Vlow,Vhigh)
EVENTS
  INITIALISATION
  WITH
    x_p': x_p' = V'
  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)
  WITH
    x_p': x_p' = V'
  THEN
    act1: V :| V' : RRealPlus --> S & AppendSolutionBAP(e,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),V,V')
  END

  ctrl_sense_too_high
  REFINES Sense
  WHERE
    grd1: Vhigh |-> V(t) : leq
  WITH
    s: s = { Emptying }
    p: p = STATES*RRealPlus*{ V_ | Vhigh |-> V_ : leq }
  THEN
    act1: x_s := Emptying
  END

  ctrl_sense_too_low
  REFINES Sense
  WHERE
    grd1: V(t) |-> Vlow : leq
  WITH
    s: s = { Filling }
    p: p = STATES*RRealPlus*{ V_ | V_ |-> Vlow : leq }
  THEN
    act1: x_s := Filling
  END

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

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

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

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

  ctrl_actuate_pumps
  REFINES Actuate
  ANY
    e
    ss
  WHERE
    grd1: e : DE(S)
    grd2: Solvable(Closed2Infinity(t),e)
    grd3: isFlowEq(ss,Closed2Infinity(t),e,Rzero,Vmax)
    grd4: ss : STATES
    grd5: x_s = ss
  WITH
    x_p': x_p' = V'
    s: s = { ss }
  THEN
    act1: 
      V :|
        V' : RRealPlus --> S &
        AppendSolutionBAP(e,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),V,V')
  END

END