CONTEXT
  WaterTank_2Ctrl_2Tanks_Ctx
EXTENDS
  WaterTank_2Tanks_Ctx
CONSTANTS
  guess_gs
AXIOMS
  axm1: guess_gs : STATES*STATES --> STATES
  axm2: 
    guess_gs = {
      (Emptying|->Emptying)|->Emptying,
      (Emptying|->Stable)|->Emptying,
      (Stable|->Emptying)|->Emptying,
      (Filling|->Filling)|->Filling,
      (Filling|->Stable)|->Filling,
      (Stable|->Filling)|->Filling,
      (Stable|->Stable)|->Stable,
      (Emptying|->Filling)|->Normal,
      (Filling|->Emptying)|->Normal
    } \/ { (x_|->y_)|->z_ | z_ = Normal & (x_ = Normal or y_ = Normal) }
END