In the beginning, the corresponding states are developed from the informal specification. This results in a sequence control, as described in chapter 4 because the states are dynamic elements. The states remember the last result from the input signals.
The following states can be defined. Of course, different definitions can arise from informal specification. The goal is to find a formal specification to fulfil the informal specification.
The initial state (Z1) is defined as "key E3 not pressed and E1 is occupied". From Z1, "key E3" can be used to change to Z2. Z2 sets A1 to one as the output function and changes to Z3 when E2 is reached. The E3 key is used to change to Z4. In Z4, A2 is set as the output function. When position E1 is reached, Z4 changes to Z1. This results in a
the sequence is as follows:
