CONTEXT
  WaterTank_base_Ctx
EXTENDS
  GenericCtx
CONSTANTS
  Vmax
  V0
  delta_in
  delta_out
  Vlow
  Vhigh
  dv_min
  dv_max
AXIOMS
  axm10: Vmax : RReal
  axm11: Rzero |-> Vmax : lt
  axm20: V0 : RReal
  axm21: Rzero |-> V0 : lt
  axm12: V0 |-> Vmax : lt
  axm30: delta_in : RReal
  axm31: Rzero |-> delta_in : lt
  axm32: delta_out : RReal
  axm33: Rzero |-> delta_out : lt
  axm34: delta_out |-> delta_in : lt
  axm40: Vlow : RReal
  axm41: Rzero |-> Vlow : lt
  axm42: Vlow |-> Vmax : lt
  axm43: Vhigh : RReal
  axm44: Rzero |-> Vhigh : lt
  axm45: Vhigh |-> Vmax : lt
  axm46: Vlow |-> Vhigh : lt
  axm47: Vlow |-> V0 : leq
  axm48: V0 |-> Vhigh : leq
  axm50: dv_min : RReal
  axm51: dv_min |-> Rzero : lt
  axm52: dv_max : RReal
  axm53: Rzero |-> dv_max : lt
  axm54: dv_min |-> dv_max : lt
END