1digraph 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