Algorithm 1 AGR
1: function AGL∗
2:
//Membership Queries
3:
Let t2 ∈ (αM
i
2 )
∗ .
4:
if t2 ∈ T (M
i
2 ) then
5:
if M1||t2 P then
6:
Let t ∈ (M1||t2) × P be an error trace.
t is a cex proving M1||M
i
2 P
7:
REPAIR(M
i
2 , t)
8:
else
M1||t2 P
9:
Return to AGL∗ in Line 2 with t2 ∈ T (A
i
j ).
10:
else
t2 /
∈ T (M
i
2 )
11:
Return to AGL∗ in Line 2 with t2 /
∈ T (A
i
j ).
12:
//Equivalence Queries
13:
Let A
i
j be the candidate assumption generated by the learner.
14:
if M1||A
i
j P then
15:
if T (M
i
2 ) ⊆ T (A
i
j ) then
16:
Terminate and return M1||M
i
2 P .
17:
else
18:
Let t2 ∈ T (M
i
2 ) \ T (A
i
j ).
19:
Set j := j + 1
20:
Return to AGL∗ in Line 2 with t2 ∈ T (A
i
j ).
21:
else
M1||A
i
j P
22:
let t ∈ (M1||A
i
j ) × P be an error trace, and denote t = (t1||tA) × tP .
23:
if tA ∈ T (M
i
2 ) then
24:
REPAIR(M
i
2 , tA)
tA is a cex proving M1||M
i
2 P
25:
else
26:
Set j := j + 1.
27:
Return to AGL∗ in Line 2 with tA /
∈ T (A
i
j ).
28: function REPAIR(M
i
2 , t)
29:
Let t1 ∈ M1, t2 ∈ M
i
2 , tp ∈ P such that t = (t1||t2) × tp.
30:
if t does not contain constraints then
31:
Return to AGL∗ in Line 2 with M
i+1
2
such that T (M
i+1
2
) = T (M
i
2 ) \ {t2} and t2 /
∈ T (A
i+1
0 ).
32:
else
t contains constraints
33:
Use abduction to eliminate t.
34:
Let c be the new constraint learned during abduction.
35:
Update αM
i+1
2
= αM
i
2 ∪ {c}.
36:
Let t
2 = t2 · c be the output of the abduction.
37:
Return to AGL∗ in Line 2 with M
i+1
2
such that T (M
i+1
2
) = (T (M
i
2 ) \ {t2}) ∪ {t
2 },
38:
and t2 ∈ T (A
i+1
0 ), t
2 ∈ T (A
i+1
0 )
4.2 Repair by Abduction
We now describe the repair we apply to M
i
2 , in case the error trace t contains constraints (see Algorithm 1,
line 32). Error traces with no constraints are removed from M
i
2 syntactically (line 31), while in abduction
we semantically eliminate t by making it infeasible. The new constraints are then added to the alphabet
of M
i+1
2
in a way that may eliminate additional error traces. Note that even-though we add new alphabet
letters to M 2 , we do not add new feasible traces, since the constraints added by abduction can only restrict
the behavior of M 2 , making more traces infeasible. Therefore, we do not add counterexamples to M 2 .
222
H. Frenkel et al.
1: function AGL∗
2:
//Membership Queries
3:
Let t2 ∈ (αM
i
2 )
∗ .
4:
if t2 ∈ T (M
i
2 ) then
5:
if M1||t2 P then
6:
Let t ∈ (M1||t2) × P be an error trace.
t is a cex proving M1||M
i
2 P
7:
REPAIR(M
i
2 , t)
8:
else
M1||t2 P
9:
Return to AGL∗ in Line 2 with t2 ∈ T (A
i
j ).
10:
else
t2 /
∈ T (M
i
2 )
11:
Return to AGL∗ in Line 2 with t2 /
∈ T (A
i
j ).
12:
//Equivalence Queries
13:
Let A
i
j be the candidate assumption generated by the learner.
14:
if M1||A
i
j P then
15:
if T (M
i
2 ) ⊆ T (A
i
j ) then
16:
Terminate and return M1||M
i
2 P .
17:
else
18:
Let t2 ∈ T (M
i
2 ) \ T (A
i
j ).
19:
Set j := j + 1
20:
Return to AGL∗ in Line 2 with t2 ∈ T (A
i
j ).
21:
else
M1||A
i
j P
22:
let t ∈ (M1||A
i
j ) × P be an error trace, and denote t = (t1||tA) × tP .
23:
if tA ∈ T (M
i
2 ) then
24:
REPAIR(M
i
2 , tA)
tA is a cex proving M1||M
i
2 P
25:
else
26:
Set j := j + 1.
27:
Return to AGL∗ in Line 2 with tA /
∈ T (A
i
j ).
28: function REPAIR(M
i
2 , t)
29:
Let t1 ∈ M1, t2 ∈ M
i
2 , tp ∈ P such that t = (t1||t2) × tp.
30:
if t does not contain constraints then
31:
Return to AGL∗ in Line 2 with M
i+1
2
such that T (M
i+1
2
) = T (M
i
2 ) \ {t2} and t2 /
∈ T (A
i+1
0 ).
32:
else
t contains constraints
33:
Use abduction to eliminate t.
34:
Let c be the new constraint learned during abduction.
35:
Update αM
i+1
2
= αM
i
2 ∪ {c}.
36:
Let t
2 = t2 · c be the output of the abduction.
37:
Return to AGL∗ in Line 2 with M
i+1
2
such that T (M
i+1
2
) = (T (M
i
2 ) \ {t2}) ∪ {t
2 },
38:
and t2 ∈ T (A
i+1
0 ), t
2 ∈ T (A
i+1
0 )
4.2 Repair by Abduction
We now describe the repair we apply to M
i
2 , in case the error trace t contains constraints (see Algorithm 1,
line 32). Error traces with no constraints are removed from M
i
2 syntactically (line 31), while in abduction
we semantically eliminate t by making it infeasible. The new constraints are then added to the alphabet
of M
i+1
2
in a way that may eliminate additional error traces. Note that even-though we add new alphabet
letters to M 2 , we do not add new feasible traces, since the constraints added by abduction can only restrict
the behavior of M 2 , making more traces infeasible. Therefore, we do not add counterexamples to M 2 .
222
H. Frenkel et al.