## Module 8 - GNI

franzose
BASIC-Programmierer
Beiträge: 146
Registriert: 9. Okt 2009 00:08

### Module 8 - GNI

In the lecture I think Prof. Mantel provided a formal definition of GNI like this:

$$\forall \tau \in Tr. \forall \alpha',\beta' \in E^*. (\exists \alpha, \beta \in E^*: \tau = \alpha.\beta \land \alpha' = \alpha \land \beta'_{|E \setminus (H \cap I)} = \beta_{|E \setminus (H \cap I)}) \Rightarrow (\exists \alpha'',\beta'' \in E^*: \alpha''.\beta'' \in Tr \land \alpha' = \alpha'' \land \beta'_{|(H \cap I) \cup L} = \beta''_{|(H \cap I) \cup L})$$

However I don't think that this formula captures the intuition of "after the first changed input" correctly.

If we take the example of $$SES_A$$ on slide 59, it is stated that while $$\langle 1, 2, 1, 3, stop, ev_A \rangle \in Tr$$ is a valid one, the trace $$\langle 1, 2, 3, 1, stop, ev_A \rangle \in Tr$$ is not a permissible correction of the perturbation $$\langle 1, 2, 1, stop, ev_A \rangle$$ of $$\langle 1, 2, stop, ev_A \rangle$$, because it adds the high output event 3 BEFORE the first change high input event 1.

But in the formula above, we could set $$\alpha' = \alpha = \alpha'' = \langle 1, 2 \rangle$$ and $$\beta' = \langle 1, stop, ev_A \rangle$$, $$\beta = \langle stop, ev_A \rangle$$ and $$\beta'' = \langle 3, 1, stop, ev_A \rangle$$, such that the formula is fulfilled.

So is the formula wrong or am I missunderstanding something?

Sarah Ereth
Neuling
Beiträge: 9
Registriert: 14. Feb 2011 16:16

### Re: Module 8 - GNI

Yes, I aggree with you that your choice of a valuation does not provide a counterexample to the satisfaction of the formula.

Furthermore, I also agree with you that the formula is not as restrictive as the informal description. You can find an alternative formal definition in the solution to Exercise 10.5.b) and finally, i.e. in the next lecture, you will see a satisfactory formal definition of GNI using MAKS

franzose
BASIC-Programmierer
Beiträge: 146
Registriert: 9. Okt 2009 00:08