// Owner of a lock (0=vapaa, 1..n=jokin prosessi) typedef unsigned (0..2) owner_t; // The number of a process (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; place idle (0..#client_t) client_t: client_t client: client; place pending (0..#client_t) client_t; place testing (0..#client_t) client_t; place critical (0..1) client_t; place turn (1) turn_t: 0 && is client_t t == granted)#client; place turn: { next, granted }; place tickets: { client, t }; }; 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 }; }; #ifdef FAIR // A fairness assumption for transition exit weakly_fair trans exit; // A fairness assumption for transitions enter and test weakly_fair client_t c: (trans enter: client == c) || (trans test: client == c); #endif // FAIR