Module 8 - GNI

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

Module 8 - GNI

Beitrag von franzose » 22. Jun 2012 14:30

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?

Thanks for your help!

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

Re: Module 8 - GNI

Beitrag von Sarah Ereth » 27. Jun 2012 16:34

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
BASIC-Programmierer
Beiträge: 146
Registriert: 9. Okt 2009 00:08

Re: Module 8 - GNI

Beitrag von franzose » 27. Jun 2012 18:07

Thank you very much for your reply :)

Antworten

Zurück zu „Archiv“