$1.$ Consider the following informal specification of the Ferryman$-$Cabbage$-$Goat$-$Wolf problem: $(12+8+5-25$ points$)$

"A ferryman has to transport a piece of cabbage, a goat and a wolf across a river. On each journey he can carry at most one item. However, he cannot leave unattended on the same side: $(1)$ the cabbage and the goat, or $(2)$ the goat and wolf $($because the goat would eat the cabbage or the wolf would eat the goat$).$ The objective of the ferryman is to transport all goods to the other side of the river, without any conflicts. Can the ferryman transport all the goods to the other side safely?"

$($Q$1)$ Draw a model expressing all possible behaviors $($including that which results conflicts$).[$hint: you may consider atomic formulas for ferryman, cabbage, goat and wolf, which indicate whether one has already crossed the river or not.$]$

$($Q$2)$ Write the following property in suitable temporal logic formula and then verify against your proposed model: "There exists a safe path following which the ferryman will be able to transport all the goods to the other side of the river".

$($Q$3)$ How does the model checking solve the above puzzle? Justify your answer.