CigaretteSmokers.tla A specification of the Cigarette smokers problem. This specification with some more description can be also found here