Computing images is fundamental to many symbolic analysis techniques, and methods for computing images efficiently is an area of ongoing research. For this reason, the image package has been designed with lots of flexibility to easily allow new methods to be integrated (to add a new method, see the instructions in imgInt.h). Applications that use the image package can switch among different image methods simply by specifying the method type in the image initialization routine. By using the returned structure (Img_ImageInfo_t) from the initialization routine, all subsequent (forward or backward) image computations will be done using the specified method.
VIS users can control which image method is used by appropriately setting the "image_method" flag. Also, VIS users can set flags to control parameters for different image computation methods. Because the user has the ability to change the values of these flags, Img_ImageInfo_t structs should be freed and re-initialized whenever the VIS user changes the value of these flags.
Following are descriptions of the methods implemented. In the descriptions, x=x_1,...x_n is the set of domain variables, u=u_1,...,u_k is the set of quantify variables, y=y_1,...,y_m is the set of range variables, and f=f_1(x,u),...,f_m(x,u) is the set of functions under which we wish to compute images.
Monolithic: This is the most naive approach possible. A single relation T(x,y) is constructed during the initialization phase, using the computation (exists u (prod_i(y_i = f_i(x,u)))). To compute the forward image, where fromUpperBound=U(x), fromLowerBound=L(x), and toCareSet=C(y), we first compute a set A(x) between U(x) and L(x). Then, T(x,y) is simplified with respect to A(x) and C(y) to get T*. Finally, x is quantified from T* to produce the final answer. Backward images are computed analogously. The monolithic method does not recognize any user-settable flags for image computation.
IWLS95: This technique is based on the early quantification heuristic. The initialization process consists of following steps: