Dancers (TLBoS, 3.8)

dancers.pml

#define pairs 5
#include "semaphore.h"

mtype = { male, female }

Semaphore mutex, convo1, convo2
Semaphore queue[3]
byte      count[3]

inline male_dance() {
    printf("Male %d: Shall we dance?\n", id)
    sem_signal(convo1)
    sem_wait(convo2)
    printf("Male %d: Take my hand.\n\n", id)
    sem_signal(mutex)
}

inline female_dance() {
    sem_wait(convo1)
    printf("Female %d: Okay...\n", id)
    sem_signal(convo2)
}

proctype Dancer(byte id; mtype me, you) {
    sem_wait(mutex)
    
    if
      :: count[you] > 0 ->
           count[you]--
           sem_signal(queue[you])
      :: else ->
           count[me]++
           sem_signal(mutex)
           sem_wait(queue[me])
    fi
    
    if
      :: me == male   -> male_dance()
      :: me == female -> female_dance()
    fi
}

init {
    byte id
    sem_init(mutex, 1)
    atomic {
        for (id : 1 .. pairs) {
            run Dancer(id, male, female)
            run Dancer(id, female, male)
        }
    }
}

sample

orin% spin -T dancers.pml
Male 1: Shall we dance?
Female 3: Okay...
Male 1: Take my hand.

Male 4: Shall we dance?
Female 5: Okay...
Male 4: Take my hand.

Male 3: Shall we dance?
Female 2: Okay...
Male 3: Take my hand.

Male 5: Shall we dance?
Female 1: Okay...
Male 5: Take my hand.

Male 2: Shall we dance?
Female 4: Okay...
Male 2: Take my hand.

11 processes created
orin% spin -T dancers.pml
Male 4: Shall we dance?
Female 4: Okay...
Male 4: Take my hand.

Male 3: Shall we dance?
Female 1: Okay...
Male 3: Take my hand.

Male 1: Shall we dance?
Female 2: Okay...
Male 1: Take my hand.

Male 5: Shall we dance?
Female 5: Okay...
Male 5: Take my hand.

Male 2: Shall we dance?
Female 3: Okay...
Male 2: Take my hand.

11 processes created
orin% spin -T dancers.pml
Male 1: Shall we dance?
Female 5: Okay...
Male 1: Take my hand.

Male 2: Shall we dance?
Female 1: Okay...
Male 2: Take my hand.

Male 5: Shall we dance?
Female 4: Okay...
Male 5: Take my hand.

Male 4: Shall we dance?
Female 3: Okay...
Male 4: Take my hand.

Male 3: Shall we dance?
Female 2: Okay...
Male 3: Take my hand.

11 processes created
orin% 

semaphore.h

#ifndef SEMAPHORE_H
#define SEMAPHORE_H

typedef Semaphore { byte _free }

#define sem_init(sem, n)  sem._free = n
#define sem_wait(sem)     atomic { sem._free > 0; sem._free-- }
#define sem_signal(sem)   sem._free++

#endif