#Dekker's Mutual Exclusion Algorithm #Petri Net model for two processes vars X1 X9 X11 X13 X15 X2 X3 X4 X5 X6 X7 X8 X10 X12 X14 X16 X17 X18 X19 X20 X21 X22 rules X1>=1,X9>=1 -> X1'=X1-1 ,X9'=X9-1 ,X2'=X2+1 ,X10'=X10+1; X2>=1,X13>=1 -> X2'=X2-1 ,X3'=X3+1 ; X3>=1,X11>=1 -> X3'=X3-1 ,X11'=X11-1 ,X4'=X4+1 ,X12'=X12+1 ; X3>=1,X12>=1 -> X3'=X3-1 ,X4'=X4+1 ; X4>=1,X10>=1 -> X4'=X4-1 ,X10'=X10-1 ,X1'=X1+1 ,X9'=X9+1 ; X2>=1,X14>=1 -> X2'=X2-1 ,X5'=X5+1 ; X5>=1,X11>=1 -> X5'=X5-1 ,X2'=X2+1 ; X5>=1,X12>=1 -> X5'=X5-1 ,X6'=X6+1 ; X6>=1,X10>=1 -> X6'=X6-1 ,X10'=X10-1 ,X7'=X7+1 ,X9'=X9+1 ; X7>=1,X12>=1 -> ; X7>=1,X11>=1 -> X7'=X7-1 ,X8'=X8+1 ; X8>=1,X9>=1 -> X8'=X8-1 ,X9'=X9-1 ,X2'=X2+1 ,X10'=X10+1 ; X15>=1,X13>=1 -> X15'=X15-1 ,X13'=X13-1 ,X16'=X16+1 ,X14'=X14+1 ; X16>=1,X9>=1 -> X16'=X16-1 ,X17'=X17+1 ; X17>=1,X12>=1 -> X17'=X17-1 ,X12'=X12-1 ,X18'=X18+1 ,X11'=X11+1 ; X17>=1,X11>=1 -> X17'=X17-1 ,X18'=X18+1 ; X18>=1,X14>=1 -> X18'=X18-1 ,X14'=X14-1 ,X15'=X15+1 ,X13'=X13+1 ; X16>=1,X10>=1 -> X16'=X16-1 ,X19'=X19+1 ; X19>=1,X12>=1 -> X19'=X19-1 ,X16'=X16+1 ; X19>=1,X11>=1 -> X19'=X19-1 ,X20'=X20+1 ; X20>=1,X14>=1 -> X20'=X20-1 ,X14'=X14-1 ,X21'=X21+1 ,X13'=X13+1 ; X21>=1,X11>=1 -> ; X21>=1,X12>=1 -> X21'=X21-1 ,X22'=X22+1 ; X22>=1,X13>=1 -> X22'=X22-1 ,X13'=X13-1 ,X16'=X16+1 ,X14'=X14+1 ; init 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 target X3>=1,X17>=1 invariants X11 = 1, X12 = 1 X9 = 1, X10 = 1 X1 = 1, X7 = 1, X8 = 1, X10 = 1 X2 = 1, X3 = 1, X4 = 1, X5 = 1, X6 = 1, X9 = 1, X13 = 1, X14 = 1 X13 = 1, X16 = 1, X17 = 1, X18 = 1, X19 = 1, X20 = 1 X1 = 1, X2 = 1, X3 = 1, X4 = 1, X5 = 1, X6 = 1, X7 = 1, X8 = 1, X13 = 1, X14 = 1 X2 = 1, X3 = 1, X4 = 1, X5 = 1, X6 = 1, X9 = 1, X14 = 1, X15 = 1 X15 = 1, X16 = 1, X17 = 1, X18 = 1, X19 = 1, X20 = 1, X21 = 1, X22 = 1 X1 = 1, X2 = 1, X3 = 1, X4 = 1, X5 = 1, X6 = 1, X7 = 1, X8 = 1, X14 = 1, X15 = 1, X21 = 1, X22 = 1