[Solved]-Two People V Either Hungry Hungry One Fork Point Holds Fork V Holds Fork Nobody Holds Fork Q37225970

There are two people i and v; they can be either hungry or nothungry. There is one fork. At each point, i holds the fork, v holdsthe fork or nobody holds the fork.  Initially neither oneof them holds the fork and neither one is hungry. At any point, oneperson gets his or her turn. We assume they each get their turninfinitely often. Here is what happens when a person has theirturn:

If that person is currently holding the fork and is hungry thenthat person continues to hold the fork but stops being hungry. Ifthat person is holding the fork and not hungry then that personputs down the fork and may or may not be hungry. If nobody holdsthe fork and that person is hungry then that person picks up thefork and remains hungry. Otherwise, if that person does not holdthe fork, then that person does not pick up the fork and remainshungry if already hungry, but otherwise may become hungry or notbecome hungry.

The specification is that if a person becomes hungry then theperson will eventually pick up the fork. In NuSMV, show that thisis false, and explain the results.

Expert Answer

---

Answer to There are two people i and v; they can be either hungry or not hungry. There is one fork. At each point, i holds the for… . . .