Die Hard
This is a good example to understand the grammar and state exploration of FizzBee.
This problem is from the movie Die Hard 3, where Bruce Willis and Samuel L. Jackson are given a task to measure 4 gallons of water using a 3gallon and a 5gallon jug.
Watch it here. https://youtu.be/6cAbgAaEOVE
This is also a known example from TLA+ video tutorial  so if you are familiar with TLA+ most likely you have done this example.
 You have a 3litre jug and a 5litre jug.
 Infinite water supply.
 You need to measure 4 litres of water. Find the [shortest] steps to measure 4 litres of water.
For these modeling problems, we need to define the state and the actions that can be performed on the state.
 Amount of water in the 3litre jug
 Amount of water in the 5litre jug
 Fill the 3litre jug
 Fill the 5litre jug
 Empty the 3litre jug
 Empty the 5litre jug
 Pour water from the 3litre jug to the 5litre jug
 Pour water from the 5litre jug to the 3litre jug
This is an unusual example  technically, we need to find the shortest path to reach the goal. So, instead of defining the invariant as what we want to be always true, we define the invariant as what should hold true to keep continuing  that is negation of end state.
That we stop when the 4 litres of water in the big jug.
Let us define two variables big and small for the two jugs, and start with both empty.
action Init:
big = 0
small = 0
Filling the 3litre jug is simple  just set the small to 3.
atomic action FillSmall:
small = 3
Set the big to 5.
atomic action FillBig:
big = 5
Set the small to 0.
atomic action EmptySmall:
small = 0
Set the big to 0.
atomic action EmptyBig:
big = 0
This is a bit tricky. We need to check if the small jug has water and the big jug is not full. If it has any remaining water, it should remain in the small jug.
atomic action SmallToBig:
if small + big <= 5:
# There is enough space in the big jug
big = big + small
small = 0
else:
# There is not enough space in the big jug
small = small  (5  big)
big = 5
This is similar to the previous action, but in the opposite direction.
atomic action BigToSmall:
if small + big <= 3:
# There is enough space in the small jug
small = big + small
big = 0
else:
# There is not enough space in the small jug
big = big  (3  small)
small = 3
We need to define the stopping condition as invariants.
always assertion NotFour:
return big != 4


Take a look at the trace that leads to the 4 litres of water in the big jug. It took 6 steps to reach the goal, each corresponding to each of the defined actions.
Equivalent implementation in TLA+. Stripped out the comments for brevity. Take a look at the github link for the code with the comments.
 MODULE DieHard 
EXTENDS Naturals
VARIABLES big,
small
TypeOK == /\ small \in 0..3
/\ big \in 0..5
Init == /\ big = 0
/\ small = 0
FillSmallJug == /\ small' = 3
/\ big' = big
FillBigJug == /\ big' = 5
/\ small' = small
EmptySmallJug == /\ small' = 0
/\ big' = big
EmptyBigJug == /\ big' = 0
/\ small' = small
Min(m,n) == IF m < n THEN m ELSE n
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small  (big'  big)
BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big  (small'  small)
Next == \/ FillSmallJug
\/ FillBigJug
\/ EmptySmallJug
\/ EmptyBigJug
\/ SmallToBig
\/ BigToSmall
Spec == Init /\ [][Next]_<<big, small>>

NotSolved == big # 4
=============================================================================
We have defined all possible actions. To find the shortest number of steps, we must use each of these actions once.
Can you reduce the number of actions and see if we can still find a solution? The solution might take more steps as it might have to repeat some actions.
Open the state graph, you might see that there are many transitions that are not necessary that are also explored. For example: Emptying a jug that is already empty, filling a jug that is already full, etc.
You can reduce these unnecessary steps by adding guard conditions to the actions.
atomic action FillSmall:
if small < 3:
small = 3
For this problem, it has no effect. But for some real problems, guard conditions would be critical to find deadlocks