Lesson 4

• Examples in CAAL (Mutex, Dining Philosophers, Peterson Algorithm - sources available here).
• The need of a notion of program equivalence.

Exercises:

• RSBook Ex. 2.7. Build the transition system of the process \(\mathit{Office}\) defined as follows:
  \(\mathit{Office} = (CS | CM) \setminus \{\mathit{coin},\mathit{coffee}\}\)
  \(CS = \overline{pub}. \overline{coin}. \mathit{coffee}. CS\)
  \(CM = \mathit{coin}. \overline{\mathit{coffee}}. CM\)

• RSBook Es. 2.8. Let  \(A = b.a.B\). Prove that the following transitions exist/do not exist:
  \((A | \bar{b}.0) \setminus \{b\} \stackrel{\tau}{\to} (a.B | 0) \setminus \{b\}\)
  \((A | \bar{b}.0) \setminus \{a\} \stackrel{b}{\to} (a.B | \bar{b}.0) \setminus \{a\}\)
  \((A | \bar{b}.a.B) + (\bar{b}.A)[a/b] \stackrel{\bar{b}}{\to} (A | a.B)\)
  \((A | \bar{b}.a.B) + (\bar{b}.A)[a/b] \stackrel{\bar{a}}{\to} (A | a.B)\)
  \(A + a.B \not  \stackrel{c}{\to}\)

• Using the process \(Sem\) as defined during the lesson, implement a semaphore \(Sem_2\) which allows for two processes to enter the critical section, as indicated by the following specification: 
  \(\mathit{Sem}_2 = p. \mathit{Sem}_1\)
  \(\mathit{Sem}_1 = p. \mathit{Sem}_0 + v. \mathit{Sem}_2\)
  \(\mathit{Sem}_0 = v. \mathit{Sem}_1\)