MACHINE
  WaterTank_1Ctrl_2Tanks_Cylinder
REFINES
  WaterTank_ode
SEES
  WaterTank_2Tanks_Cylinder_Ctx
VARIABLES
  t
  x_s
  h1
  h2
INVARIANTS
  inv1: h1 : RRealPlus --> RReal
  inv2: h2 : RRealPlus --> RReal
  inv3: V = LinComb2(B1,h1,B2,h2)
EVENTS
  INITIALISATION
  WITH
    V': V' = LinComb2(B1,h1',B2,h2')
  THEN
    act1: t := Rzero
    act2: 
      h1,h2 :|
        h1' : RRealPlus --> S &
        h2' : RRealPlus --> S &
        solutionOf(
          RRealPlus,
          h1',
          ode(
            NoFlow,
            H10,
            Rzero
          )
        ) &
        solutionOf(
          RRealPlus,
          h2',
          ode(
            NoFlow,
            H20,
            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
    V': V' = LinComb2(B1,h1',B2,h2')
  THEN
    act1: 
      h1,h2 :|
        h1' : RRealPlus --> S &
        h2' : RRealPlus --> S &
        AppendSolutionBAP(
          e,
          RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),
          LinComb2(B1,h1,B2,h2),
          LinComb2(B1,h1',B2,h2')
        )
  END

  ctrl_sense_too_high
  REFINES ctrl_sense_too_high
  WHERE
    grd1: Vhigh |-> LinComb2(B1,h1,B2,h2)(t) : leq
  THEN
    act1: x_s := Emptying
  END

  ctrl_sense_too_low
  REFINES ctrl_sense_too_low
  WHERE
    grd1: LinComb2(B1,h1,B2,h2)(t) |-> Vlow : leq
  THEN
    act1: x_s := Filling
  END

  ctrl_transition_emptying
  REFINES ctrl_transition_emptying
  WHERE
    grd1: Vlow |-> LinComb2(B1,h1,B2,h2)(t) : lt
  THEN
    act1: x_s := Emptying
  END

  ctrl_transition_filling
  REFINES ctrl_transition_filling
  WHERE
    grd1: LinComb2(B1,h1,B2,h2)(t) |-> Vhigh : lt
  THEN
    act1: x_s := Filling
  END

  ctrl_transition_normal
  REFINES ctrl_transition_normal
  WHERE
    grd1: Vlow |-> LinComb2(B1,h1,B2,h2)(t) : lt
    grd2: LinComb2(B1,h1,B2,h2)(t) |-> Vhigh : lt
  THEN
    act1: x_s := Normal
  END

  ctrl_transition_stable
  REFINES ctrl_transition_stable
  WHERE
    grd1: Vlow |-> LinComb2(B1,h1,B2,h2)(t) : lt
    grd2: LinComb2(B1,h1,B2,h2)(t) |-> Vhigh : lt
  THEN
    act1: x_s := Stable
  END

  ctrl_actuate_pumps
  REFINES ctrl_actuate_pumps
  ANY
    io
    ss
  WHERE
    grd4: ss : STATES
    grd5: x_s = ss
    grd6: io : SingleTankPolicy(x_s)
  WITH
    V': V' = LinComb2(B1,h1',B2,h2')
    Phi: 
      Phi : RRealPlus*S --> S &
      isFlowODE(Emptying,Closed2Infinity(t),Phi,Rzero,Vmax) &
      Solvable(Closed2Infinity(t),ode(Phi,V(t),t)) &
      (! h1_,h2_ .
        h1_ : Closed2Infinity(t) --> RReal & h2_ : Closed2Infinity(t) --> RReal &
        solutionOf(Closed2Infinity(t),h1_,FlowIOODE(Rzero,H1max,delta_in_h1,delta_out_h1)(io)(t|->h1(t))) &
        solutionOf(Closed2Infinity(t),h2_,FlowIOODE(Rzero,H2max,delta_in_h2,delta_out_h2)(io)(t|->h2(t))) =>
        solutionOf(Closed2Infinity(t),LinComb2(B1,h1_,B2,h2_),ode(Phi,V(t),t))
      )
  THEN
    act1: 
      h1,h2 :|
        h1' : RRealPlus --> S &
        h2' : RRealPlus --> S &
        AppendSolutionBAP(
          FlowIOODE(Rzero,H1max,delta_in_h1,delta_out_h1)(io)(t|->h1(t)),
          RRealPlus,
          Closed2Open(Rzero,t),Closed2Infinity(t),
          h1,h1'
        ) &
        AppendSolutionBAP(
          FlowIOODE(Rzero,H2max,delta_in_h2,delta_out_h2)(io)(t|->h2(t)),
          RRealPlus,
          Closed2Open(Rzero,t),Closed2Infinity(t),
          h2,h2'
        )
  END

END