Assertions for
BAKERY
Reachable States
j
:
"
i: (
p
[i]
Î
{0,1}
«
y[i]=0)
Ù
"
i
¹
j: [(y[i]=y[j]
«
y[i]=0
Ù
y[j]=0)
Ù
(
p
[i]
Î
{3,4}
®
y[j]
>
y[i])]
Pending States
pend
:
p
Î
{1,2}
Ù
j
Helpful Assertions
h
k
[i]
:
Denote
a
:
p
[j]
Î
{3,4}
Ù
(
p
[j]
Î
{0,1}
®
y[j]=0)
h
k
[z]
h
k
[i], i
¹
j
k=1
p
[z]=1
Ù
y[z]=0
0
k=2
p
[z]=2
Ù
y[z]
¹
0
Ù
"
j
¹
z: (
a
Ù
y[j]
>
y[z])
p
[z]=2
Ù
y[z]
¹
0
Ù
p
[i]=2
Ù
y[i]
¹
0
Ù
"
j
¹
i: (
a
Ù
y[j]
>
y[i])
k=3
0
p
[z]=2
Ù
y[z]
¹
0
Ù
p
[i]=3
Ù
y[i]
¹
0
Ù
"
j
¹
i: (
a
Ù
y[j]
>
y[i])
k=4
0
p
[z]=2
Ù
y[z]
¹
0
Ù
p
[i]=4
Ù
y[i]
¹
0
Ù
"
j
¹
i: (
a
Ù
y[j]
>
y[i])