I don't know if it's better or nicer. "I am but an egg."
Here is Lecture 4 of Lamport's course: https://lamport.azurewebsites.net/video/video4.html
TLA+ source code:
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
SmallToBig == IF big + small =
This is what I came up with (SWI Prolog). Note that I made some constraints explicit to prune the search,
like guarding the empty_FOO steps with constraints that the jugs
must not already be empty:
:- use_module(library(clpfd)).
type_ok(Small, Big) :- Small in 0..3, Big in 0..5.
next_dh(Moves) :- next_dh(0, 0, Moves).
next_dh(Small, Big, [[Move, Si, Bi]|Moves]) :-
type_ok(Small, Big),
die_hard(Move, Small, Big, Si, Bi),
(Bi = 4 -> Moves = [] ; next_dh(Si, Bi, Moves)).
die_hard( fill_small, Small, Big, 3, Big) :- Small # 0.
die_hard( empty_big, Small, Big, Small, 0) :- Big #> 0.
die_hard(small_to_big, Small, Big, S, B) :-
Big # 0,
small_to_big(Small, Big, S, B).
die_hard(big_to_small, Small, Big, S, B) :-
Small # 0,
big_to_small(Small, Big, S, B).
big_to_small(Small, Big, S, 0) :-
Small + Big #= 3,
B #= Big - (3 - Small).
small_to_big(Small, Big, 0, B) :-
Small + Big #= 5,
S #= Small - (5 - Big).
And here's a query with depth limit and some manual reflow of the list for presentation...
?- call_with_depth_limit(next_dh(Moves), 11, _).
Moves = [
[fill_big, 0, 5],
[big_to_small, 3, 2],
[empty_small, 0, 2],
[big_to_small, 2, 0],
[fill_big, 2, 5],
[big_to_small, 3, 4]
] ;
true.