Formal definition: Selmo automaton

We define the Selmo automaton as a 8-tuple:

S=(Z,Σ,Γ,δ,λ,z0,B,M)

🔹 1. Z – set of states

The finite set of all modeled States of a Selmo sequence (e.g. Init, Insert, Tension, …)

---

🔹 2. Σ – input alphabet

The set of all relevant inputs (sensors, buttons, feedback signals)

---

🔹 3. Γ – output alphabet

The set of all possible output signals (valves, motors, LEDs, etc.)

---

🔹 4. δ – transition function

δ:Z×Σ×M→Z

→ The next state is determined by:

• the current state

• the current inputs

• the memory state (mem zones)

The transition is only permitted, if:

• all S-zones fulfilled are

• no I (interlock) is violated

• CMZ (optional) reports no error

---

🔹 5. λ – output function

λ:Z→Γ∗

→ All outputs of a zone are set upon entering a state, if the zone is marked in the bit-control with S and has an output.

This corresponds to Moore logic: → Outputs depend only on the current state, not on the transition.

---

🔹 6. z0 ∈ Z – start state

The initial state of the sequence after release

---

🔹 7. B : Z×X→{0,S,I, M} – bit-control matrix

A cross-table that indicates:

• for each state z∈Z

• and each zone x ∈ X

→ which behavior applies:

• 0 = don't care

• S = expected action (control or monitoring)

• I = interlock (safety monitoring)

• M = monitoring (documentation of deviation without reaction)

---

🔹 8. M – set and state of all mem zones

M={m1,m2,...,mk}, mi∈{0,1}

→ Each mem zone is a binary memory, which is set or cleared by S in that state. → Used in the transition logic (δ) to store conditions or enable decisions.

---

🧩 Additional logical structures in the Selmo automaton

🔸 Zone system X:

Zones are typed:

• Input zones: provide states from sensors

• Output zones: activate actuators

• In-out zones: actuator + sensor (with feedback)

• Mem zones: pure logical memory

• Each zone is assigned to one or more states via bit-control

---

🔸 Interlock (I):

• As soon as a zone is associated with a state with i the current signal state is compared with the setpoint.

• In case of deviation:

  • → Sequence stop

  • → Automatic release disabled

  • → red error message in the HMI

---

🔸 Monitoring (M):

• As soon as a zone is associated with a state with M the current signal state is compared with the setpoint.

• In case of deviation:

  • → Documentation

  • → Automatic release remains enabled

  • → no error message in the HMI, but documented in history

---

🔸 Sequence-check (S):

• Controls actuators (for output/in-out)

• Expects inputs (for input/in-out)

• → State is only left when all S-zones are fulfilled

• → blue HMI marking indicates active expectation

---

🔸 Memory function (Mem):

• State sets a mem zone → m=1

• A later state resets the same mem zone → m=0

• The current value m can be monitoring and a transition condition for δ

---

🔸 Extendable by:

• CMZ (Constantly Monitoring Zones) → state-independent monitoring on three levels (sequence, hw zone, plant)

• MXIC (Manual Cross Interlock) → release conditions for manual buttons (e.g. HMI control with safety logic)

• parameter layer → modeled variables such as times, repetition counts, thresholds

---

🏁 Conclusion

The Selmo automaton is a fully formalized extended Moore automaton with:

Property	Yes / No
Deterministic states	✅
State-driven outputs	✅
Signal monitoring per state	✅
Logic for allowed transitions	✅
Automatic error detection	✅
Interlock (safety monitoring)	✅
Memory functions (mem zones)	✅
Operator guidance in the HMI	✅
Advanced diagnostic function	✅