🚀 go-pugleaf

In article <1993Jan26.154610.27454@spectrum.xerox.com> kirby@xerox.com writes:

> 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 out of different states? 

Yes.  If S is the state schema that contains the state variables 
for the subsystem modelled by the diagram,
then each bubble in the diagram represents a set of states distinguished
by some predicate on those variables.   So, bubbles labelled A and B can be 
represented by Z state schemas also:

	SA =^=  [ S  | ... predicate for state SA ... ]

	SB =^=  [ S  | ... predicate for state SB ... ]

Then the transition from A to B is simply:

	TrAB =^=  SA /\ SB'

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA