Die Harder

There is a 3-gallon jug and a 5-gallon jug next to a fountain with infinite water. Your goal is to measure out exactly 4 gallons by filling, emptying, and pouring between the jugs.

Variables

Your spec should contain two variables:

small — the number of gallons currently in the 3-gallon jug.
big — the number of gallons currently in the 5-gallon jug.

Initial State

Both jugs initial start without any water.

Transitions

At each step any of the following can happen

Fill the small jug to its capacity.
Fill the big jug to its capacity.
Empty the small jug.
Empty the big jug.
Pour from the small jug into the big jug until the big jug is full or the small jug is empty.
Pour from the big jug into the small jug until the small jug is full or the big jug is empty.

Invariant

Add an invariant asserting that the big jug never contains exactly 4 gallons: big # 4. When TLC violates this invariant it will produce a counter-example — a sequence of actions that reaches big = 4. That sequence is the solution to the puzzle.