// Mutual exclusion algorithm for n processes with a shared lock

// Process identifiers
typedef unsigned (1..2) pid_t;
// For n processes, the system has (n + 2) << (n - 1) states.

// pending processes
place pending (0..#pid_t) pid_t;
// processes in critical section
place critical (0..1) pid_t;
// quiescent processes (redundant place)
place quiet (0..#pid_t) pid_t: (pid_t p: p) minus
(place pending union place critical);

// flag: is the critical section available (redundant place)
place lock (0..1) bool (true): (place critical equals empty)#true;

trans Request
in {
  place quiet: x;
}
out {
  place pending: x;
};

trans GoCrit 
in {
  place pending: x;
  place lock: true;
}
out {
  place critical: x;
}
strongly_fair pid_t p: p == x;

trans Release 
in {
  place critical: x;
} out {
  place quiet: x;
  place lock: true;
};

// weak fairness for trans Request should not hold:
// []<>((>pid_t subset place quiet) => (>pid_t subset place pending))

// strong fairness for trans Request should not hold:
// ([]<>(>pid_t subset place quiet)) => ([]<>(>pid_t subset place pending))

// accessability property should hold:
// []((>pid_t subset place pending) => <>(>pid_t subset place critical))