A bit more of a big hammer, but it's pretty straightforward with TLA+ as well:<p><pre><code> ---- MODULE DogBunny ----
VARIABLE location
Init ==
location = [
dog |-> "Tree",
bunny1 |-> "House",
bunny2 |-> "Boat"
]
Goal ==
location = [
dog |-> "Bone",
bunny1 |-> "Carrot",
bunny2 |-> "Carrot"
]
Occupied(loc) ==
\E animal \in DOMAIN location: location[animal] = loc
Unidir(animal, from, to) ==
location[animal] = from /\ location' = [ location EXCEPT ![animal] = to ]
Bidir(animal, a, b) ==
Unidir(animal, a, b) \/ Unidir(animal, b, a)
Move(animal) ==
\/ Unidir(animal, "Carrot", "Tree")
\/ Bidir(animal, "Well", "Carrot") /\ ~Occupied("Bone")
\/ Bidir(animal, "Well", "Tree")
\/ Bidir(animal, "Well", "Flower")
\/ Bidir(animal, "Tree", "House") /\ Occupied("Bone") /\ Occupied("Flower")
\/ Unidir(animal, "Flower", "Boat")
\/ Bidir(animal, "House", "Boat") /\ Occupied("Tree")
\/ Bidir(animal, "House", "Bone") /\ Occupied("Carrot")
\/ Unidir(animal, "Bone", "Boat")
Next ==
\E animal \in DOMAIN location: Move(animal)
Invariant ==
~Goal
====
</code></pre>
with this config file:<p><pre><code> INIT Init
NEXT Next
INVARIANT Invariant
CHECK_DEADLOCK FALSE
</code></pre>
Finds (presumably) the same solution, with 26 steps.