--Dekker's Mutual Exclusion Algorithm --Petri Net model for two processes var X1, X9, X11, X13, X15, X2, X3, X4, X5, X6, X7, X8, X10, X12, X14, X16, X17, X18, X19, X20, X21, X22 : discrete; automaton p synclabs : ; initially ss & True; loc ss : while X1 >= 0 & X9 >= 0 & X11 >= 0 & X13 >= 0 & X15 >= 0 & X2 >= 0 & X3 >= 0 & X4 >= 0 & X5 >= 0 & X6 >= 0 & X7 >= 0 & X8 >= 0 & X10 >= 0 & X12 >= 0 & X14 >= 0 & X16 >= 0 & X17 >= 0 & X18 >= 0 & X19 >= 0 & X20 >= 0 & X21 >= 0 & X22 >= 0 & X11 + X12 = 1 & X9 + X10 = 1 & X1 + X7 + X8 + X10 = 1 & X2 + X3 + X4 + X5 + X6 + X9 + X13 + X14 = 2 & X13 + X16 + X17 + X18 + X19 + X20 = 1 & X1 + X2 + X3 + X4 + X5 + X6 + X7 + X8 + X13 + X14 = 2 & X2 + X3 + X4 + X5 + X6 + X9 + X14 + X15 = 2 & X15 + X16 + X17 + X18 + X19 + X20 + X21 + X22 = 1 & X1 + X2 + X3 + X4 + X5 + X6 + X7 + X8 + X14 + X15 + X21 + X22 = 2 wait {} when X1 >= 1 & X9 >= 1 do { X1' = X1 - 1 , X9' = X9 -1 , X2' = X2 + 1 , X10' = X10 + 1 } goto ss; when X2 >= 1 & X13 >= 1 do { X2' = X2 - 1 , X3' = X3 + 1 } goto ss; when X3 >= 1 & X11 >= 1 do { X3' = X3 - 1 , X11' = X11 - 1 , X4' = X4 + 1 , X12' = X12 + 1 } goto ss; when X3 >= 1 & X12 >= 1 do { X3' = X3 - 1 , X4' = X4 + 1 } goto ss; when X4 >= 1 & X10 >= 1 do { X4' = X4 - 1 , X10' = X10 - 1 , X1'=X1+1 , X9'=X9+1 } goto ss; when X2 >= 1 & X14 >= 1 do { X2' = X2 - 1 , X5' = X5 + 1 } goto ss; when X5 >= 1 & X11 >= 1 do { X5' = X5 - 1 , X2' = X2 + 1 } goto ss; when X5 >= 1 & X12 >= 1 do { X5' = X5 - 1 , X6' = X6 + 1 } goto ss; when X6 >= 1 & X10 >= 1 do { X6' = X6 - 1 , X10' = X10 - 1 , X7' = X7 + 1 , X9' = X9 + 1 } goto ss; when X7 >= 1 & X11 >= 1 do { X7' = X7 - 1 , X8' = X8 + 1 } goto ss; when X8 >= 1 & X9 >= 1 do { X8' = X8 - 1 , X9' = X9 - 1 , X2' = X2 + 1 , X10' = X10 + 1 } goto ss; when X15 >= 1 & X13 >= 1 do { X15' = X15 - 1 , X13' = X13 - 1 , X16' = X16 + 1 , X14' = X14 + 1 } goto ss; when X16 >= 1 & X9 >= 1 do { X16' = X16 - 1 , X17' = X17 + 1 } goto ss; when X17 >= 1 & X12 >= 1 do { X17' =X17 - 1 , X12' = X12 - 1 , X18' = X18 + 1 , X11' =X11 + 1 } goto ss; when X17 >= 1 & X11 >= 1 do { X17' = X17 - 1 , X18' = X18 + 1 } goto ss; when X18 >= 1 & X14 >= 1 do { X18' = X18 - 1 , X14' = X14 - 1 , X15' = X15 + 1 , X13' = X13 + 1 } goto ss; when X16 >= 1 & X10 >= 1 do { X16' = X16 - 1 , X19' = X19 + 1 } goto ss; when X19 >= 1 & X12 >= 1 do { X19' = X19 - 1 , X16' = X16 + 1 } goto ss; when X19 >= 1 & X11 >= 1 do { X19' = X19 - 1 , X20' = X20 + 1 } goto ss; when X20 >= 1 & X14 >= 1 do { X20' = X20 - 1 , X14' = X14 - 1 , X21' = X21 + 1 , X13' = X13 + 1 } goto ss; when X21>=1 & X12>=1 do { X21' = X21 - 1 , X22' = X22 + 1 } goto ss; when X22 >= 1 & X13 >= 1 do { X22' = X22 - 1 , X13' = X13 - 1 , X16' = X16 + 1 , X14' = X14 + 1 } goto ss; end var init_reg, final_reg, reached : region; init_reg := X1=1 & X9=1 & X11=1 & X13=1 & X15=1 & X2=0 & X3=0 & X4=0 & X5=0 & X6=0 & X7=0 & X8=0 & X10=0 & X12=0 & X14=0 & X16=0 & X17=0 & X18=0 & X19=0 & X20=0 & X21=0 & X22=0; final_reg := X3>=1 & X17>=1; reached := reach backward from final_reg endreach; if empty(reached & init_reg) then print reached; prints "=================================== "; prints "SAFETY HOLD!"; prints "=================================== "; else print reached; prints " "; prints "SAFETY DOES NOT HOLD!"; endif;