Monday:

1. First download and install SPIN (including iSPIN)
2. Windows (My solution)
• Download and unpack pc_spin601.zip
• Install cygwin Click on link setup.exe
• make sure during cygwin installation to select packages gcc and tcl
• Download graphviz for windows (current stable release)
• copy dot.exe to the unpacked pc_spin directory
• Run cygwin. Goto /cygdrive/c/... where you unpacked pc_spin. Run ./ispin
3. Start with the simple steps in GettingStarted
• Note for number seven: if you get an error message click on the advanced options first.

Tuesday:

1. Continue with exercises 1a to 1h
2. Model a system with three processes (A, B and C)
1. Initialize all processes.
2. They send message from A -> B -> C -> A ...
3. They may communicate on different channels or on one channel, where the first data field is the intended receiver.
4. Each process receives an integer and increments it by one before sending it to the next process.

SPIN hand-in:

Dekker's algorithm from page 204 of the slides

1. Implement the algorithm with two processes
2. Check relevant properties
3. Extend the algorithm in some way to three processes
4. Check relevant properties
5. Describe your findings in a pdf document
6. Send two models and a pdf file to kgl@cs.aau.dk and ulrik@cs.aau.dk by the 22nd of February