The nature of AG L ∗ is such that the assumptions it learns before it reaches M 2 may contain the traces
of M 2 and more, but still be represented by a smaller automaton. Therefore, similarly to [9], AG L ∗ often
terminates with an assumption A that is much smaller than M 2 . Indeed, our tool often produces very small
assumptions (see Section 5).
As mentioned before, not only that we determine whether M 1 ||M 2 P , but we also repair the program
in case it violates the specification. When M 1 ||M 2 P , the AG L ∗ algorithm returns an error trace t as
a witness for the violation. In this case, we initiate the REPAIR procedure, which eliminates t from M 2 .
REPAIR applies abduction in order to learn a new constraint which, when added to t, creates an infeasible
trace.
7 The new constraint enriches the alphabet in a way which may make similar traces infeasible as well.
We elaborate on our use of abduction in Section 4.2. The removal of t and the addition of the new constraint
result in a new goal M
2 for AG L ∗ to learn. We now return to AG L ∗ to search for a new assumption A
that
allows to verify M 1 ||M
2 P .
An important feature of our AGR algorithm is its incrementality. When learning an assumption A
for
M
2 we can use the membership queries previously asked for M 2 , since the answer for them has not been
changed. In the full version [1] we prove that the difference between the languages of M 2 and M
2 lies in
words (traces) whose membership has not yet been queried on M 2 . This allows the learning of M
2 to start
from the point where the previous learning has left off, resulting in a more efficient algorithm.
As opposed to the case where M 1 ||M 2 P , we cannot guarantee the termination of the repair process
in case M 1 ||M 2 P . This, since we are only guaranteed to remove one (bad) trace and add one (infeasible)
trace in every AGR REPAIR iteration (although in practice, every iteration may remove a larger set of
traces). Thus, we may never converge to a repaired system. Nevertheless, in case of property violation, our
algorithm always finds an error trace, thus a progress towards a “less erroneous” program is guaranteed.
It should be noted that the AG L ∗ part of our AGR algorithm deviates from the AG-rule of [9] in two
important ways. First, since the goal of our learning is M 2 rather than A w , our membership queries are
different in type and order. Second, in order to identify real error traces and send them to REPAIR as early
as possible, we add additional queries to the membership phase that reveal such traces. We then send them to
REPAIR without ever passing through equivalence queries, which improves the overall efficiency. Indeed,
our experiments include several cases in which all repairs were invoked from the membership phase. In these
cases, AGR ran an equivalence query only when it has already successfully repaired M 2 , and terminated.
4.1 The Assume-Guarantee-Repair (AGR) Algorithm
We now describe our AGR algorithm in more detail (see Algorithm 1). Figure 5 describes the flow of the
algorithm. AGR comprises two main parts, namely AG L ∗ and REPAIR.
The input to AGR are the components M 1 and M 2 , and the property P . While M 1 and P stay unchanged
during AGR, M 2 keeps being updated as long as the algorithm recognizes that it needs repair (we can
guarantee termination in certain cases, as we discuss in Section 4.4).
The algorithm works in iterations, where in every iteration the next updated M
i
2 is calculated, starting
with iteration i = 0, where M
0
2 = M 2 . An iteration starts with the membership phase in line 2, and ends
either when AG L ∗ successfully terminates (line 16) or when procedure REPAIR is called (lines 7 and 24).
When a new system M
i
2 is constructed, AG L ∗ does not start from scratch. The information that has been
used in previous iterations is still valid for M
i
2 . The new iteration is given additional new trace(s) that have
been added or removed from the previous M
i
2 (lines 9,11,20, 27).
AG L ∗ consists of two phases: membership, and equivalence.
The membership phase (lines 2-11) consists of a loop in which the learner constructs the next assumption A
i
j according to answers it gets from the teacher on a sequence of membership queries on various
7 There are also cases in which we do not use abduction, as discussed in Section 4.3
220
H. Frenkel et al.
of M 2 and more, but still be represented by a smaller automaton. Therefore, similarly to [9], AG L ∗ often
terminates with an assumption A that is much smaller than M 2 . Indeed, our tool often produces very small
assumptions (see Section 5).
As mentioned before, not only that we determine whether M 1 ||M 2 P , but we also repair the program
in case it violates the specification. When M 1 ||M 2 P , the AG L ∗ algorithm returns an error trace t as
a witness for the violation. In this case, we initiate the REPAIR procedure, which eliminates t from M 2 .
REPAIR applies abduction in order to learn a new constraint which, when added to t, creates an infeasible
trace.
7 The new constraint enriches the alphabet in a way which may make similar traces infeasible as well.
We elaborate on our use of abduction in Section 4.2. The removal of t and the addition of the new constraint
result in a new goal M
2 for AG L ∗ to learn. We now return to AG L ∗ to search for a new assumption A
that
allows to verify M 1 ||M
2 P .
An important feature of our AGR algorithm is its incrementality. When learning an assumption A
for
M
2 we can use the membership queries previously asked for M 2 , since the answer for them has not been
changed. In the full version [1] we prove that the difference between the languages of M 2 and M
2 lies in
words (traces) whose membership has not yet been queried on M 2 . This allows the learning of M
2 to start
from the point where the previous learning has left off, resulting in a more efficient algorithm.
As opposed to the case where M 1 ||M 2 P , we cannot guarantee the termination of the repair process
in case M 1 ||M 2 P . This, since we are only guaranteed to remove one (bad) trace and add one (infeasible)
trace in every AGR REPAIR iteration (although in practice, every iteration may remove a larger set of
traces). Thus, we may never converge to a repaired system. Nevertheless, in case of property violation, our
algorithm always finds an error trace, thus a progress towards a “less erroneous” program is guaranteed.
It should be noted that the AG L ∗ part of our AGR algorithm deviates from the AG-rule of [9] in two
important ways. First, since the goal of our learning is M 2 rather than A w , our membership queries are
different in type and order. Second, in order to identify real error traces and send them to REPAIR as early
as possible, we add additional queries to the membership phase that reveal such traces. We then send them to
REPAIR without ever passing through equivalence queries, which improves the overall efficiency. Indeed,
our experiments include several cases in which all repairs were invoked from the membership phase. In these
cases, AGR ran an equivalence query only when it has already successfully repaired M 2 , and terminated.
4.1 The Assume-Guarantee-Repair (AGR) Algorithm
We now describe our AGR algorithm in more detail (see Algorithm 1). Figure 5 describes the flow of the
algorithm. AGR comprises two main parts, namely AG L ∗ and REPAIR.
The input to AGR are the components M 1 and M 2 , and the property P . While M 1 and P stay unchanged
during AGR, M 2 keeps being updated as long as the algorithm recognizes that it needs repair (we can
guarantee termination in certain cases, as we discuss in Section 4.4).
The algorithm works in iterations, where in every iteration the next updated M
i
2 is calculated, starting
with iteration i = 0, where M
0
2 = M 2 . An iteration starts with the membership phase in line 2, and ends
either when AG L ∗ successfully terminates (line 16) or when procedure REPAIR is called (lines 7 and 24).
When a new system M
i
2 is constructed, AG L ∗ does not start from scratch. The information that has been
used in previous iterations is still valid for M
i
2 . The new iteration is given additional new trace(s) that have
been added or removed from the previous M
i
2 (lines 9,11,20, 27).
AG L ∗ consists of two phases: membership, and equivalence.
The membership phase (lines 2-11) consists of a loop in which the learner constructs the next assumption A
i
j according to answers it gets from the teacher on a sequence of membership queries on various
7 There are also cases in which we do not use abduction, as discussed in Section 4.3
220
H. Frenkel et al.