This paper presents an analysis of the Production Cell system. We were able to model the system and verify most of its properties in Promela/SPIN. Our model is very close to the implementation level, and deriving code from it is trivial. In order to verify properties with SPIN's partial order reduction algorithms, we needed to ensure that all of our properties are closed under stuttering. We introduce the notion of logic edges and use them to show that properties of interest to us are closed under stuttering.