ex4: ConnectionClosed test flawed?

[tgp]

The ConnectionClosedMonitorTemplate in the helpers package defines the FSM

close+(c) write(c)

The tests in test.ConnectionClosed use this template, although they seem to be flawed. In testSimple, the trace should be "{C=c2}{C=c1}", because both closed connections v and v2 are being written to, the same is true for testInterleaving. In testTwoMatches the assertion seems to be OK, in testWriteFirst the trace tested should be "{C=c1}", since v is being written to after it was closed.

These three tests are the only ones that fail when running the AllTests test suite with our SymbolBasedIndexing class...

[ericbodden]

Hello.

This really depends on the semantics one gives to matching a pattern against a runtime trace. There are two different semantics, standard semantics and suffix-matching semantics MOPBox (and JavaMOP as well, actually) implement the standard semantics. This semantics states that whatever is not explicitly allowed by the pattern will not be accepted by the automaton, i.e., will not lead to a match. In the case you mention, the pattern is "close+(c) write(c)", and in particular it is not "(write(c)|close(c))* close+(c) write(c)". In other words, when reading a trace "write(v2) close(v2) write(v2)" such as in the test case, then this trace is not in the regular language defined by the regular expression "close+(c) write(c)" and therefore is not matched.

Tracematches, for example, implement a suffix-matching semantics, which arguably is more intuitive: tracematches ignore any prefix of the trace, matching against all possible suffixes. Hence, the expression "close+(c) write(c)" would match against the suffix "close(v2) write(v2)" and hence lead to a match.

The test case you mention only states "{C=c1}" in the assertion because we specifically test that MOPBox implements the "standard semantics".

For the exercise I will accept both kinds of implementation.

I hope that answers your question.