1. Download the elevator example Alloy document, and open it in the Alloy analyzer. Execute all the checks and simulations (main menu, Execute>Execute All).
2. Notice that the reqStaysScheduledUntilServed assertion fails to check. Is it because the scope is too small or because the property does not hold?
3. Notice that the notStuckAtDestFloor assertion fails to check. Use the evaluator to analyze the counterexample and convince yourself that it is not because the scope is too small, but because the property does not hold. Propose a convincing modification to the system so that the property holds.
4. Consider the "easy" liveness property at slide n. 122. Write an assertion for it and check with the Alloy Analyzer whether it holds. If it doesn't, analyze the counterexample, possibly using the evaluator, and explain why.

Send your answers to pietro.braione@unimib.it.