// discrete time simulation of fischer real time mutual exclusion protocol // parameters: // N = number of processes // MAX = matimal time // K1, K2 = protocol constants byte id; byte t[3] = { 255 ,255 ,255 }; process Timer { state q; init q; trans q -> q { guard t[0] != 0 && t[1] != 0 && t[2] != 0 ; effect t[0] = (t[0]-1) | ((t[0]==255)*255) ,t[1] = (t[1]-1) | ((t[1]==255)*255) ,t[2] = (t[2]-1) | ((t[2]==255)*255) ; }; } process P_0 { state NCS, try, wait, CS; init NCS; trans NCS -> try { guard id == 0; effect t[0] = 2;}, try -> wait { effect t[0] = 3, id =0 +1; }, wait -> wait { guard t[0] == 0; effect t[0] = 255;}, wait -> CS { guard t[0] == 255 && id == 0 +1; }, wait -> NCS { guard id != 0 +1 && t[0] == 255;}, CS -> NCS { effect id = 0; }; } process P_1 { state NCS, try, wait, CS; init NCS; trans NCS -> try { guard id == 0; effect t[1] = 2;}, try -> wait { effect t[1] = 3, id =1 +1; }, wait -> wait { guard t[1] == 0; effect t[1] = 255;}, wait -> CS { guard t[1] == 255 && id == 1 +1; }, wait -> NCS { guard id != 1 +1 && t[1] == 255;}, CS -> NCS { effect id = 0; }; } process P_2 { state NCS, try, wait, CS; init NCS; trans NCS -> try { guard id == 0; effect t[2] = 2;}, try -> wait { effect t[2] = 3, id =2 +1; }, wait -> wait { guard t[2] == 0; effect t[2] = 255;}, wait -> CS { guard t[2] == 255 && id == 2 +1; }, wait -> NCS { guard id != 2 +1 && t[2] == 255;}, CS -> NCS { effect id = 0; }; } system async;