> 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-solution/selmo-solution-en/selmo-documentation-of-the-logic/sdea-model/formal-definition-selmo-automaton.md).

# 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  | ✅        |


---

# 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-solution/selmo-solution-en/selmo-documentation-of-the-logic/sdea-model/formal-definition-selmo-automaton.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.