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" ]
;
17 dead
-> locked [
style=
dotted, label=
"locked\nafter destroy" ]
;
18 dead
-> free [
style=
dotted, label=
"unlocked\nafter destroy" ]
;
20 locked
-> free [
style=
dotted, label=
"unlocked\nby non-owner" ]
;
21 locked
-> dead [
style=
dotted, label=
"destroyed\nwhile locked" ]
;