Automatic Program Repair (APR) is a practical research topic that produces techniques to automatically repair pro-grams to fix bugs. Most existing APR techniques are designed for imperative programs, such as C and Java, and rely on analyzing correct and incorrect executions of the program to identify and repair suspicious statements.

We introduce a new APR approach for models written in the Alloy declarative language, where the models are not “executed”, but rather converted into a logical formula and solved using backend constraint solvers. We present ATR, a tool that takes as input an Alloy specification consisting of some violated assertion and returns a repaired specification that satisfies the assertion. The key ideas are (i) analyzing the differences between counterexamples that do not satisfy the assertion and instances that do satisfy the assertion to guide the repair and (ii) generating repair candidates under specific templates and further pruning them using the counterexample and satisfying instances. Experimental results using existing large Alloy benchmarks show that ATR is effective in generating expressive repairs, i.e., repairs 66.3%of 1974 fault specifications, allowing it to repair specifications that cannot be handled by existing Alloy repair techniques. ATR and all benchmarks are open-source and available in the following anonymous Github repository for blind review: https://anonymous.4open.science/r/AlloyTemplateRepair/ .