FSM definitions

Moderator: Automated Software Engineering

Romeo
Erstie
Erstie
Beiträge: 12
Registriert: 16. Nov 2011 10:03

FSM definitions

Beitrag von Romeo » 9. Dez 2011 07:19

Good morning,

I have some questions concerning the definition of the FSMs for Exercise 4:

In the HasNextMonitorTemplate class, I think the regular expression
<code>create(c,i) update(c)* iter(i)+ update(c)+ iter(i)</code>
mirrors the "FailSafeIter" contract.

Furthermore - concerning the same class - I'm confused why we allow for an unchecked "next" operation from the initial to the middle state. I understand that - in the general case - this state represents the situation when we have called "hasNext" and are therefore sure to be able to call "next", but when we start the iterator we did not necessarily call "hasNext" which would fail if the collection being iterated over is empty.

Code: Alles auswählen

initial.addTransition(getSymbolByLabel(Next), middle);
And why do we allow the machine to return from the error state?

Code: Alles auswählen

error.addTransition(getSymbolByLabel(HasNext), initial);
This goes against my intuition, that we cannot make an unchecked "next" undone by calling the "hasNext" method afterwards, especially because
we may have looped in the error state due to several "next" events.

Best regards
Roland

Benutzeravatar
ericbodden
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 243
Registriert: 5. Apr 2010 19:06

Re: FSM definitions

Beitrag von ericbodden » 9. Dez 2011 09:58

Good morning!
Romeo hat geschrieben: In the HasNextMonitorTemplate class, I think the regular expression
<code>create(c,i) update(c)* iter(i)+ update(c)+ iter(i)</code>
mirrors the "FailSafeIter" contract.
This is a copy/paste mistake on my side. This should rather read "next(i) next(i)" (over an alphabet {next(i), hasNext(i)}.

Furthermore - concerning the same class - I'm confused why we allow for an unchecked "next" operation from the initial to the middle state. I understand that - in the general case - this state represents the situation when we have called "hasNext" and are therefore sure to be able to call "next", but when we start the iterator we did not necessarily call "hasNext" which would fail if the collection being iterated over is empty.
This is also correct, however, I did this on purpose. The property as described (i.e., "next next") has been used several times in the literature. Surely, a more realistic property description should not allow "next" to be called in the beginning of the trace, and one could always define an appropriate monitor template if wanted.

Code: Alles auswählen

initial.addTransition(getSymbolByLabel(Next), middle);
And why do we allow the machine to return from the error state?

Code: Alles auswählen

error.addTransition(getSymbolByLabel(HasNext), initial);
This goes against my intuition, that we cannot make an unchecked "next" undone by calling the "hasNext" method afterwards, especially because
we may have looped in the error state due to several "next" events.

Best regards
Roland
Good question as well. The semantics of MOPBox (and also all other monitoring tools I am aware of) is that the error handler is called whenever entering the error state. In other words, if the program violates the property repeatedly, then, due to the current structure of the automaton, the error state will be reached repeatedly, and therefore an error message will be shown at each violating event. Again, this is a design decision. One could omit these extra "back" edges, which would then result in a monitor that only issues an error message on the first violation.

Hope that helps,
Eric
-- Eric

Romeo
Erstie
Erstie
Beiträge: 12
Registriert: 16. Nov 2011 10:03

Re: FSM definitions

Beitrag von Romeo » 9. Dez 2011 13:47

Thank you for clarifying this!

Roland

Antworten

Zurück zu „Automated Software Engineering“