122
W. Wang et al.
input size, and the inputs are characterized by a logical formula [42]. Assume
the goal is to identify a bound that will lead to a feasible number of inputs that
can be executed within the testing budget. We use model counting to estimate
the number of solutions for different bounds.
Assume the inputs to the program under test are binary trees. Figure 3a shows
a partial Alloy specification for binary trees. The singleton sig BT represents the
tree, which has a root node and an integer size; the keyword lone defines a partial
function, so, e.g., the tree root is either exactly one node or none. Each node
has an integer key and a left and a right child. The predicate RepOk specifies
the constraints for a valid binary tree, which must be acyclic. The predicate
Acyclic specifies acyclicity; the operator “ ˆ” is transitive closure, “*” is reflexive
transitive closure, “+” is set union, “&” is set intersection, and “˜” is transpose.
Consider the constraint solving problem for size k so that the binary tree
has exactly k nodes and the keys are 1, . . . , k. Figure 3b illustrates the 5 nonisomorphic trees for size 3.
To show that the impact of symmetry is not limited to only approximate
counting, we perform this case study with the exact model counter ProjMC [40].
Table 3 shows the model counts for different sizes. As before, CNF-level symmetry breaking reduces the model count, which is further reduced by Alloy’s
Table 3: ProjMC results for binary tree constraints for trees with 6, 7, 8, 9, and
10 nodes. Time-out (t.o.) is 5000 sec.
6
7
8
9
10
# t[s]
#
t[s]
#
t[s]
# t[s]
#
t[s]
exact
no-sb 95040 5.57 2162160 129.25 57657600 3673.89
- t.o.
-
t.o.
cnf-sb 61538 7.39 1538628 184.97 25955296 3466.19
- t.o.
-
t.o.
dom-sb
357 0.10
1866 0.70
10286
4.94 60616 40.21 373001 610.35
man-sb 132 0.03
429 0.09
1430
0.34 4862 1.48 16796 10.53
OEIS
132
429
1430
4862
16796
one sig BT {
root: lone Node }
sig Node {
left, right: lone Node }
pred Acyclic(t: BT) {
all n: t.root.*(left + right) {
n !in n.^(left + right) -- no directed cycle
lone n.~(left + right) -- at most one parent
no n.left & n.right }} -- children are different
pred RepOk(t: BT) { Acyclic[t] }
...
N0
N1
N2
N0
N1
N2
N0
N1
N2
N0
N1
N2
N0
N1
N2
trees with 3 nodes. N0 is the root.
Fig. 3: (a) Alloy specification of binary trees. (b) Five non-isomorphic binary
W. Wang et al.
input size, and the inputs are characterized by a logical formula [42]. Assume
the goal is to identify a bound that will lead to a feasible number of inputs that
can be executed within the testing budget. We use model counting to estimate
the number of solutions for different bounds.
Assume the inputs to the program under test are binary trees. Figure 3a shows
a partial Alloy specification for binary trees. The singleton sig BT represents the
tree, which has a root node and an integer size; the keyword lone defines a partial
function, so, e.g., the tree root is either exactly one node or none. Each node
has an integer key and a left and a right child. The predicate RepOk specifies
the constraints for a valid binary tree, which must be acyclic. The predicate
Acyclic specifies acyclicity; the operator “ ˆ” is transitive closure, “*” is reflexive
transitive closure, “+” is set union, “&” is set intersection, and “˜” is transpose.
Consider the constraint solving problem for size k so that the binary tree
has exactly k nodes and the keys are 1, . . . , k. Figure 3b illustrates the 5 nonisomorphic trees for size 3.
To show that the impact of symmetry is not limited to only approximate
counting, we perform this case study with the exact model counter ProjMC [40].
Table 3 shows the model counts for different sizes. As before, CNF-level symmetry breaking reduces the model count, which is further reduced by Alloy’s
Table 3: ProjMC results for binary tree constraints for trees with 6, 7, 8, 9, and
10 nodes. Time-out (t.o.) is 5000 sec.
6
7
8
9
10
# t[s]
#
t[s]
#
t[s]
# t[s]
#
t[s]
exact
no-sb 95040 5.57 2162160 129.25 57657600 3673.89
- t.o.
-
t.o.
cnf-sb 61538 7.39 1538628 184.97 25955296 3466.19
- t.o.
-
t.o.
dom-sb
357 0.10
1866 0.70
10286
4.94 60616 40.21 373001 610.35
man-sb 132 0.03
429 0.09
1430
0.34 4862 1.48 16796 10.53
OEIS
132
429
1430
4862
16796
one sig BT {
root: lone Node }
sig Node {
left, right: lone Node }
pred Acyclic(t: BT) {
all n: t.root.*(left + right) {
n !in n.^(left + right) -- no directed cycle
lone n.~(left + right) -- at most one parent
no n.left & n.right }} -- children are different
pred RepOk(t: BT) { Acyclic[t] }
...
N0
N1
N2
N0
N1
N2
N0
N1
N2
N0
N1
N2
N0
N1
N2
trees with 3 nodes. N0 is the root.
Fig. 3: (a) Alloy specification of binary trees. (b) Five non-isomorphic binary