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