# (Bi-)simulation quotienting and model-checking

This chapter is inspired from example 7.13 in "Principles of Model-Checking"
by Joost-Pieter Katoen and Christel Baier.

## A simplified Bakery algorithm

We consider the simplified version of Lamport's Bakery algorithm for 2
processes described below.

while (TRUE) { while (TRUE) {
n1: x1 := x2 + 1; n2: x2 := x1 + 1;
w1: wait until(x2 = 0 || x1 < x2); w2: wait until(x1 = 0 || x2 < x1);
c1: ... critical section ... c2: ... critical section ...
r1: x1 := 0; r2: x2 := 0;
} }

This algorithm has an infinite state space and cannot be model-checked as
is. Our goal is to define a finite bisimulation relation over
the states of this algorithm. The resulting
quotient transition system is finite and can be used to prove the
correctness of this (simplified) Bakery algorithm.

We see from the algorthm above that the actual values of `x1`

and `x2`

are irrelevant. We only need to know if they are 0 or
not. And, if both are non zero, we also need to know whether
`x1 < x2`

or `x2 < x1`

(observe that in this
simplified algorithm, two processes cannot have the same access number).
Hence, we propose the following relation over the states of the algorithm.

(l1,l2,v1,v2) R (l1',l2',v1',v2') if:

- l1=l1' and l2=l2' (the two processes are on the same labels)
- v1=0 iff v1'=0
- v2=0 iff v2'=0
- v1 < v2 iff v1' < v2'
- v1 = v2 iff v1' = v2'

- Prove that R is a bisimulation relation over the states of the
algorithm above
- What is a state in the quotient of this algorithm by R?
- Represent the quotient of the algorithm by R
- Write a PlusCal model corresponding to the quotient of the algorithm by
R.
- Check that your PlusCal model satisfies: mutual exclusion, absence of
deadlock and absence of starvation. What can you deduce for the
(simplified) Bakery algorithm?

## Lamport's Bakery algorithm

We consider Lamport's Bakery algorithm as described in
Formal design of a distributed mutual exclusion
algorithm.

- Define a bisimulation relation R over the states of the algorithm.
- What is a state in the quotient of the algorithm by R?
- How can you represent a state in the quotient in PlusCal?
- Write a PlusCal model for the quotient of the algorithm by R
- Check that your PlusCal model satisfies: mutual exclusion, absence of
deadlock and absence of starvation. What can you deduce for
Lamport's Bakery algorithm?