4 ms·
Solving the Dog-Bunny Puzzle with Program Verification Technology
- an1sotropy 4y agoPuzzle in question: https://news.ycombinator.com/item?id=32884467 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.
- note89 4y agoThanks 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.
- colanderman 4y agoA 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.