MACHINE
  WaterTank_2Ctrl_2Tanks
REFINES
  WaterTank_base
SEES
  WaterTank_2Ctrl_2Tanks_Ctx
VARIABLES
  t
  V1
  V2
  V1_sim
  V2_sim
  x_s1
  x_s2
  Delta_sim_1
  Delta_sim_2
INVARIANTS
  inv1: V1 : RRealPlus --> S
  inv2: V2 : RRealPlus --> S
  inv3: V1_sim : RRealPlus --> S
  inv4: V2_sim : RRealPlus --> S
  inv5: x_s1 : STATES
  inv6: x_s2 : STATES
  inv7: V = fadd(V1, V2)
  inv8: boundedBy(RRealPlus,fadd(V1,V2_sim),Vlow,Vhigh)
  inv9: boundedBy(RRealPlus,fadd(V1_sim,V2),Vlow,Vhigh)
  inv10: Delta_sim_1 : RRealPlus
  inv11: Delta_sim_2 : RRealPlus
  inv12: ! t_ . t_ : RRealPlus => abs(minus(V2(t_) |-> V2_sim(t_))) |-> Delta_sim_2 : leq
  inv13: ! t_ . t_ : RRealPlus => abs(minus(V1(t_) |-> V1_sim(t_))) |-> Delta_sim_1 : leq
  inv14: x_s = guess_gs(x_s1|->x_s2)
