Use the \nparallel invariants to constrain initial partitioning

[GoogleCodeExporter]

Even though we do not explicitly use the \parallel and \nparallel invariants in 
the check/refine loop, we can use these invariants to create a more accurate 
model.

In particular, we can use these invariants to improve our initial partitioning. 
For example, let's say we have two observed states s_1 and s_2 that emit events 
e_1 and e_2, respectively. And, we mined the invariant e_1 \nparallel e_2. 
Then, we know that s_1 and s_2 should _not_ be mapped to the same partition. If 
they were, then e_1 and e_2 would be concurrent and therefore violate the mined 
invariant.

This observation should be used to constrain the initial partitioning.

We can also apply the above reasoning to \parallel, and to absence of 
\nparallel and \parallel invariants. Unfortunately, the model constraints are 
more complex in these cases and are beyond the scope of this Issue.

Original issue reported on code.google.com by bestchai on 25 Sep 2012 at 2:29

[GoogleCodeExporter]

More generally, for each of the initial partitions we can build a
graph to encode whether or not the events in the partition can in fact
be emitted by the same partition. For a partition P we build a graph
that we call harmony(P) in which each event e^i_j emitted by state
s^i_j (corresponding to process i) that is mapped to partition P is
represented as a single node, which we refer to using the event
notation e^i_j. We construct harmony(P) as follows:

- Events from the same process form a clique (complete sub-graph) in
  harmony(P). That is, \forall i,j1,j2 e^i_j1 has an edge to e^i_j2 in
  harmony(P), since e^i_j1 and e^i_j2 occur at the same process and
  are allowed to be emitted by P.

- Events from different processes have an edge between them iff the
  events were found to be concurrent in the log. That is, \forall
  i1,i2,j1,j2 e^i1_j1 has an edge to e^i2_j2 in harmony(P) iff the
  invariant (e^i1_j1 \parallel e^i2_j2) was mined from the input log.

Once we have constructed harmony(P), we can use this graph to further
partition P into P1,...,Pn such that each Pi contains states from P
that correspond to a set of events Ei which map to a clique in
harmony(P), and the set of states in the new partitions must union up
to the set of states in P. To generate such a sub-partitioning, we
need to solve the clique cover problem for harmony(P).

Original comment by bestchai on 7 Oct 2012 at 12:14