One of the great features of the Alloy Analyzer is that it can produce examples illustrating the meaning of the user's model. These inside-the-box examples, which are formally permissible but (potentially) undesirable, help the user understand underconstraint bugs in the model. To get similar help with overconstraint bugs in the model the user needs to see examples that are desirable but formally excluded: that is, they need to see outside-the-box (near-miss) examples. We have developed a prototype extension of the Alloy Analyzer, named Bordeaux, that can find these examples that are near the border of what is permitted, and hence might be desirable. More generally, Bordeaux finds a pair of examples, a, c, at a minimum distance to each other, and where o satisfies model A and c satisfies model C. The primary use case described is when model C is the negation of model A, but there are also other uses for this relative minimization. Previous works, such as Aluminum, have focused on finding inside-the-box examples that are absolutely minimal.
展开▼
