**This is an old revision of the document!**

Objectives:

• Predict the size of a state space in a PROMELA verification model
• Write simple PROMELA verification models that use shared variables for synchronization
• Use PROMELA to find solutions to brain-teasers

Problems

1. (10 points) Answer problems 1(a) through 1(e) from the SPIN Verification Examples and Exercises

2. (30 points) Model the following mutual exclusion algorithm with Promela (25 points) and prove is correctness or incorrectness with SPIN (5 points).

/*
R. W. Doran and L. K. Thomas.  Variants of the software solution to
mutual exclusion.  Information Processing Letters 10(4--5):206--208,
1980.

Process A                           Process B
1. A_needs := true;                    B_needs :=  true;
2. if B_needs then begin               if A_needs then begin
3.   if turn = 'B' then begin            if turn = 'A' then begin
4.     A_needs := false;                   B_needs := false;
5.     wait until turn = 'A';              wait until turn = 'B';
6.     A_needs := true;                    B_needs := true;
7.   end;                                end;
8.   wait until !B_needs;                wait until !A_needs;
9. end;                                end;
10. CRITICAL SECTION                    CRITICAL SECTION
11. turn := 'B';                        turn := 'A';
12. A_needs := false;                   B_needs := false;
13. NON-CRITICAL SECTION                NON-CRITICAL SECTION
*/

3. (30 points) Write a Promela model for the below problem (25 point) and use SPIN to find a solution (5 points).

A farmer wants to cross a river and take with him a wolf, a goat, and a cabbage. There is a boat that can fit himself plus either the wolf, the goat, or the cabbage. If the wolf and the goat are alone on one shore, the wolf will eat the goat. If the goat and the cabbage are alone on the shore, the goat will eat the cabbage. How can the farmer bring the wolf, the goat, and the cabbage across the river?