Q1:
In Korat, while searching for valid inputs, optimization done depends on the
order that repOK() accesses fields. What step should the users follow to
write efficient repOK() functions?

Because Korat monitors the order that fields are accessed, the most
important guideline is to avoid reading new fields until no more validation
can be performed using the fields that are already read. Many invalid data
structures can be discovered by only reading a subset of the fields -- for
example, a cycle in a tree can be discovered after reading the fields from
the nodes that participate in the cycle.

The repOK function should take advantage of this fact and do as many tests
as possible on the previously accessed subset of fields, before accessing
fields that have not yet been accessed.

Q2:
Explain the idea of "Finitization" presented by the paper. What is it? How
does it work? How can one use Finitization in Korat?

Finitization ensures that the search space of data structures is finite. To
do this, a finitization specifies the number of objects allowed in a
configuration and a (finite) set of possible values for each field in an
object. To write a finitization, the developer writes a Java method that
returns a data structure containing this information. Korat will use this
finitization to define the search space when looking for valid data
structures to use as test data.

Q3:
Give an example of a binary tree configuration and explain (a) why not all
configurations are valid and (b) what mechanism one can use that helps to
reduce test cases.

A configuration is specified by a vector of fields and object references.

An example configuration:

BinaryTree.root=N0
BinaryTree.size=2
N0.left=N1
N0.right=N1
N1.left=null
N1.right=null

This example configuration is invalid because one node has two parents. Many
other configurations will be invalid because they violate constraints like
these.

This fact can be exploited to reduce the number of test cases by eliminating
invalid configurations. To do this, the developer can write a repOK()
function that checks for invalid data structures, and Korat will use it to
reduce test cases.