Zu Beginn werden aus der informellen Spezifikation die entsprechenden Zustände erarbeitet. Dadurch ergibt sich eine Ablaufsteuerung, weil es sich durch die Zustände um dynamische Elemente handelt. Die Zustände merken sich das letzte Ergebnis aus den Eingangssignalen.
Folgende Zustände können definiert werden. Es können natürlich verschiedene Definitionen aus der informellen Spezifikation entstehen. Das Ziel ist eine formale Spezifikation zur Erfüllung der informellen Spezifikation zu finden.
Als Anfangszustand (Z1)wird festgelegt „Taste E3 nicht gedrückt und E1 ist belegt“. Aus dem Z1 kann mit der „Taste E3“ in den Z2 gewechselt werden. Z2 setzt als Ausgangsfunktion A1 auf eins und wechselt bei erreichen von E2 in Z3. Mit der Taste E3 wird in Z4 gewechselt. In Z4 wird in der Ausgangsfunktion A2 gesetzt. Bei erreichen der Position E1 wechselt Z4 in Z1. Dadurch ergibt sich ein
Ablauf der wie folgt lautet:
