🚀 go-pugleaf

I am a new user to Z.  I've picked up most of the syntax.  But I have some questions
about how to go about applying it.  One of the most useful features of your 
traditional design and analysis methodologies (like rumbaugh, shlaer/mellor, etc..) is
the state-transition diagram.  Is there a way in Z to model not only the
states, but the transitions into and outof different states?  It would be
nice if I could specify states, and then when  I specify my member functions
I can describe the state that this function is valid for. 

I am using the Object-Z Specification descripted in TR91-1 from Duke et al.
Is there a newer specification that is available?  

Thanks,
Mike Kirby
Xerox Corp
E-mail: kirby.roch803@xerox.com

Refs:

Roger King, et al., "The Object-Z Specification Language, Version 1,"  Technical
Report 91-1, University of Queensland, Queensland Australia, May 1991