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

P

Current State

1

0

S

0 1 2

P

S

Event

2

P 1 2 2

S 2 0 2

P/S

(a) Finite state machine

(b) Table

FIGURE 8.5: Representing the Alternating template in different forms.

algorithm determines the next state by looking it up in the table. For example,
if the current state is state 0 and the event is P, the next state is state 1.
Figure 8.6 shows our inference algorithm. Figure 8.7 shows how our infer-
ence algorithm infers which of the 12 instantiations of the Alternating template
the trace ABCACBDC satisfies.
The algorithm scans a trace twice. In the first pass, it identifies all the
distinct events and creates a mapping between the event names and integer
index numbers (lines 3-13). After scanning the whole trace, the algorithm cre-
ates state , an NN array, for keeping track of the states of the instantiations
of the Alternating pattern (line 17). The value of state[i][j] corresponds to the
FSM state of the instantiation in which P is Eventi i and S is Eventi j . The
elements of this array, except the diagonal ones, are initialized to 0 since all
FSMs start in the initial state (lines 18-23). The diagonal elements are ini-
tialized to 2 (i.e., the error state) because the two events cannot be equal
(line 21). In the second pass, our algorithm rescans the execution trace (line
27). When it reads an event from the trace, it updates the state array (lines
28-34). Here the key observation is that an event, Event k , could be either the
P event or the S event. If Event k is the P event, our algorithm updates the
k-th row of the state array (line 32). If Event k is the S event, our algorithm
updates the k-th column of the state array (line 34). Our algorithm updates
the state by looking up the pre-encoded tables of the FSMs (Figure 8.5). After
scanning the trace twice, if state[i][j] is in an accepting state, our algorithm
outputs Event i ! Event j as a satisfied Alternating property (lines 37-41).
This algorithm has time complexity in (NL) and space complexity in
(N 2 ). The loop from line 11 to 13 has running time in (L): it scans the
trace once, updating the event2index mapping for each element. The loop from
line 18 to 23 has running time in (N 2 ). The loop from line 28 to 34 updates
one row and one column of the state array for each event in the trace. Hence,
the time complexity of the loop is in (NL). Finally, the loop from line 37