FSM definitions

[Romeo]

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

[ericbodden]

Good morning!

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

[Romeo]

Thank you for clarifying this!

Roland