EVENTS
  INITIALISATION
  WITH
    V': V' = fadd(V1', V2')
  THEN
    act1: t := Rzero
    act2: 
      V1,V1_sim,V2,V2_sim :|
        V1' : RRealPlus --> S & V2' : RRealPlus --> S &
        V1_sim' : RRealPlus --> S & V2_sim' : RRealPlus --> S &
        solutionOf(RRealPlus,V1',ode(NoFlow,V10,Rzero)) &
        solutionOf(RRealPlus,V2',ode(NoFlow,V20,Rzero)) &
        V1_sim' = V1' & V2_sim' = V2'
    act3: x_s1,x_s2 := Stable,Stable
    act4: Delta_sim_1 :: RRealPlus
    act5: Delta_sim_2 :: RRealPlus
  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' = fadd(V1',V2')
  THEN
    act1: 
      V1,V2 :|
        V1' : RRealPlus --> S & V2' : RRealPlus --> S &
        AppendSolutionBAP(e,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),fadd(V1,V2),fadd(V1',V2'))
  END

  ctrl_sense_too_high_1
  REFINES ctrl_sense_too_high
  WHERE
    grd1: plus(Vhigh |-> Delta_sim_2) |-> plus(V1(t) |-> V2_sim(t)) : leq
  THEN
    act1: x_s1 := Emptying
  END

  ctrl_sense_too_high_2
  REFINES ctrl_sense_too_high
  WHERE
    grd1: plus(Vhigh |-> Delta_sim_1) |-> plus(V1_sim(t) |-> V2(t)) : leq
  THEN
    act1: x_s2 := Emptying
  END

  ctrl_sense_too_low_1
  REFINES ctrl_sense_too_low
  WHERE
    grd1: plus(V1(t) |-> V2_sim(t)) |-> minus(Vlow |-> Delta_sim_2) : leq
  THEN
    act1: x_s1 := Filling
  END

  ctrl_sense_too_low_2
  REFINES ctrl_sense_too_low
  WHERE
    grd1: plus(V1_sim(t) |-> V2(t)) |-> minus(Vlow |-> Delta_sim_1) : leq
  THEN
    act1: x_s2 := Filling
  END

  ctrl_transition_emptying_1
  REFINES ctrl_transition_emptying
  WHERE
    grd1: plus(Vlow |-> Delta_sim_2) |-> plus(V1(t) |-> V2_sim(t)) : lt
  THEN
    act1: x_s1 := Emptying
  END

  ctrl_transition_emptying_2
  REFINES ctrl_transition_emptying
  WHERE
    grd1: plus(Vlow |-> Delta_sim_1) |-> plus(V1_sim(t) |-> V2(t)) : lt
  THEN
    act1: x_s2 := Emptying
  END

  ctrl_transition_filling_1
  REFINES ctrl_transition_filling
  WHERE
    grd1: plus(V1(t) |-> V2_sim(t)) |-> minus(Vhigh |-> Delta_sim_2) : lt
  THEN
    act1: x_s1 := Filling
  END

  ctrl_transition_filling_2
  REFINES ctrl_transition_filling
  WHERE
    grd1: plus(V1_sim(t) |-> V2(t)) |-> minus(Vhigh |-> Delta_sim_1) : lt
  THEN
    act1: x_s2 := Filling
  END

  ctrl_transition_normal_1
  REFINES ctrl_transition_normal
  WHERE
    grd1: plus(Vlow |-> Delta_sim_2) |-> plus(V1(t) |-> V2_sim(t)) : lt
    grd2: plus(V1(t) |-> V2_sim(t)) |-> minus(Vhigh |-> Delta_sim_2) : lt
  THEN
    act1: x_s1 := Normal
  END

  ctrl_transition_normal_2
  REFINES ctrl_transition_normal
  WHERE
    grd1: plus(Vlow |-> Delta_sim_1) |-> plus(V1_sim(t) |-> V2(t)) : lt
    grd2: plus(V1_sim(t) |-> V2(t)) |-> minus(Vhigh |-> Delta_sim_1) : lt
  THEN
    act1: x_s2 := Normal
  END

  ctrl_transition_stable_1
  REFINES ctrl_transition_stable
  WHERE
    grd1: plus(Vlow |-> Delta_sim_2) |-> plus(V1(t) |-> V2_sim(t)) : lt
    grd2: plus(V1(t) |-> V2_sim(t)) |-> minus(Vhigh |-> Delta_sim_2) : lt
  THEN
    act1: x_s1 := Stable
  END

  ctrl_transition_stable_2
  REFINES ctrl_transition_stable
  WHERE
    grd1: plus(Vlow |-> Delta_sim_1) |-> plus(V1_sim(t) |-> V2(t)) : lt
    grd2: plus(V1_sim(t) |-> V2(t)) |-> minus(Vhigh |-> Delta_sim_1) : lt
  THEN
    act1: x_s2 := Stable
  END

  ctrl_actuate_pumps
  REFINES ctrl_actuate_pumps
  ANY
    ss
    e1
    e2
    ss1
    ss2
    fV1_sim
    fV2_sim
  WHERE
    grd01: ss : STATES
    grd02: ss = guess_gs(ss1|->ss2)
    grd11: e1 : DE(S)
    grd12: Solvable(Closed2Infinity(t),e1)
    grd13: isFlowEq(ss1,Closed2Infinity(t),e1,Rzero,V1max)
    grd14: ss1 : STATES
    grd15: x_s1 = ss1
    grd16: fV1_sim : Closed2Infinity(t) --> S
    grd17: ! V1_ . V1_ : Closed2Infinity(t) --> S & solutionOf(Closed2Infinity(t),V1_,e1) => (! t_ . t_ : Closed2Infinity(t) => abs(minus(V1_(t)|->fV1_sim(t))) |-> Delta_sim_1 : leq)
    grd21: e2 : DE(S)
    grd22: Solvable(Closed2Infinity(t),e2)
    grd23: isFlowEq(ss2,Closed2Infinity(t),e2,Rzero,V2max)
    grd24: ss2 : STATES
    grd25: x_s2 = ss2
    grd26: fV2_sim : Closed2Infinity(t) --> S
    grd27: ! V2_ . V2_ : Closed2Infinity(t) --> S & solutionOf(Closed2Infinity(t),V2_,e2) => (! t_ . t_ : Closed2Infinity(t) => abs(minus(V2_(t)|->fV2_sim(t))) |-> Delta_sim_2 : leq)
  WITH
    V': V' = fadd(V1',V2')
    e: 
      e : DE(S) & Solvable(Closed2Infinity(t),e) & isFlowEq(guess_gs(ss1|->ss2),Closed2Infinity(t),e,Rzero,Vmax) &
      (! V1_, V2_ .
        V1_ : Closed2Infinity(t) --> S & V2_ : Closed2Infinity(t) --> S &
        solutionOf(Closed2Infinity(t),V1_,e1) &
        solutionOf(Closed2Infinity(t),V2_,e2)
        => solutionOf(Closed2Infinity(t),fadd(V1_,V2_),e)
      )
  THEN
    act1: 
      V1,V2,V1_sim,V2_sim :|
        V1' : RRealPlus --> S & V2' : RRealPlus --> S &
        V1_sim' : RRealPlus --> S & V2_sim' : RRealPlus --> S &
        AppendSolutionBAP(e1,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),V1,V1') &
        AppendSolutionBAP(e2,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),V2,V2') &
        Closed2Open(Rzero,t) <| V1_sim' = Closed2Open(Rzero,t) <| V1_sim &
        Closed2Infinity(t) <| V1_sim' = fV1_sim &
        Closed2Open(Rzero,t) <| V2_sim' = Closed2Open(Rzero,t) <| V2_sim &
        Closed2Infinity(t) <| V2_sim' = fV2_sim
  END

END