Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations.