CONTEXT
  WaterTank_1Tank_Cylinder_Ctx
EXTENDS
  WaterTank_1Tank_Ctx
CONSTANTS
  cylinderV
  Base
  H0
  Hmax
  delta_in_H
  delta_out_H
AXIOMS
  axm0: cylinderV = (% h_ . h_ : RReal | times(Base |-> h_))
  axm1: Base : RReal
  axm2: Rzero |-> Base : lt
  axm3: H0 : RReal
  axm4: times(Base |-> H0) = V0
  axm5: Hmax : RReal
  axm6: times(Base |-> Hmax) = Vmax
  axm7: delta_in_H : RReal
  axm8: times(Base |-> delta_in_H) = delta_in
  axm9: delta_out_H : RReal
  axm10: times(Base |-> delta_out_H) = delta_out
END