Bakery-Boulangerie specs don't satisfy `DeadlockFree` or `StarvationFree` liveness properties

[ahelwer]

I've been defining models as part of work on #107. Currently these properties fail so these specs can only be subject to safety checking. Some fairness assumptions are required for the properties to be satisfied. @muenchnerkindl any idea what those fairness assumptions would be? The one in Spec is insufficient.

[ahelwer]

Although it's only really possible to model-check Boulanger.tla with a state constraint, because action e3 increments a natural number without bound. So liveness checking is restricted to Bakery.tla.