State Transition Diagram

When the number of states is finite (and reasonably small), the state machine can be described by a very readable diagram. Create one bubble for each state, one arc for each transition:

state Î States
guard1 Ì Inputs
guard2 Ì Inputs
output1 Î Outputs
output2 Î Outputs

else = {x Î Inputs | x Ï guard1 È guard2 }

The else arc can be implicit if