CONTEXT
  WaterTank_2Tanks_Cylinder_Ctx
EXTENDS
  WaterTank_2Tanks_Ctx
  WaterTank_ode_Ctx
CONSTANTS
  B1
  B2
  H1max
  H2max
  H10
  H20
  delta_in_h1
  delta_out_h1
  delta_in_h2
  delta_out_h2
AXIOMS
  axm1: B1 : RReal
  axm2: Rzero |-> B1 : lt
  axm3: B2 : RReal
  axm4: Rzero |-> B2 : lt
  axm5: H1max : RReal
  axm6: Rzero |-> H1max : lt
  axm7: H2max : RReal
  axm8: Rzero |-> H2max : lt
  axm9: H10 : RReal
  axm10: Rzero |-> H10 : leq
  axm11: H10 |-> H1max : leq
  axm12: H20 : RReal
  axm13: Rzero |-> H20 : leq
  axm14: H20 |-> H2max : leq
  axm15: Vmax = sLinComb2(B1,H1max,B2,H2max)
  axm16: V0 = sLinComb2(B1,H10,B2,H20)
  axm17: delta_in_h1 : RReal
  axm18: Rzero |-> delta_in_h1 : lt
  axm19: delta_out_h1 : RReal
  axm20: Rzero |-> delta_out_h1 : lt
  axm21: delta_in_h2 : RReal
  axm22: Rzero |-> delta_in_h2 : lt
  axm23: delta_out_h2 : RReal
  axm24: Rzero |-> delta_out_h2 : lt
END