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

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities

Other

1.25k stars 196 forks source link

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

Open ahelwer opened 6 months ago

ahelwer commented 6 months ago

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 commented 6 months ago

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.