TLA+ has no type declarations. Type correctness means variables have sensible values. We define a formula that asserts type correctness.

The next-state formula describes all permitted steps. It’s usually written as F1 \/ F2 \/ … \/ Fn, where each Fi allows a different kind of step. The behavior we wrote has 3 kinds of steps:

• Fill a jug.
• Empty a jug.
• Pour from one jug into the other.

It’s a formula that’s true for some steps and false for others.

Most people think this shouldn’t be needed. That’s a bad idea! It’s not math.

FillSmall == /\ small' = 3
						 /\ big' = big

EXTENDS Integers

VARIABLES small, big

TypeOk == /\ small \in 0..3
					/\ big   \in 0..5

Init == /\ big = 0
				/\ small = 0

FillSmall == /\ small' = 3
             /\ big' = big

FillBig == /\ big' = 5
	         /\ small' = small

EmptySmall == /\ small' = 0
              /\ big' = big

EmptyBig == /\ big' = 0
						/\ small' = small