// lukon omistaja (0=vapaa, 1..n=jokin prosessi)
typedef unsigned (0..2) owner_t;
// prosessin numero (1..>owner_t)
typedef owner_t (1..) client_t;

typedef struct {
  client_t next;
  client_t granted;
} turn_t;

typedef struct {
  client_t client;
  owner_t owner;
} ticket_t;

// paikka "jouten"
place idle (0..#client_t) client_t: client_t client: client;

// paikka "pyrkii"
place entering (0..#client_t) client_t;

// paikka "tarkkailee"
place testing (0..#client_t) client_t;

// paikka "kriittinen"
place critical (0..1) client_t;

// paikka "vuoro"
place turn (1) turn_t: <turn_t;

// paikka "liput"
place tickets (#client_t) ticket_t: client_t client: { client, 0 };

// siirtymä "aloita"
trans try
in { place idle: client; }
out { place entering: client; };

// siirtymä "siirry"
trans enter
in {
  place entering: client;
  place turn: { next, granted };
  place tickets: { client, t };
}
out {
  place testing: (next != granted)#client;
  place critical: (next == granted)#client;
  place turn: { +next, granted };
  place tickets: { client, next };
};

// siirtymä "koeta"
trans test
in {
  place testing: client;
  place turn: { next, granted };
  place tickets: { client, t };
}
out {
  place testing: (t == 0 || is client_t t != granted)#client;
  place critical: (t > 0 && is client_t t == granted)#client;
  place turn: { next, granted };
  place tickets: { client, t };
};

// siirtymä "poistu"
trans exit
in {
  place critical: client;
  place turn: { next, granted };
  place tickets: { client, t };
}
out {
  place idle: client;
  place turn: { next, +granted };
  place tickets: { client, 0 };
};

// tilakaava "pyrkii(1)"
prop entering: 1 subset place entering;
// tilakaava "kriittinen (1)"
prop critical: 1 subset place critical;

#ifdef FAIR
// siirtymän "poistu" reiluusoletus
weakly_fair trans exit;
// siirtymien "siirry" ja "koeta" reiluusoletus
weakly_fair client_t c:
(trans enter: client == c) || (trans test: client == c);
#endif // FAIR