-
Notifications
You must be signed in to change notification settings - Fork 0
PersonalSpecs GoatCabbageWolf
I was discussing my DieHard spec with a friend, and he shared with me a folklore puzzle called The Wolf, Goat & Cabbage Problem. It felt similar enough to sretch my DieHard model into this problem space.
The cabbage problem -- a farmer goes to market.
Comes to a river, Boat can only carry one item and himself.
Wolf eats the goat. Goat eats the cabbage.
How does everone cross?
Initially I thought that the farmer and the boat were unessential. I can abstract away these details. However, I see now that the Boat provides a key place for conflicting items to "live". It is not enough to simply send an item from one side to the other. the "transfer to shore" or "exchange with shore" is important.
Thus The following actions need to be added to the spec.
transferToShore == \* takes an item from boat and places on shore. Can only occur when non-conflicting items are on shore.
exchangeWithShore == \* takes an item fro the boat and replaces it with an item on the shore. Allows items which conflict to be arrived with the shore.Additionally, the Farmer is also essential. Modeling the Initial state without the farmer immediately creates and invalid condition, e.g., the wolf eats the fox. Hence, The wolf will not eat the fox in the presence of the farmer. This the Farmer also is essential to the definition.