Pattern-based debugging of declarative models

Pattern-based debugging compares the engineer´s model to a pre-computed library of patterns, and generates discriminating examples that help the engineer decide if the model´s constraints need to be strengthened or weakened. A number of tactics are used to help connect the generated examples to the text of the model. This technique augments existing example/counter-example generators and unsatisfiable core analysis tools, to help the engineer better localize and understand defects caused by complete overconstraint, partial overconstraint, and underconstraint. The technique is applied to localizing, understanding, and fixing a defect in an Alloy model of Dijkstra´s Dining Philosopher´s problem. Automating the search procedure remains as essential future work.