More work on PROMELA transformation