Slicing Models for Equiconsistency with Alloy

Model-driven development enables collaborative design across heterogeneous modelling domains, but it also raises the risk of inconsistent models. We study the problem of extracting minimal submodels that preserve cross-domain consistency. Concretely, given two sets of models related by a consistency specification and a model from the first set, we seek an equiconsistent slice, that is, a submodel that preserves the same consistency relationships with models of the second set. Since the definition of equiconsistency quantifies over the complete second set, a direct computation is infeasible (and undecidable in general). Thus, we formulate slicing as a declarative synthesis problem and solve it using counterexample-guided inductive synthesis (CEGIS). The procedure iteratively proposes candidate slices and refines them using counterexamples (models obtained as violation witnesses if a candidate is not a valid slice). Iterating the CEGIS loop converges to equiconsistent, minimal slices within the bounds used by the model finder. We instantiate the abstract equiconsistency slice problem using attributed typed graphs as models, express consistency relations declaratively, and further realize it using relational logic and SAT-based solving. ... mehrWe then obtain an automated synthesis of equiconsistent slices based only on the consistency relation. We evaluate the method on a synthetic dataset to compare three CEGIS implementations: an explicit loop in Alloy, an explicit loop in Alloy*, and a quantified encoding in Alloy*. We highlight their practical trade-offs.