Solving the Dog-Bunny Puzzle with Program Verification Technology

Puzzle in question: https://news.ycombinator.com/item?id=32884467

"We use Standard ML, as the language endorsed by a certain breed of university professor who thinks they know programming better than you do." yikes - that is painfully accurate.

A bit more of a big hammer, but it's pretty straightforward with TLA+ as well:

    ---- 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
    
    ====

with this config file:

    INIT Init
    NEXT Next
    INVARIANT Invariant
    CHECK_DEADLOCK FALSE

Finds (presumably) the same solution, with 26 steps.

Thanks for showing me petri-nets, i have been wanting to learn about them for quite some time. But been to lazy to look it up.