CONTEXT
  WaterTank_2Tanks_Ctx
EXTENDS
  WaterTank_base_Ctx
CONSTANTS
  V1max
  V2max
  V10
  V20
AXIOMS
  axm1: V1max : RReal
  axm2: Rzero |-> V1max : lt
  axm3: V2max : RReal
  axm4: Rzero |-> V2max : lt
  axm5: V10 : RReal
  axm6: Rzero |-> V10 : leq
  axm7: V10 |-> V1max : leq
  axm8: V20 : RReal
  axm9: Rzero |-> V20 : leq
  axm10: V20 |-> V2max : leq
END