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