Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 262

there is a path from node i to node j, the first Eventi i must occur before the
rst Event j in the trace.
We prove the lemma by induction on l, the length of a path from node i
to node j. The base case is l = 1. In this case there is an edge from node i to
node j. According to the definition of the property graph, Eventi i ! Event j
is true. Therefore, according to the definition of the Alternating property, the
rst Event i must occur before the first Eventi j in the trace. For k > 1, assume
that the lemma holds for all l where 1 6 l < k. Next, we prove the lemma
when l = k. Suppose there is a path from node i to node j and this path's
length is k. If the next to last node on this path is node p, there is a path from
node i to node p and this path's length is k 1. According to the induction
hypothesis, the first Event i must occur before the first Eventi p in the trace. In
addition, there is an edge from node p to node j. According to the induction
hypothesis, the first Event p must occur before the first Eventi j in the trace.
As a result, the first Eventi i must occur before the first Eventi j in the trace.
Using the above lemma, we prove by contradiction that a property graph
is a DAG. If a property graph G is not a DAG, then G contains a cycle. There
must exist two nodes, i and j, such that there exists a path P from i to j
and a path P 0 from j to i. According to the above lemma, the existence of P
implies that the first Eventi i must occur before the first Eventi j in the trace.
In addition, the existence of P 0 implies the first Event j must occur before the
rst Event i in the trace, which is a contradiction. Hence, a property graph is
a DAG.
When a property graph includes Alternating properties with p AL < 1:0, it
might still be a DAG. As explained later, our chaining algorithm first checks
if a property graph (with properties whose p AL < 1:0) has any cycles. Our
algorithm only performs the chaining operation when the property graph is a
DAG. The rest of this section assumes a property graph is a DAG.
A topological number of a node in a DAG is an integer such that if there
exists an edge from node i to node j, then the topological number of node i
is less than the topological number of node j [15]. Because a property graph
is a DAG, we can sort the nodes based on their topological numbers. The
subscript of each node in Figure 8.13 indicates its topological number.
An alternating chain is a subgraph G 0 =< V 0 ;E 0 > of a property graph
G =< V;E >, where V 0 V and E 0 = f(i;j) j i;j 2 V 0 and (i;j) 2 Eg, such
that if the topological number of node i is less than the topological number
of node j, then (i;j) 2 E 0 . By definition, an edge in a property graph is a
trivial alternating chain. For example, in Figure 8.13, the subgraph consisting
of A and B is a trivial alternating chain. In addition, the subgraph consisting
of A, B, and C is an alternating chain, while the subgraph consisting of A,
B, C, and D is not an alternating chain.
A maximal alternating chain is an alternating chain G 0 =< V 0 ;E 0 > of
a property graph G =< V;E > such that 8i 2 V V 0 , G 00 =< V 00 ;E 00 > is
not an alternating chain, where V 00 = V 0 [fig and E 00 = E 0 [f(i;j) j j 2
V 0 and (i;j) 2 Eg[f(j;i) j j 2 V 0 and (j;i) 2 Eg. For example, in Figure