Slicing Models for Equiconsistency with Alloy - Replication Package

This repository contains the complete data and reproducibility artifacts accompanying the paper "Slicing Models for Equiconsistency with Alloy". The paper investigates the problem of extracting minimal submodels (equiconsistent slices) that preserve cross-domain consistency between heterogeneous model sets. Because equiconsistency is defined via quantification over an entire model space and cannot be computed directly, the paper introduces a counterexample-guided inductive synthesis (CEGIS) workflow that iteratively proposes, checks, and refines candidate slices. This reproduction package provides all models, specifications, solver encodings, experiment data, and scripts needed to reproduce the experiments and benchmarks presented in the paper. It includes the model instances used for evaluation, the Alloy and Alloy* encodings of the CEGIS implementations, the generated counterexamples, and the collected runtime and performance measurements.