1 digraph mutex_states { 2 // States 3 free; 4 locked; 5 unlocking; 6 dead; 7 8 // Valid transitions 9 dead -> free [ label="initialized" ]; 10 free -> locked [ label="locked" ]; 11 locked -> unlocking [ label="unlocked\nby owner" ]; 12 unlocking -> free [ label="unlock completed" ]; 13 unlocking -> locked [ label="lock changed owner" ]; 14 free -> dead [ label="destroyed" ]; 15 16 // Bad transitions 17 dead -> locked [ style=dotted, label="locked\nafter destroy" ]; 18 dead -> free [ style=dotted, label="unlocked\nafter destroy" ]; 19 20 locked -> free [ style=dotted, label="unlocked\nby non-owner" ]; 21 locked -> dead [ style=dotted, label="destroyed\nwhile locked" ]; 22 } 23
