(Step 1) ݐ ଶ א Ȯ ܯ ଶ
(Step ) ܯ ଵ צ ݐ ଶ ٧ ܲ
݁ݑݎݐ
ܿ ՚abduction on ݐ
ݐ ଶ
ᇱ ՚ ݐ ଶ ڄ ܿ
Generate
Assumption Loop
ݐ ଶ ב ܣ
݂݈ܽ݁ݏ
Membership
abduction
Repair
ࡳ ࡸכ
ݐ א Ȯሺܯ ଶ
ሻ
ݐ
cex ݐ א ሺݐ ଵ ȁ ݐ ൈ ܲ
݁ݑݎݐ
ݐ ଶ א ܣ
Equivalence
(Step 1) ܯ ଵ ȁȁܣ
٧ ܲ
(Step ) ܶ ܯ ଶ
ك ܶሺܣ
ሻ
݁ݑݎݐ
݂݈ܽ݁ݏ
ܯ ଵ ȁȁܯ ଶ
୧ ٧ ܲ
cex ݐ א ܣ ାଵ
݁ݑݎݐ
݂݈ܽ݁ݏ
݁ݑݎݐ
ݐଶ ՚ ݐ
ܿ א ݐ
݂݈ܽ݁ݏ
ݐ ଶ ב ܣ
ାଵ
݂݈ܽ݁ݏ
ݐ ଶ
ᇱ א ܣ
ାଵ
ݐ ଶ ב ܣ
ାଵ
ݐ ב Ȯሺܣ ାଵ
ሻ
ܣ
AGR
ܯ ଵ ǡ ܯ ଶ ǡ ܲ
݅ǡ ݆ ՚ Ͳ
ݐ ଶ
݂݈ܽ݁ݏ
݁ݑݎݐ
Fig. 5: The flow of AGR
traces. These queries are answered in accordance with traces we allow in A
i
j : traces in M
i
2 that in parallel
with M 1 satisfy P . If a trace t ∈ T (M
i
2 ) in parallel with M 1 does not satisfy P , then t is a bad behavior of
M 2 . Therefore, if such a t is found during the membership phase, REPAIR is invoked.
Once the learner reaches a stable assumption A
i
j , it passes it to the equivalence phase (lines 12-27). A
i
j
is a suitable assumption if both M 1 ||A
i
j P and T (M
i
2 ) ⊆ T (A
i
j ) hold. In this case, AGR terminates
and returns M
i
2 as a successful repair of M 2 . If M 1 ||A
i
j P , then a counterexample t is returned, that is
composed of bad traces in M 1 , A
i
j , and P . If the bad trace t 2 , the restriction of t to the alphabet of A
i
j , is
also in M
i
2 , then t 2 is a bad behavior of M
i
2 , and here too the REPAIR phase is invoked. Otherwise, AGR
returns to the membership phase with t 2 as a trace that should not be in A
i
j , and continues to learn A
i
j+1 .
As we have described, REPAIR is called when a bad trace t is found in (M 1 ||M
i
2 ) × P and should
be removed. If t contains no constraints then its sequence of actions is illegal and its subtrace t 2 from M
i
2
should be removed from M
i
2 . In this case, REPAIR returns to AG L ∗ with a new learning goal M
i+1
2
such
that T (M
i+1
2
) ⊆ T (M
i
2 ) \ {t 2 }, along with the answer “no” to the membership query on t 2 . In 4.3 we
discuss different methods for removing t 2 from M
i
2 .
The more interesting case is when t contains constraints. In this case, we not only remove the matching
t 2 from M
i
2 , but we also add a new constraint c to the alphabet of M
i+1
2
, which causes t 2 to be infeasible.
This way we eliminate t 2 , and may also eliminate a family of bad traces that violate the property in the
same manner. We deduce c using abduction, see Section 4.2. As before, REPAIR returns to AG L ∗ with a
new goal to be learned, but now also with an extended alphabet. The membership phase is then provided
with two new answers to the membership query: t 2 that should not be included in the new assumption, and
(t 2 · c) that should be included.
Incremental learning One of the advantages of AGR is that it is incremental, in the sense that membership
answers from previous iterations remain unchanged for the repaired system. Indeed, since this is the first
time that AG L ∗ queries t 2 , we can return to AG L ∗ with the answer t 2 /
∈ T (M
i+1
2
), without contradicting
any previous queries. In addition, t
2 obtained by abduction is a new word (over a new alphabet), which also
was not queried earlier. Therefore, we can incrementally add t 2 and t
2 as answers from the teacher, and
continue to use answers from previous queries on all other traces.
Assume, Guarantee or Repair
221
(Step ) ܯ ଵ צ ݐ ଶ ٧ ܲ
݁ݑݎݐ
ܿ ՚abduction on ݐ
ݐ ଶ
ᇱ ՚ ݐ ଶ ڄ ܿ
Generate
Assumption Loop
ݐ ଶ ב ܣ
݂݈ܽ݁ݏ
Membership
abduction
Repair
ࡳ ࡸכ
ݐ א Ȯሺܯ ଶ
ሻ
ݐ
cex ݐ א ሺݐ ଵ ȁ ݐ ൈ ܲ
݁ݑݎݐ
ݐ ଶ א ܣ
Equivalence
(Step 1) ܯ ଵ ȁȁܣ
٧ ܲ
(Step ) ܶ ܯ ଶ
ك ܶሺܣ
ሻ
݁ݑݎݐ
݂݈ܽ݁ݏ
ܯ ଵ ȁȁܯ ଶ
୧ ٧ ܲ
cex ݐ א ܣ ାଵ
݁ݑݎݐ
݂݈ܽ݁ݏ
݁ݑݎݐ
ݐଶ ՚ ݐ
ܿ א ݐ
݂݈ܽ݁ݏ
ݐ ଶ ב ܣ
ାଵ
݂݈ܽ݁ݏ
ݐ ଶ
ᇱ א ܣ
ାଵ
ݐ ଶ ב ܣ
ାଵ
ݐ ב Ȯሺܣ ାଵ
ሻ
ܣ
AGR
ܯ ଵ ǡ ܯ ଶ ǡ ܲ
݅ǡ ݆ ՚ Ͳ
ݐ ଶ
݂݈ܽ݁ݏ
݁ݑݎݐ
Fig. 5: The flow of AGR
traces. These queries are answered in accordance with traces we allow in A
i
j : traces in M
i
2 that in parallel
with M 1 satisfy P . If a trace t ∈ T (M
i
2 ) in parallel with M 1 does not satisfy P , then t is a bad behavior of
M 2 . Therefore, if such a t is found during the membership phase, REPAIR is invoked.
Once the learner reaches a stable assumption A
i
j , it passes it to the equivalence phase (lines 12-27). A
i
j
is a suitable assumption if both M 1 ||A
i
j P and T (M
i
2 ) ⊆ T (A
i
j ) hold. In this case, AGR terminates
and returns M
i
2 as a successful repair of M 2 . If M 1 ||A
i
j P , then a counterexample t is returned, that is
composed of bad traces in M 1 , A
i
j , and P . If the bad trace t 2 , the restriction of t to the alphabet of A
i
j , is
also in M
i
2 , then t 2 is a bad behavior of M
i
2 , and here too the REPAIR phase is invoked. Otherwise, AGR
returns to the membership phase with t 2 as a trace that should not be in A
i
j , and continues to learn A
i
j+1 .
As we have described, REPAIR is called when a bad trace t is found in (M 1 ||M
i
2 ) × P and should
be removed. If t contains no constraints then its sequence of actions is illegal and its subtrace t 2 from M
i
2
should be removed from M
i
2 . In this case, REPAIR returns to AG L ∗ with a new learning goal M
i+1
2
such
that T (M
i+1
2
) ⊆ T (M
i
2 ) \ {t 2 }, along with the answer “no” to the membership query on t 2 . In 4.3 we
discuss different methods for removing t 2 from M
i
2 .
The more interesting case is when t contains constraints. In this case, we not only remove the matching
t 2 from M
i
2 , but we also add a new constraint c to the alphabet of M
i+1
2
, which causes t 2 to be infeasible.
This way we eliminate t 2 , and may also eliminate a family of bad traces that violate the property in the
same manner. We deduce c using abduction, see Section 4.2. As before, REPAIR returns to AG L ∗ with a
new goal to be learned, but now also with an extended alphabet. The membership phase is then provided
with two new answers to the membership query: t 2 that should not be included in the new assumption, and
(t 2 · c) that should be included.
Incremental learning One of the advantages of AGR is that it is incremental, in the sense that membership
answers from previous iterations remain unchanged for the repaired system. Indeed, since this is the first
time that AG L ∗ queries t 2 , we can return to AG L ∗ with the answer t 2 /
∈ T (M
i+1
2
), without contradicting
any previous queries. In addition, t
2 obtained by abduction is a new word (over a new alphabet), which also
was not queried earlier. Therefore, we can incrementally add t 2 and t
2 as answers from the teacher, and
continue to use answers from previous queries on all other traces.
Assume, Guarantee or Repair
221