> For the complete documentation index, see [llms.txt](https://infosys.selmotech.com/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://infosys.selmotech.com/selmo-dokumentation-der-logik/sdea-modell/formale-definition-selmo-automat.md).

# Formale Definition: Selmo-Automat

Wir definieren den **Selmo-Automaten** als ein **8-Tupel**:

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

#### 🔹 1. Z – Zustandsmenge

Die endliche Menge aller modellierten **Zustände** einer Selmo-Sequence\
(z. B. Init, Einlegen, Spannen, …)

***

#### 🔹 2. Σ – Eingabealphabet

Die Menge aller **relevanten Eingaben** (Sensoren, Taster, Rückmeldesignale)

***

#### 🔹 3. Γ – Ausgabealphabet

Die Menge aller **möglichen Ausgangssignale** (Ventile, Motoren, LEDs, etc.)

***

#### 🔹 4. δ – Übergangsfunktion

δ:Z×Σ×M→Z

→ Der **nächste Zustand** wird bestimmt durch:

* den aktuellen Zustand
* die aktuellen Eingaben
* den Speicherzustand (Mem-Zonen)

Die Transition ist **nur zulässig**, wenn:

* alle `S`-Zonen **erfüllt** sind
* kein I (Interlock) verletzt ist
* CMZ (optional) keinen Fehler meldet

***

#### 🔹 5. λ – Ausgabefunktion

λ:Z→Γ∗

→ Alle **Ausgänge einer Zone werden bei Eintritt in einen Zustand gesetzt**, wenn die Zone in der Bit-Control mit `S` versehen ist und einen Ausgang besitzt.

Dies entspricht der **Moore-Logik**:\
→ **Outputs hängen nur vom aktuellen Zustand ab**, nicht vom Übergang.

***

#### 🔹 6. z0 ∈ Z  – Startzustand

Der initiale Zustand der Sequenz nach Freigabe

***

#### 🔹 7. B : Z×X→{0,S,I, M} – Bit-Control-Matrix

Eine Kreuztabelle, die angibt:

* für jeden Zustand z∈Zz 
* und jede Zone x ∈ X

→ welches Verhalten gilt:

* `0` = don't care
* `S` = erwartete Aktion (Steuerung oder Überwachung)
* `I` = Interlock (Sicherheitsüberwachung)
* M = Monitoring (Dokumentation der Abweichung ohne Reaktion)

***

#### 🔹 8. M – Menge und Zustand aller Mem-Zonen

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

→ Jede Mem-Zone ist ein **binärer Speicher**, der durch `S` im Zustand gesetzt oder gelöscht wird.\
→ Wird in der Übergangslogik (δ) verwendet, um Bedingungen zu speichern oder Entscheidungen zu ermöglichen.

***

### 🧩 Weitere logische Strukturen im Selmo-Automaten

#### 🔸 Zonensystem X:

Zonen sind typisiert:

* **Input-Zonen**: liefern Zustände aus Sensoren
* **Output-Zonen**: aktivieren Aktoren
* **In-Out-Zonen**: Aktor + Sensor (mit Feedback)
* **Mem-Zonen**: reine logische Speicher
* Jede Zone ist einer oder mehreren Zuständen per Bit-Control zugeordnet

***

#### 🔸 Interlock (I):

* Sobald eine Zone im Zustand mit `i` verknüpft ist, wird der aktuelle Signalzustand mit dem Sollwert verglichen.
* Bei Abweichung:
  * → **Sequenzstopp**
  * → **Automatik-Release deaktiviert**
  * → **rote Fehlermeldung im HMI**

***

#### 🔸 Monitoring (M):

* Sobald eine Zone im Zustand mit `M` verknüpft ist, wird der aktuelle Signalzustand mit dem Sollwert verglichen.
* Bei Abweichung:
  * → Dokumentation
  * → **Automatik-Release bleibt erhalten**
  * → **kein Fehlermeldung im HMI, aber dokumentiert in Historie**

***

#### 🔸 Sequence-Check (S):

* Steuert Aktoren (bei Output/In-Out)
* Erwartet Eingaben (bei Input/In-Out)
* → **Zustand wird erst verlassen, wenn alle `S`-Zonen erfüllt sind**
* → **blaue HMI-Markierung zeigt aktive Erwartung**

***

#### 🔸 Speicherfunktion (Mem):

* Zustand setzt eine Mem-Zone → m=1
* Späterer Zustand setzt dieselbe Mem-Zone wieder zurück → m=0
* Der aktuelle Wert m kann Überwachung und Übergangsbedingung für δ sein

***

#### 🔸 Erweiterbar um:

* **CMZ (Constantly Monitoring Zones)** → zustandsunabhängige Überwachung auf drei Ebenen (Sequence, HW-Zone, Plant)
* **MXIC (Manual Cross Interlock)** → Freigabebedingungen für Handtasten (z. B. HMI-Steuerung mit Sicherheitslogik)
* **Parameter-Layer** → modellierte Variablen wie Zeiten, Wiederholzahlen, Schwellenwerte

***

### 🏁 Fazit

Der **Selmo-Automat ist ein vollständig formalisierter erweiterter Moore-Automat** mit:

| Eigenschaft                        | Ja / Nein |
| ---------------------------------- | --------- |
| Deterministische Zustände          | ✅         |
| Zustandsgesteuerte Ausgänge        | ✅         |
| Signalüberwachung pro Zustand      | ✅         |
| Logik für erlaubte Übergänge       | ✅         |
| Automatische Fehlererkennung       | ✅         |
| Interlock (Sicherheitsüberwachung) | ✅         |
| Speicherfunktionen (Mem-Zonen)     | ✅         |
| Bedienerführung im HMI             | ✅         |
| Erweiterte Diagnosefunktion        | ✅         |


---

# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.

## Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter:

```
GET https://infosys.selmotech.com/selmo-dokumentation-der-logik/sdea-modell/formale-definition-selmo-automat.md?ask=<question>&goal=<endgoal>
```

`ask` is the immediate question: it should be specific, self-contained, and written in natural language.
`goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal.

The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.