Hi Stephan, yes it was my fault. I misinterpreted an error message and while reading some articles I also got a wrong impression of how powerful TLA+s invariants are. Anyhow, thanks for your reply which encouraged me to have a second look at my example :) Cheers, Stefan