The consistent observed FSM states strategy (i.e., where two states in
different traces with identical event histories are considered equivalent) runs
into issues when one of the states is non-terminal and another state is
terminal. The current strategy is to accumulate the terminal flag, that is we
assume that a process can terminate at a state if this state was ever observed
to be a terminal in any of the input traces.
Unfortunately, this strategy is insufficient to handle even simple cases that
we haven't seen until now. Here is an example input log that cannot be parsed
because the cross-product-based system state that is generated is considered
terminal (due to the accumulation described above), while the channel contents
associated with the state are non-empty. This is a problem because all terminal
traces (observed, or synthetic) must terminate with empty channels.
Log:
1,0 M!a
1,1 M?a
--
1,0 M!a
1,1 M?a
2,0 M!a
2,2 M?a
Base args (omitting -o and --mcPath):
-r ^(?<VTIME>)(?<TYPE>)$
-s ^--$
-q M:0->1
Another way of seeing the problem is that consistent observed FSM states
allowed us to perform efficient trace stitching. However, in the log above this
leads to stitching the trace at process 2 in trace 1 (i.e., M?a) with the trace
at process 1 in trace 2 (i.e., M!a, M!a). This leads to an abstract terminal
(cross-product) state that contains an "a" in the channel.
There are two solutions to this issue, both requiring significant code change.
1. Treat terminal and non-terminal states with identical histories as different
states, thus avoiding accumulating the terminal flag -- the root of the problem.
2. Create an exemption post-processing state that makes states as non-terminal
if the associated channels are non-empty (the exemption is necessary to not
outright remove these branches).
3. Ignore the generated inconsistent states altogether.
Re 1: Insufficient to solve the problem during the cross-product phase. Even
for the log above, we'll get branches that need to be removed in a
post-processing stage.
Re 2: The exemption step is non-trivial -- it's not clear when to apply it and
when to not apply it (and delete the entire branch). This partly depends on
whether or not the branch contains a unique trace (with proper termination).
Re 3: Easiest solution, but limits generalization. For the trace above this
would result in eliminating partial orders of the second trace that are
legitimate. This may cripple CFSM construction.
Original issue reported on code.google.com by bestchai on 7 Aug 2014 at 3:23
Original issue reported on code.google.com by
bestchaion 7 Aug 2014 at 3:23