Imprecise abstraction of observed terminal states

[GoogleCodeExporter]

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