-- BAKERY protocol, 2 processes -- MP 26/11/2007 var a, -- P1's counter b, -- P2's counter c -- P3's counter : discrete; -- -------------------------------------------------------------- *) automaton p1 synclabs : ; initially s_think & True; loc s_think: while a>=0 & b>=0 & c>=0 wait {} when b>c do {a' = b+1} goto s_wait; when c>=b do {a' = c+1} goto s_wait; loc s_wait: while a>=0 & b>=0 & c>=0 wait {} when b>a & c>a goto s_use; when b>a & c=0 goto s_use; when c>a & b=0 goto s_use; when b=0 & c=0 goto s_use; loc s_use: while a>=0 & b>=0 & c>=0 wait {} when True do {a' =0} goto s_think; end automaton p2 synclabs : ; initially s_think & True; loc s_think: while a>=0 & b>=0 & c>=0 wait {} when a>c do {b' = a+1} goto s_wait; when c>=a do {b' = c+1} goto s_wait; loc s_wait: while a>=0 & b>=0 & c>=0 wait {} when a>b & c>b goto s_use; when a>b & c=0 goto s_use; when c>b & a=0 goto s_use; when a=0 & c=0 goto s_use; loc s_use: while a>=0 & b>=0 & c>=0 wait {} when True do {b' =0} goto s_think; end automaton p3 synclabs : ; initially s_think & True; loc s_think: while a>=0 & b>=0 & c>=0 wait {} when a>b do {c' = a+1} goto s_wait; when b>=a do {c' = b+1} goto s_wait; loc s_wait: while a>=0 & b>=0 & c>=0 wait {} when a>c & b>c goto s_use; when a>c & b=0 goto s_use; when b>c & a=0 goto s_use; when a=0 & b=0 goto s_use; loc s_use: while a>=0 & b>=0 & c>=0 wait {} when True do {c' =0} goto s_think; end -- var init_reg, final_reg, final_reg1, final_reg2, final_reg3, reached : region; init_reg:= loc[p1] = s_think & loc[p2] = s_think & loc[p3] = s_think & a=0 & b=0 & c=0; final_reg1:= loc[p1] = s_use & loc[p2] = s_use; final_reg2:= loc[p1] = s_use & loc[p3] = s_use; final_reg3:= loc[p2] = s_use & loc[p3] = s_use; final_reg:= final_reg1 | final_reg2 | final_reg3; reached:= reach backward from final_reg endreach; if empty(reached & init_reg) then prints "mutual exclusion holds!"; print reached; else prints "mutual exclusion does NOT hold!"; endif; --reached:= reach forward from init_reg endreach; --if empty(reached & final_reg) -- then prints "Target not reached (safety holds!)"; -- print reached; -- else prints "Target reached (safety does not hold!)"; -- endif;