<< Click to Display Table of Contents >> Navigation: Welcome to Selmo > Method > The control example > Formal specifications > Finite automata as a state graph |
At the beginning, the corresponding states are developed from the informal specification. This results in sequence control 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 the informal specification. The aim is to find a formal specification to fulfill the informal specification.
The initial state (Z1) is defined as "Button E3 not pressed and E1 is occupied". You can switch from Z1 to Z2 by pressing "button E3". Z2 sets A1 to one as the initial function and changes to Z3 when E2 is reached. The E3 button is used to switch to Z4. The output function A2 is set in Z4. When position E1 is reached, Z4 changes to Z1. This results in a
sequence which is as follows: