Lab 8 Assignment

1. Form the same groups of 2 that you worked in last week.
2. In these groups, encode two critical properties of your system in the PROMELA models of your state diagram that you created last week.
3. Run XSpin to verify that those critical properties hold with your model. To do this, open your PROMELA model, then Select Run -> Set Verification Parameters.. from the menu bar. Click the Run button to run the verification.
4. Turn in the results of your verification at the end of the lab session.