iteration, and are indicated by verification. We tested the three repair methods described in Section 4.3
for counterexamples without constraints, and used abduction when needed. Figure 6 presents comparisons
between the three methods in terms of run-time and the size of the repair and assumptions (note that the
graphs are given in logarithmic scale).
Table 1: AGR algorithm results on various examples
Example M1 Size M2 Size P Size Time (sec.) A size Repair Size Repair Method #Iterations
#4
64
64
3
95
7
verification
#6
2
27
2
0.106
5
27
aggress.
2
0.126
6
28
approx.
2
0.132
8
81
exact
2
#7
2
81
2
0.13
6
81
aggress.
2
0.138
7
82
approx.
2
0.165
9
243
exact
2
#8
2
243
2
0.15
8
243
aggress.
2
0.17
8
244
approx.
2
0.223
10
729
exact
2
#11
5
256
6
4.88
92
verification
#14
5
256
6
4.44
109
verification
#15
3
16
5
0.69
12
16
aggress.
5
0.28
13
18
approx.
3
4.27
44
864
exact
5
#16
4
256
8
6.63
113
256
aggress.
2
5.94
113
257
approx.
2
12.87
155
1280
exact
2
#19
3
16
5
1.07
18
18
aggress.
3
1.12
18
18
approx.
3
1.26
18
18
exact
3
#22
2
4
2
0.09
1
4 (trivial)
aggress.
4
0.21
6
8
approx.
5
timeout
exact
timeout
Most of our examples model multi-client-server communication protocols, with varying sizes. Our tool
managed repairing all these examples when needed.
As can be seen in Table 1, our tool successfully generates assumptions that are significantly smaller
than the repaired and the original M 2 .
For the examples that needed repair, in most cases our tool needed 2-5 iterations of verify-repair in
order to successfully construct a repaired component. Interestingly, in example #15 the aggressive method
converged slower than the approximate method. This is due to the structure of M 2 , in which different
error traces lead to different states. Marking these states as non-accepting removed each trace separately.
However, some of these traces have a common transition, and preventing this transition from reaching an
accepting state, as done in the approximate method, managed removing several error traces in a single
repair. This example also includes repairs by abduction (as do examples #16, #18 and #19).
Assume, Guarantee or Repair
225
for counterexamples without constraints, and used abduction when needed. Figure 6 presents comparisons
between the three methods in terms of run-time and the size of the repair and assumptions (note that the
graphs are given in logarithmic scale).
Table 1: AGR algorithm results on various examples
Example M1 Size M2 Size P Size Time (sec.) A size Repair Size Repair Method #Iterations
#4
64
64
3
95
7
verification
#6
2
27
2
0.106
5
27
aggress.
2
0.126
6
28
approx.
2
0.132
8
81
exact
2
#7
2
81
2
0.13
6
81
aggress.
2
0.138
7
82
approx.
2
0.165
9
243
exact
2
#8
2
243
2
0.15
8
243
aggress.
2
0.17
8
244
approx.
2
0.223
10
729
exact
2
#11
5
256
6
4.88
92
verification
#14
5
256
6
4.44
109
verification
#15
3
16
5
0.69
12
16
aggress.
5
0.28
13
18
approx.
3
4.27
44
864
exact
5
#16
4
256
8
6.63
113
256
aggress.
2
5.94
113
257
approx.
2
12.87
155
1280
exact
2
#19
3
16
5
1.07
18
18
aggress.
3
1.12
18
18
approx.
3
1.26
18
18
exact
3
#22
2
4
2
0.09
1
4 (trivial)
aggress.
4
0.21
6
8
approx.
5
timeout
exact
timeout
Most of our examples model multi-client-server communication protocols, with varying sizes. Our tool
managed repairing all these examples when needed.
As can be seen in Table 1, our tool successfully generates assumptions that are significantly smaller
than the repaired and the original M 2 .
For the examples that needed repair, in most cases our tool needed 2-5 iterations of verify-repair in
order to successfully construct a repaired component. Interestingly, in example #15 the aggressive method
converged slower than the approximate method. This is due to the structure of M 2 , in which different
error traces lead to different states. Marking these states as non-accepting removed each trace separately.
However, some of these traces have a common transition, and preventing this transition from reaching an
accepting state, as done in the approximate method, managed removing several error traces in a single
repair. This example also includes repairs by abduction (as do examples #16, #18 and #19).
Assume, Guarantee or Repair
225