Assignment 2

Model your algorithm in Promela.
Verify some properties of your model using Spin.
Write a report. In the report, describe your model. Motivate the design decisions that you have made. Also describe the properties that you have checked.

If you present material that is not your own, then mention the source.

If you are using LaTeX, you may want to try the package Listings for typesetting code. The user manual can be found here.