////////////////////////////////////////////
// CIRCAL Semaphore Excersise (and solution)

// Joel Kelso 2008

// Excersise 1 - Semaphores
// Quesiton 1.5

// Worker processes

Process A, ACritical, B, BCritical, C, CCritical
Event startCriticalA, finishCriticalA, pA, vA, sleepA, wakeA, goA
Event startCriticalB, finishCriticalB, pB, vB, sleepB, wakeB, goB
Event startCriticalC, finishCriticalC, pC, vC, sleepC, wakeC, goC
Event semaphoreEvents = pA vA pB vB pC vC sleepA sleepB sleepC wakeA wakeB wakeC goA goB goC

A         <- pA (goA ACritical + sleepA wakeA ACritical)
ACritical <- startCriticalA finishCriticalA vA A

B         <- pB (goB BCritical + sleepB wakeB BCritical)
BCritical <- startCriticalB finishCriticalB vB B

C         <- pC (goC CCritical + sleepC wakeC CCritical)
CCritical <- startCriticalC finishCriticalC vC C

// Semaphore

Process Sem, Empty, Full0, Full1, Full2, Wake0, Wake1

Empty       <- pA goA Full0 + 
               pB goB Full0 + 
               pC goC Full0 +
               vA Empty + vB Empty + vC Empty
Full0       <- pA sleepA Full1 +
               pB sleepB Full1 +
               pC sleepC Full1 +
               vA Empty + vB Empty + vC Empty
Full1       <- pA sleepA Full2 +
               pB sleepB Full2 +
               pC sleepC Full2 +
               vA Wake0 + vB Wake0 + vC Wake0
Full2       <- vA Wake1 + vB Wake1 + vC Wake1
Wake0       <- wakeA Full0 + wakeB Full0 + wakeC Full0
Wake1       <- wakeA Full1 + wakeB Full1 + wakeC Full1

Sem   <- Empty