cptest4choco

cptest4choco is a testing framework that we built for testing choco constraint models. cptest4choco is a complete Java testing library for choco with a backend process that produces dedicated choco programs as output. These programs have then to be solved in order to detect, localize and correct faults. The distribution includes four packages, namely detection, localization, correction and negation, which are described below.

Detection package:

This package contains first an implementation of the fault models and non-conformity relations. Second, it implements the conformity relations found in (Lazaar et al.,  Constraints12). It also contains a full implementation of fault-detection process. This process takes as input two choco models and, when possible, it returns a non-conformity, i.e., an assignment which satisfies the constraints of one model but not the other. From a Choco-user point of view, different testing functionalities of cptest4choco can be exploited just  by importing this package in a choco project.

Localization package:

This package implements the fault localization approach presented in (Lazaar et al., ICTAI10). The localization process takes as input the non-conformity returned by the detection package, and returns a suspeciousSet. This set helps the user spotting the constraint responsible of the fault in the constraint model.

Correction package:

This package includes an implementation of algorithm that can be found in (Lazaar et al., ICST11). The automatic correction process takes as input the suspiciousSet previously computed, and proposes a set of possible corrections to restore the conformity between a cput and its model-Oracle. This package is the most advanced technology of cptest4choco and needs to be carefully explained to the user.

Negation package:

Our approach of fault-detection and automatic correction is based on constraint refutation, and the usage of automatic constraint negation. In cptest4choco , a specific module is given to negate most of the available constraints in choco.
The cptest4choco library handles several global constraints over discrete values; either by rewriting them using arithmetic and/or logic constraints (e.g., allDifferent can be rewritten using inequality constraints), or by expressed them using other global constraints. For instance, the negation of the atLeast global constraint can simply be obtained by considering the atMost global constraint. However, the module cannot negate all the available global constraints. For instance, global constraints such as cumulative or circuit require additional developments to be easily negated. The negation of complex global constraints is included in our further work.