// Petersonin algoritmi keskinäiselle poissulkevuudelle // Verkon graafinen kuvaus löytyy laskuharjoituksen 3 vastauksista // Käytetään mustan tokenin tyyppinä tyhjää structia. Mikä tahansa tyyppi // jolla on tasan 1 mahdollinen arvo käy. typedef struct {} token_t; typedef unsigned (0..1) var_t; // Paikat prosessille 0 place ncs0 (0..1) token_t : {}; place p01 (0..1) token_t; place p02 (0..1) token_t; place cs0 (0..1) token_t; // Paikat prosessille 1 place ncs1 (0..1) token_t : {}; place p11 (0..1) token_t; place p12 (0..1) token_t; place cs1 (0..1) token_t; // Paikat muuttujille place in0 (1) var_t : 0; place turn (1) var_t : 0; place in1 (1) var_t : 0; trans t01 in { place ncs0 : {}; place in0 : i; } out { place p01 : {}; place in0 : 1; }; trans t02 in { place p01 : {}; place turn : t; } out { place p02 : {}; place turn : 1; }; trans t03 in { place p02 : {}; place turn : t; place in1 : i; } out { place cs0 : {}; place turn : t; place in1 : i; } gate t == 0 || i == 0; trans t04 in { place cs0 : {}; place in0 : i; } out { place ncs0 : {}; place in0 : 0; }; trans t11 in { place ncs1 : {}; place in1 : i; } out { place p11 : {}; place in1 : 1; }; trans t12 in { place p11 : {}; place turn : t; } out { place p12 : {}; place turn : 0; }; trans t13 in { place p12 : {}; place turn : t; place in0 : i; } out { place cs1 : {}; place turn : t; place in0 : i; } gate t == 1 || i == 0; trans t14 in { place cs1 : {}; place in1 : i; } out { place ncs1 : {}; place in1 : 0; }; // Tarkastetaan keskinäisen poissulkevuuden toteutuminen // fakta-siirtymällä // Voitaisiin tehdä myös rejectillä trans fakta in { place cs0 : {}; place cs1 : {}; } gate fatal;