## 3 Specification Mining Based on the OPTICS Clustering Algorithm and Model Checking
### FSA Refinement Based on Model Checking
If so, \(FindErrTr\) returns the set _Trans_ of error segments in the FSA according to the type of violated property as follows:  
```
Input:\(D=(Q,\Sigma,\delta,\)\(q_{0},F)\), \(K=\{K_{1},\)\(\dots,K_{l}\}\) Output:\(D^{\prime}\)= \((Q^{\prime},\Sigma,\delta^{\prime},\)\(q_{0},F)\)
1 Initialize:\(num=0\), \(times=0\), \(D^{\prime}=D\);
2 while\(times++<T\) and there exists a property \(K_{j}\in K\) violated by \(D^{\prime}\)do
3\(Trans=FindErrTr(K_{j},D^{\prime})\);
4 forach\(\langle SM,q_{2},m_{2},q_{3},MS\rangle\in\)\(Trans\)do
5 if\(K_{j}\) is \(NIF(a,b)\)then
6 Delete \(\delta^{\prime}\) (\(q_{2},m_{2}\)) = \(q_{3}\);
7\(Q^{\prime}=Q^{\prime}\cup\{C^{\prime}_{num}\}\);
8 Add transition rules to \(\delta^{\prime}\): \(\delta^{\prime}\) (\(q_{2},\)\(m_{2}\)) = \(C^{\prime}_{num}\) and \(\delta^{\prime}\) (\(C^{\prime}_{num}\), \(m_{3}\)) = \(q4\) for each \(\langle m_{3},q_{4}\rangle\in MS\);
9\(num=num+1\);
10
11 end if
12 if\(K_{j}\) is \(AIP(a,b)\)then
13 Delete \(\delta^{\prime}\) (\(q_{2},\)\(m_{2}\)) = \(q_{3}\);
14 Add transition rules to \(\delta^{\prime}\): \(\delta^{\prime}\) (\(q_{1},\)\(m_{1}\)) = \(C^{\prime}_{num}\) for each \(\langle q_{1},m_{1}\rangle\in SM\);
15\(num=num+1\);
16\(Q^{\prime}=Q^{\prime}\cup\{C^{\prime}_{num}\}\);
17 Add transition rules to \(\delta^{\prime}\): \(\delta^{\prime}\) (\(C^{\prime}_{num-1}\), \(a\)) = \(C^{\prime}_{num}\) and \(\delta^{\prime}\) (\(C^{\prime}_{num}\), \(m_{2}\)) = \(q_{3}\);
18\(num=num+1\);
19
20 end if
21 if\(K_{j}\) is \(AIF(a,b)\)then
22 Delete \(\delta^{\prime}\) (\(q_{2},\)\(m_{2}\)) = \(q_{3}\) ;
23\(Q^{\prime}=Q^{\prime}\cup\{C^{\prime}_{num}\}\);
24 Add a transition rule to \(\delta^{\prime}\): \(\delta^{\prime}\) (\(q_{2},\)\(m_{2}\)) = \(C^{\prime}_{num}\);
25\(num=num+1\);
26\(Q^{\prime}=Q^{\prime}\cup\{C^{\prime}_{num}\}\);
27 Add transition rules to \(\delta^{\prime}\): \(\delta^{\prime}\) (\(C^{\prime}_{num-1}\), \(b\)) = \(C^{\prime}_{num}\) and \(\delta^{\prime}\) (\(C^{\prime}_{num}\), \(m_{3}\)) = \(q_{4}\) for each \(\langle m_{3},q_{4}\rangle\in MS\);
28\(num=num+1\);
29
30 end if
31\(D^{\prime}\) = \((Q^{\prime},\Sigma,\delta^{\prime},q_{0},F)\);
32
33 end if
```  
**Algorithm 2** Refinement Process  
If the violated property is \(NIF(a,b)\), it returns all segments \(\langle SM,q_{2},m_{2},q_{3}\), \(MS\rangle\) that satisfy \(m_{2}=a,\delta^{\prime}(q_{2},a)=q_{3}\), \(SM\) containing all tuples \(\langle q_{1},m_{1}\rangle\) satisfying \(\delta^{\prime}(q_{1},m_{1})=\)  
Figure 5: FSA refinement method based on model checking. \(q_{2}\), \(MS\) containing all tuples \(\langle m_{3},q_{4}\rangle\) satisfying \(\delta^{\prime}(q_{3},m_{3})=q_{4}\), and there is \(\langle m^{\prime}_{3},q^{\prime}_{4}\rangle\in MS\) satisfying \(m^{\prime}_{3}=b\);
2. If the violated property is \(AIP(a,b)\), it returns all segments \(\langle SM,q_{2},m_{2},q_{3},\,MS\rangle\) that satisfy \(m_{2}=b\), \(\delta^{\prime}(q_{2},b)=q_{3}\), \(MS\) containing all tuples \(\langle m_{3},q_{4}\rangle\) satisfying \(\delta^{\prime}(q_{3},m_{3})=q_{4}\), \(SM\) containing all tuples \(\langle q_{1},m_{1}\rangle\) satisfying \(\delta^{\prime}(q_{1},m_{1})=q_{2}\), and for each \(\langle q_{1},m_{1}\rangle\in SM\), \(m_{1}\
eq a\);
3. If the violated property is \(AIF(a,b)\), it returns all segments \(\langle SM,q_{2},m_{2},q_{3},\,MS\rangle\) that satisfy \(m_{2}=a,\delta^{\prime}(q_{2},a)=q_{3}\), \(SM\) containing all tuples \(\langle q_{1},m_{1}\rangle\) satisfying \(\delta^{\prime}(q_{1},m_{1})=q_{2}\), \(MS\) containing all tuples \(\langle m_{3},q_{4}\rangle\) satisfying \(\delta^{\prime}(q_{3},m_{3})=q_{4}\), and for each \(\langle m_{3},q_{4}\rangle\in MS\), \(m_{3}\
eq b\). Further, we refine the FSA with different refinement rules depending on the type of formula that the error segment \(\langle SM,q_{2},m_{2},q_{3},MS\rangle\) violates as follows:  
1. If it violates \(NIF(a,b)\), \(m_{2}=a\), we first delete the transition rule from state \(q_{2}\) to state \(q_{3}\) using method \(a\), so that the traces violating \(NIF(a,b)\) are removed (Line 6).