– Exact. To eliminate only t from M 2 , we construct a program (an automaton) A t that accepts only t, and
complement it to construct A
t that accepts all traces except for t. Finally, we intersect A
t with M 2 .
– Approximate. Similarly to our repair via abduction in Section 4.2, we prevent the last transition that t
takes from reaching an accepting state. Let q be the state that t reaches. We mark q as non-accepting,
and add an accepting state q
, to which all in-going transitions to q are diverted, except for the last
transition on t. This way, some traces that lead to q are preserved by reaching q
instead, and the traces
that share the last transition of t are eliminated along with t. As we have argued, these transitions may
also be erroneous.
– Aggressive. In this simple method, we remove q, the state that t reaches, from the set of accepting states.
This way we eliminate t along with all other traces that lead to q. In case that every accepting state is
reached by some error trace, this repair might result in an empty language, creating a trivial repair.
However, our experiments show that in most cases, this method quickly leads to a non-trivial repair.
4.4 Correctness and Termination
For this discussion, we assume a sound and complete teacher who can answer the membership and equivalence queries in AG L ∗ , which require verifying communicating programs and properties with first-order
constraints.
As we have discussed earlier, AGR is not guaranteed to terminate, and there are cases where the REPAIR
stage may be called infinitely many times. However, in case that no repair is needed, or if a repaired system
is obtained after finitely many calls to REPAIR, then AGR is guaranteed to terminate with a correct answer.
To see why, consider a repaired system M
i
2 for which M 1 ||M
i
2 P . Since the goal of AG L ∗ is to
syntactically learn M
i
2 , which is regular, this stage will terminate at the latest when AG L ∗ learns exactly
M
i
2 (it may terminate sooner if a smaller appropriate assumption is found). Notice that, in particular, if
M 1 ||M 2 P , then AGR terminates with a correct answer in the first iteration of the verify-repair loop.
REPAIR is only invoked when a (real) error trace t is found in M
i
2 , in which case a new system M
i+1
2
,
that does not include t, is produced by REPAIR. If M 1 ||M
i
2 P , then an error trace is guaranteed to be
found by AG L ∗ either in the membership or equivalence phase. Therefore, also in case that M
i
2 violates P ,
the iteration is guaranteed to terminate. To conclude, we have the following.
Theorem 1. – An iteration i of AGR ends with an error trace t iff M 1 ||M
i
2 P , where M
i
2 is the repaired
system at iteration i.
– If, after finitely many iterations, a repaired program M
2 is such that M 1 ||M
2 P , then AGR terminates
with a correct answer.
We have shown that every iteration of AGR is guaranteed to terminate with a correct answer. The
detailed correctness proofs are in the full version of this paper [1].
In particular, since every iteration of AGR finds and removes an error trace t, and no new erroneous
traces are introduced in the updated system, then in case that M 2 has finitely many error traces, AGR is
guaranteed to terminate with a correctly repaired system.
5 Experimental Results and Conclusions
We implemented our AGR framework in Java, integrating L
∗ implementation from the LTSA tool [20]. We
used Z3 [10] as the teacher for the satisfaction queries in AG L ∗ , and for abduction in REPAIR.
Table 1 displays some results of running AGR on various examples, varying in their sizes, types of errors
– semantic and syntactic – and their amount. Additional results are in the full version of this paper [1],
and the full examples are available on [2]. The iterations column indicates the number of iterations of
the verify-repair loop, until a repaired M 2 is achieved. Examples with no errors were verified in the first
224
H. Frenkel et al.
complement it to construct A
t that accepts all traces except for t. Finally, we intersect A
t with M 2 .
– Approximate. Similarly to our repair via abduction in Section 4.2, we prevent the last transition that t
takes from reaching an accepting state. Let q be the state that t reaches. We mark q as non-accepting,
and add an accepting state q
, to which all in-going transitions to q are diverted, except for the last
transition on t. This way, some traces that lead to q are preserved by reaching q
instead, and the traces
that share the last transition of t are eliminated along with t. As we have argued, these transitions may
also be erroneous.
– Aggressive. In this simple method, we remove q, the state that t reaches, from the set of accepting states.
This way we eliminate t along with all other traces that lead to q. In case that every accepting state is
reached by some error trace, this repair might result in an empty language, creating a trivial repair.
However, our experiments show that in most cases, this method quickly leads to a non-trivial repair.
4.4 Correctness and Termination
For this discussion, we assume a sound and complete teacher who can answer the membership and equivalence queries in AG L ∗ , which require verifying communicating programs and properties with first-order
constraints.
As we have discussed earlier, AGR is not guaranteed to terminate, and there are cases where the REPAIR
stage may be called infinitely many times. However, in case that no repair is needed, or if a repaired system
is obtained after finitely many calls to REPAIR, then AGR is guaranteed to terminate with a correct answer.
To see why, consider a repaired system M
i
2 for which M 1 ||M
i
2 P . Since the goal of AG L ∗ is to
syntactically learn M
i
2 , which is regular, this stage will terminate at the latest when AG L ∗ learns exactly
M
i
2 (it may terminate sooner if a smaller appropriate assumption is found). Notice that, in particular, if
M 1 ||M 2 P , then AGR terminates with a correct answer in the first iteration of the verify-repair loop.
REPAIR is only invoked when a (real) error trace t is found in M
i
2 , in which case a new system M
i+1
2
,
that does not include t, is produced by REPAIR. If M 1 ||M
i
2 P , then an error trace is guaranteed to be
found by AG L ∗ either in the membership or equivalence phase. Therefore, also in case that M
i
2 violates P ,
the iteration is guaranteed to terminate. To conclude, we have the following.
Theorem 1. – An iteration i of AGR ends with an error trace t iff M 1 ||M
i
2 P , where M
i
2 is the repaired
system at iteration i.
– If, after finitely many iterations, a repaired program M
2 is such that M 1 ||M
2 P , then AGR terminates
with a correct answer.
We have shown that every iteration of AGR is guaranteed to terminate with a correct answer. The
detailed correctness proofs are in the full version of this paper [1].
In particular, since every iteration of AGR finds and removes an error trace t, and no new erroneous
traces are introduced in the updated system, then in case that M 2 has finitely many error traces, AGR is
guaranteed to terminate with a correctly repaired system.
5 Experimental Results and Conclusions
We implemented our AGR framework in Java, integrating L
∗ implementation from the LTSA tool [20]. We
used Z3 [10] as the teacher for the satisfaction queries in AG L ∗ , and for abduction in REPAIR.
Table 1 displays some results of running AGR on various examples, varying in their sizes, types of errors
– semantic and syntactic – and their amount. Additional results are in the full version of this paper [1],
and the full examples are available on [2]. The iterations column indicates the number of iterations of
the verify-repair loop, until a repaired M 2 is achieved. Examples with no errors were verified in the first
224
H. Frenkel et al.