/////////////////////////////
// CIRCAL Semaphore Excersise

// Joel Kelso 2008

// Excersise 1 - Semaphores

// Worker processes

Process A, ACritical, B, BCritical
Event startCriticalA, finishCriticalA, pA, vA, sleepA, wakeA, goA
Event startCriticalB, finishCriticalB, pB, vB, sleepB, wakeB, goB
Event semaphoreEvents = pA vA pB vB sleepA sleepB wakeA wakeB goA goB

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

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

// Semaphore

Process Sem, Empty, Full, Wake, FullWaiting

Empty       <- pA goA Full + pB goB Full +
               vA Empty + vB Empty
Full        <- pA sleepA FullWaiting + pB sleepB FullWaiting +
               vA Empty + vB Empty
FullWaiting <- vA Wake + vB Wake
Wake        <- wakeA Full + wakeB Full

Sem   <- Empty

// Mutual exclusion property

Process Mutex

Mutex <- startCriticalA finishCriticalA Mutex +
         startCriticalB finishCriticalB Mutex